const SNo : set prop const SNoLt : set set prop term < = SNoLt infix < 2020 2020 const In : set set prop term iIn = In infix iIn 2000 2000 const SNoL : set set const SNoR : set set axiom SNoLt_SNoL_or_SNoR_impred: !x:set.!y:set.SNo x -> SNo y -> x < y -> !P:prop.(!z:set.z iIn SNoL y -> z iIn SNoR x -> P) -> (x iIn SNoL y -> P) -> (y iIn SNoR x -> P) -> P axiom SNoLt_trichotomy_or_impred: !x:set.!y:set.SNo x -> SNo y -> !P:prop.(x < y -> P) -> (x = y -> P) -> (y < x -> P) -> P claim !x:set.!y:set.SNo x -> SNo y -> !P:prop.(x = y -> P) -> (!z:set.z iIn SNoL y -> z iIn SNoR x -> P) -> (x iIn SNoL y -> P) -> (y iIn SNoR x -> P) -> (!z:set.z iIn SNoR y -> z iIn SNoL x -> P) -> (x iIn SNoR y -> P) -> (y iIn SNoL x -> P) -> P