const In : set set prop term iIn = In infix iIn 2000 2000 term nIn = \x:set.\y:set.~ x iIn y term Subq = \x:set.\y:set.!z:set.z iIn x -> z iIn y term TransSet = \x:set.!y:set.y iIn x -> Subq y x axiom or3I1: !P:prop.!Q:prop.!R:prop.P -> P | Q | R axiom or3I3: !P:prop.!Q:prop.!R:prop.R -> P | Q | R const ordinal : set prop axiom ordinal_Hered: !x:set.ordinal x -> !y:set.y iIn x -> ordinal y axiom set_ext: !x:set.!y:set.Subq x y -> Subq y x -> x = y axiom or3I2: !P:prop.!Q:prop.!R:prop.Q -> P | Q | R axiom xm: !P:prop.P | ~ P axiom In_ind: !p:set prop.(!x:set.(!y:set.y iIn x -> p y) -> p x) -> !x:set.p x lemma !x:set.!y:set.!z:set.(!w:set.w iIn x -> !u:set.ordinal w -> ordinal u -> w iIn u | w = u | u iIn w) -> ordinal x -> ordinal y -> nIn y x -> z iIn x -> ordinal z -> z iIn y lemma !x:set.!y:set.!z:set.(!w:set.w iIn y -> ordinal x -> ordinal w -> x iIn w | x = w | w iIn x) -> ordinal x -> ordinal y -> nIn x y -> z iIn y -> ordinal z -> z iIn x claim !x:set.!y:set.ordinal x -> ordinal y -> x iIn y | x = y | y iIn x