let x, y be Element of REAL+ ; :: thesis: ( not x *' y = {} or x = {} or y = {} )
assume A1: x *' y = {} ; :: thesis: ( x = {} or y = {} )
( DEDEKIND_CUT x = {} or DEDEKIND_CUT y = {} )
proof
assume DEDEKIND_CUT x <> {} ; :: thesis: DEDEKIND_CUT y = {}
then consider r0 being Element of RAT+ such that
A2: r0 in DEDEKIND_CUT x by SUBSET_1:4;
assume DEDEKIND_CUT y <> {} ; :: thesis: contradiction
then consider s0 being Element of RAT+ such that
A3: s0 in DEDEKIND_CUT y by SUBSET_1:4;
r0 *' s0 in { (r *' s) where r, s is Element of RAT+ : ( r in DEDEKIND_CUT x & s in DEDEKIND_CUT y ) } by A2, A3;
hence contradiction by A1, Lm11; :: thesis: verum
end;
hence ( x = {} or y = {} ) by Lm10; :: thesis: verum