const SNo : set prop const SNoLt : set set prop term < = SNoLt infix < 2020 2020 axiom SNoLt_trichotomy_or: !x:set.!y:set.SNo x -> SNo y -> x < y | x = y | y < x claim !x:set.!y:set.SNo x -> SNo y -> !P:prop.(x < y -> P) -> (x = y -> P) -> (y < x -> P) -> P