let X be Subset of REAL ; :: thesis: X = 0 ++ X

now

let x be set ; :: thesis: ( ( x in X implies x in 0 ++ X ) & ( x in 0 ++ X implies x in X ) )

hereby :: thesis: ( x in 0 ++ X implies x in X )

assume A1: x in X ; :: thesis: x in 0 ++ X
then reconsider x' = x as Real ;
0 + x' = x ;
hence x in 0 ++ X by A1; :: thesis: verum

end;

assume x in 0 ++ X ; :: thesis: x in X
then consider r3 being Real such that
A2: ( x = 0 + r3 & r3 in X ) ;
thus x in X by A2; :: thesis: verum

end;

hence X = 0 ++ X by TARSKI:2; :: thesis: verum