theorem :: ORDINAL3:37
for A, B being Ordinal st A *^ B = 1 holds
( A = 1 & B = 1 )