let x, y be Element of REAL+ ; :: thesis: ( x = {} implies x *' y = {} )
set A = DEDEKIND_CUT x;
set B = DEDEKIND_CUT y;
assume A1: x = {} ; :: thesis: x *' y = {}
for e being object holds not e in { (r *' s) where r, s is Element of RAT+ : ( r in DEDEKIND_CUT x & s in DEDEKIND_CUT y ) }
proof
given e being object such that A2: e in { (r *' s) where r, s is Element of RAT+ : ( r in DEDEKIND_CUT x & s in DEDEKIND_CUT y ) } ; :: thesis: contradiction
ex r, s being Element of RAT+ st
( e = r *' s & r in DEDEKIND_CUT x & s in DEDEKIND_CUT y ) by A2;
hence contradiction by A1, Lm10; :: thesis: verum
end;
then { (r *' s) where r, s is Element of RAT+ : ( r in DEDEKIND_CUT x & s in DEDEKIND_CUT y ) } = {} by XBOOLE_0:def 1;
hence x *' y = {} by Lm11; :: thesis: verum