theorem Th11: :: ORDINAL6:11

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