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 ) ; :: thesis: ( q3 + r in q3 ++ X implies r in X )
assume q3 + r in q3 ++ X ; :: thesis: r in X
then ex mr being Real st
( q3 + r = q3 + mr & mr in X ) ;
hence r in X ; :: thesis: verum