const ordinal : set prop const SNo : set prop axiom ordinal_SNo: !x:set.ordinal x -> SNo x const Subq : set set prop const SNoLe : set set prop term <= = SNoLe infix <= 2020 2020 axiom ordinal_Subq_SNoLe: !x:set.!y:set.ordinal x -> ordinal y -> Subq x y -> x <= y const SNoLt : set set prop term < = SNoLt infix < 2020 2020 axiom SNoLtLe_tra: !x:set.!y:set.!z:set.SNo x -> SNo y -> SNo z -> x < y -> y <= z -> x < z axiom SNoLt_irref: !x:set.~ x < x axiom FalseE: ~ False const In : set set prop term iIn = In infix iIn 2000 2000 axiom ordinal_In_Or_Subq: !x:set.!y:set.ordinal x -> ordinal y -> x iIn y | Subq y x claim !x:set.!y:set.ordinal x -> ordinal y -> x < y -> x iIn y