theorem :: ORDINAL3:12

for A, B being Ordinal holds
( A \/ B = A or A \/ B = B )