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

for x being object st x in {v} + M holds

x in v + M

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

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

then A2:
v + M c= {v} + M
;
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;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

for x being object st x in {v} + M holds

x in v + M

proof

then
{v} + M c= v + M
;
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;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

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