let IT be Subset of REAL ; :: thesis: ( IT = p ++ X iff IT = { (p + r3) where r3 is Real : r3 in X } )

hereby :: thesis: ( IT = { (p + r3) where r3 is Real : r3 in X } implies IT = p ++ X )

assume A1: IT = p ++ X ; :: thesis: IT = { (p + r3) where r3 is Real : r3 in X }
A2: IT c= { (p + r3) where r3 is Real : r3 in X }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in IT or x in { (p + r3) where r3 is Real : r3 in X } )
assume A3: x in IT ; :: 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, A3, MEASURE6:def 6;
hence x in { (p + r3) where r3 is Real : r3 in X } ; :: thesis: verum

end;

{ (p + r3) where r3 is Real : r3 in X } c= IT

proof

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

end;

hence IT = { (p + r3) where r3 is Real : r3 in X } by A2, XBOOLE_0:def 10; :: thesis: verum

end;

assume A4: IT = { (p + r3) where r3 is Real : r3 in X } ; :: thesis: IT = p ++ X

now

let y be Real; :: thesis: ( ( y in IT implies ex z being Real st
( z in X & y = p + z ) ) & ( ex z being Real st
( z in X & y = p + z ) implies y in IT ) )

hereby :: thesis: ( ex z being Real st
( z in X & y = p + z ) implies y in IT )

assume y in IT ; :: thesis: ex z being Real st
( z in X & y = p + z )
then ex r3 being Real st
( y = p + r3 & r3 in X ) by A4;
hence ex z being Real st
( z in X & y = p + z ) ; :: thesis: verum

end;

given z being Real such that A5: ( z in X & y = p + z ) ; :: thesis: y in IT
thus y in IT by A4, A5; :: thesis: verum

end;

hence IT = p ++ X by MEASURE6:def 6; :: thesis: verum