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 A1: y in x ** {} ; :: thesis: y in {}
then reconsider y = y as Real ;
ex z being Real st
( z in {} & y = x * z ) by A1, INTEGRA2:def 2;
hence y in {} ; :: thesis: verum

end;

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