const In : set set prop term iIn = In infix iIn 2000 2000 const Sing : set set axiom SingI: !x:set.x iIn Sing x const binunion : set set set axiom binunionI1: !x:set.!y:set.!z:set.z iIn x -> z iIn binunion x y const Inj1 : set set const Empty : set const Repl : set (set set) set axiom Inj1_eq: !x:set.Inj1 x = binunion (Sing Empty) (Repl x Inj1) claim !x:set.Empty iIn Inj1 x