let V be non empty right_complementable Abelian add-associative right_zeroed addLoopStr ; :: thesis: for M, N being Subset of V
for v being Element of V st v in N holds
M + {v} c= M + N
let M, N be Subset of V; :: thesis: for v being Element of V st v in N holds
M + {v} c= M + N
let v be Element of V; :: thesis: ( v in N implies M + {v} c= M + N )
assume A1: v in N ; :: thesis: M + {v} c= M + N
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in M + {v} or x in M + N )
assume A2: x in M + {v} ; :: thesis: x in M + N
then reconsider x = x as Element of V ;
x in { (u1 + v1) where u1, v1 is Element of V : ( u1 in M & v1 in {v} ) } by A2, RUSUB_4:def 9;
then consider u2, v2 being Element of V such that
A3: x = u2 + v2 and
A4: u2 in M and
A5: v2 in {v} ;
x = u2 + v by A3, A5, TARSKI:def 1;
then x in { (u1 + v1) where u1, v1 is Element of V : ( u1 in M & v1 in N ) } by A1, A4;
hence x in M + N by RUSUB_4:def 9; :: thesis: verum