let x be Real; :: thesis: x ** {} = {}
x ** {} c= {}

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in x ** {} or y in {} )
assume A2: y in x ** {} ; :: thesis: y in {}
then reconsider y = y as Real ;
consider z being Real such that
A3: ( z in {} & y = x * z ) by A2, INTEGRA2:def 2;
thus y in {} by A3; :: thesis: verum

end;

hence x ** {} = {} ; :: thesis: verum