let r be real number ; :: thesis: for X being Subset of REAL
for q3 being Real holds
( r in X iff q3 + r in q3 ++ X )
let X be Subset of REAL; :: thesis: for q3 being Real holds
( r in X iff q3 + r in q3 ++ X )
let q3 be Real; :: thesis: ( r in X iff q3 + r in q3 ++ X )
thus ( r in X implies q3 + r in q3 ++ X ) by MEMBER_1:141; :: thesis: ( q3 + r in q3 ++ X implies r in X )
assume q3 + r in q3 ++ X ; :: thesis: r in X
then q3 + r in { (q3 + r3) where r3 is Real : r3 in X } by Lm5;
then ex mr being Real st
( q3 + r = q3 + mr & mr in X ) ;
hence r in X ; :: thesis: verum