const If_i : prop set set set const SNoLe : set set prop term <= = SNoLe infix <= 2020 2020 const Empty : set const minus_SNo : set set term - = minus_SNo term abs_SNo = \x:set.If_i (Empty <= x) x - x axiom If_i_1: !P:prop.!x:set.!y:set.P -> If_i P x y = x claim !x:set.Empty <= x -> abs_SNo x = x