let V be non empty addLoopStr ; :: thesis: for M being Subset of V
for v being Element of V holds {v} + M = v + M
let M be Subset of V; :: thesis: for v being Element of V holds {v} + M = v + M
let v be Element of V; :: thesis: {v} + M = v + M
for x being object st x in v + M holds
x in {v} + M

proof

let x be object ; :: thesis: ( x in v + M implies x in {v} + M )
assume x in v + M ; :: thesis: x in {v} + M
then A1: ex u being Element of V st
( x = v + u & u in M ) ;
v in {v} by TARSKI:def 1;
hence x in {v} + M by A1; :: thesis: verum

end;

then A2: v + M c= {v} + M ;
for x being object st x in {v} + M holds
x in v + M

proof

let x be object ; :: thesis: ( x in {v} + M implies x in v + M )
assume x in {v} + M ; :: thesis: x in v + M
then consider v1, u1 being Element of V such that
A3: x = v1 + u1 and
A4: v1 in {v} and
A5: u1 in M ;
v1 = v by A4, TARSKI:def 1;
hence x in v + M by A3, A5; :: thesis: verum

end;

then {v} + M c= v + M ;
hence {v} + M = v + M by A2; :: thesis: verum