Proofgold Address

Known FalseE^FalseE : False ⟶ ∀ x0 : ο . x0
Known 2901c..^EmptyE : ∀ x0 . In x0 0 ⟶ False
Known d0de4..^Empty_eq : ∀ x0 . (∀ x1 . nIn x1 x0) ⟶ x0 = 0
Known 9d2e6..^nIn_I2 : ∀ x0 x1 . (In x0 x1 ⟶ False) ⟶ nIn x0 x1
Known 2109a..^UnionE2 : ∀ x0 x1 . In x1 (Union x0) ⟶ ∀ x2 : ο . (∀ x3 . In x1 x3 ⟶ In x3 x0 ⟶ x2) ⟶ x2
Known 367e6..^SubqE : ∀ x0 x1 . Subq x0 x1 ⟶ ∀ x2 . In x2 x0 ⟶ In x2 x1
Theorem 3e831.. : ∀ x0 . Subq x0 (Union 0) ⟶ ∀ x1 . In x1 x0 ⟶ and (∀ x2 . not (exactly5 x0) ⟶ ∀ x3 : ο . (∀ x4 . and (Subq x4 x0) (∀ x5 . In x5 0 ⟶ not (ordinal x2)) ⟶ x3) ⟶ x3) (∀ x2 : ο . (∀ x3 . and (In x3 x1) (∃ x4 . not (TransSet x1)) ⟶ x2) ⟶ x2) ⟶ atleast4 x1 (proof)