Proofgold Proposition

∀ x0 . x0 ∈ real ⟶ ∀ x1 . x1 ∈ real ⟶ SNoLt x0 x1 ⟶ ∃ x2 . and (x2 ∈ SNoS_ omega) (and (SNoLt x0 x2) (SNoLt x2 x1))

type
prop

theory
HotG

name
real_Lt_SNoS_omega_inter

proof
PUeVh..

Megalodon
-

proofgold address
TMdw4..

creator
29749 PrQUS../ae528..

owner
29749 PrQUS../ae528..

term root
10f82..