const SNo : set prop const Empty : set axiom SNo_0: SNo Empty const SNoLt : set set prop term < = SNoLt infix < 2020 2020 const mul_SNo : set set set term * = mul_SNo infix * 2291 2290 axiom neg_mul_SNo_Lt: !x:set.!y:set.!z:set.SNo x -> x < Empty -> SNo y -> SNo z -> z < y -> x * y < x * z axiom SNoLt_irref: !x:set.~ x < x axiom pos_mul_SNo_Lt: !x:set.!y:set.!z:set.SNo x -> Empty < x -> SNo y -> SNo z -> y < z -> x * y < x * z 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 axiom FalseE: ~ False claim !x:set.!y:set.!z:set.SNo x -> x != Empty -> SNo y -> SNo z -> x * y = x * z -> y = z