theorem :: XXREAL_3:73

for x, y being ExtReal holds
( not x * y in REAL or ( x in REAL & y in REAL ) or x * y = 0 ) by Lm23;