Proofgold Address

Param and^and : ο → ο → ο
Param atleastp^atleastp : ι → ι → ο
Param omega^omega : ι
Param real^real : ι
Param not^not : ο → ο
Param equip^equip : ι → ι → ο
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Param Subq^Subq : ι → ι → ο
Known Subq_atleastp^{Subq_atleastp} : ∀ x0 x1 . x0 ⊆ x1 ⟶ atleastp x0 x1
Param SNoS_^SNoS_ : ι → ι
Known Subq_tra^Subq_tra : ∀ x0 x1 x2 . x0 ⊆ x1 ⟶ x1 ⊆ x2 ⟶ x0 ⊆ x2
Known omega_SNoS_omega^{omega_SNoS_omega} : omega ⊆ SNoS_ omega
Known SNoS_omega_real^{SNoS_omega_real} : SNoS_ omega ⊆ real
Known form100_22_real_uncountable_equip^{form100_22_real_uncountable_equip} : not (equip real omega)
Theorem c2bf7..^{form100_22_real_uncountable} : and (atleastp omega real) (not (equip real omega)) (proof)