const In : set set prop term iIn = In infix iIn 2000 2000 term nIn = \x:set.\y:set.~ x iIn y const Empty : set const Inj1 : set set axiom Inj1I1: !x:set.Empty iIn Inj1 x axiom EmptyE: !x:set.nIn x Empty claim !x:set.Inj1 x != Empty