theorem Th4: :: ORDINAL6:4

for a, b being Ordinal holds
( a c= b iff b nin a )