let A be Subset of REAL; :: thesis: for x being Real holds (- x) ++ (x ++ A) = A
let x be Real; :: thesis: (- x) ++ (x ++ A) = A
thus (- x) ++ (x ++ A) c= A :: according to XBOOLE_0:def 10 :: thesis: A c= (- x) ++ (x ++ A)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (- x) ++ (x ++ A) or y in A )
assume A1: y in (- x) ++ (x ++ A) ; :: thesis: y in A
then reconsider y = y as Real ;
consider z being Real such that
A2: z in x ++ A and
A3: y = (- x) + z by A1, Lm1;
ex t being Real st
( t in A & z = x + t ) by A2, Lm1;
hence y in A by A3; :: thesis: verum

end;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in A or y in (- x) ++ (x ++ A) )
assume A4: y in A ; :: thesis: y in (- x) ++ (x ++ A)
then reconsider y = y as Real ;
reconsider t = y - (- x) as Real ;
reconsider z = t - x as Real ;
A5: z = (- x) + t ;
t in x ++ A by A4, Lm1;
hence y in (- x) ++ (x ++ A) by A5, Lm1; :: thesis: verum