theorem :: ORDINAL3:31

for A, B being Ordinal holds
( not A *^ B = {} or A = {} or B = {} )