let x be Real; :: thesis: for A being Subset of REAL st A = REAL holds
x ++ A = A
let A be Subset of REAL; :: thesis: ( A = REAL implies x ++ A = A )
assume A1: A = REAL ; :: thesis: x ++ A = A
A c= x ++ A

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in A or y in x ++ A )
assume y in A ; :: thesis: y in x ++ A
then reconsider y = y as Real ;
reconsider z = y - x as Element of REAL by XREAL_0:def 1;
y = x + z ;
hence y in x ++ A by A1, Lm1; :: thesis: verum

end;

hence x ++ A = A by A1; :: thesis: verum