theorem Th54: :: ORDINAL3:54

for A being Ordinal holds A -^ A = {}