let X be Subset of REAL; :: thesis: for p being Real holds p ++ X = { (p + r3) where r3 is Real : r3 in X }
let p be Real; :: thesis: p ++ X = { (p + r3) where r3 is Real : r3 in X }
thus p ++ X c= { (p + r3) where r3 is Real : r3 in X } :: according to XBOOLE_0:def 10 :: thesis: { (p + r3) where r3 is Real : r3 in X } c= p ++ X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in p ++ X or x in { (p + r3) where r3 is Real : r3 in X } )
assume A1: x in p ++ X ; :: thesis: x in { (p + r3) where r3 is Real : r3 in X }
then reconsider x9 = x as Real ;
ex z being Real st
( z in X & x9 = p + z ) by A1, Lm1;
hence x in { (p + r3) where r3 is Real : r3 in X } ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (p + r3) where r3 is Real : r3 in X } or x in p ++ X )
assume x in { (p + r3) where r3 is Real : r3 in X } ; :: thesis: x in p ++ X
then ex r3 being Real st
( x = p + r3 & r3 in X ) ;
hence x in p ++ X by Lm1; :: thesis: verum