theorem Th56: :: ORDINAL3:56

for A being Ordinal holds
( A -^ {} = A & {} -^ A = {} )