let x be real number ; :: thesis: x ++ {} = {}
thus x ++ {} c= {} :: according to XBOOLE_0:def 10 :: thesis: {} c= x ++ {}

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, Def6;
hence y in {} ; :: thesis: verum

end;

thus {} c= x ++ {} by XBOOLE_1:2; :: thesis: verum