const ordinal : set prop const In : set set prop term iIn = In infix iIn 2000 2000 axiom ordinal_trichotomy_or: !x:set.!y:set.ordinal x -> ordinal y -> x iIn y | x = y | y iIn x axiom or3E: !P:prop.!Q:prop.!R:prop.P | Q | R -> !P2:prop.(P -> P2) -> (Q -> P2) -> (R -> P2) -> P2 claim !x:set.!y:set.ordinal x -> ordinal y -> !P:prop.(x iIn y -> P) -> (x = y -> P) -> (y iIn x -> P) -> P