let a, b be Ordinal; :: thesis: ( a c= b iff b nin a )
( a c= b & b in a implies b in b ) ;
hence ( a c= b iff b nin a ) by ORDINAL1:16; :: thesis: verum