| ∀ x0 . x0 ⊆ SNoS_ omega ⟶ ∀ x1 . x1 ⊆ SNoS_ omega ⟶ SNoCutP x0 x1 ⟶ (x0 = 0 ⟶ ∀ x2 : ο . x2) ⟶ (x1 = 0 ⟶ ∀ x2 : ο . x2) ⟶ (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 : ο . (∀ x4 . and (x4 ∈ x0) (SNoLt x2 x4) ⟶ x3) ⟶ x3) ⟶ (∀ x2 . x2 ∈ x1 ⟶ ∀ x3 : ο . (∀ x4 . and (x4 ∈ x1) (SNoLt x4 x2) ⟶ x3) ⟶ x3) ⟶ SNoCut x0 x1 ∈ real |
|
|
|
| name |
|---|
| real_SNoCut_SNoS_omega |
|
|
|
|
|
|
|