const In : set set prop term iIn = In infix iIn 2000 2000 term Subq = \x:set.\y:set.!z:set.z iIn x -> z iIn y const ordinal : set prop const SNo : set prop const SNoLev : set set const SNoLt : set set prop term < = SNoLt infix < 2020 2020 axiom ordinal_SNoLev_max: !x:set.ordinal x -> !y:set.SNo y -> SNoLev y iIn x -> y < x axiom SNoLt_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 SNoR : set set axiom SNoR_E: !x:set.SNo x -> !y:set.y iIn SNoR x -> !P:prop.(SNo y -> SNoLev y iIn SNoLev x -> x < y -> P) -> P const Empty : set axiom Empty_Subq_eq: !x:set.Subq x Empty -> x = Empty var x:set hyp ordinal x hyp SNo x claim SNoLev x = x -> SNoR x = Empty