let S be non empty addLoopStr ; :: thesis: for v, w being Element of S holds {(v + w)} = v + {w}

let p, q be Element of S; :: thesis: {(p + q)} = p + {q}

assume x in p + {q} ; :: thesis: x in {(p + q)}

then consider v being Element of S such that

A2: x = p + v and

A3: v in {q} ;

v = q by A3, TARSKI:def 1;

hence x in {(p + q)} by A2, TARSKI:def 1; :: thesis: verum

let p, q be Element of S; :: thesis: {(p + q)} = p + {q}

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: p + {q} c= {(p + q)}

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in p + {q} or x in {(p + q)} )let x be object ; :: thesis: ( x in {(p + q)} implies x in p + {q} )

assume x in {(p + q)} ; :: thesis: x in p + {q}

then A1: x = p + q by TARSKI:def 1;

q in {q} by TARSKI:def 1;

hence x in p + {q} by A1; :: thesis: verum

end;assume x in {(p + q)} ; :: thesis: x in p + {q}

then A1: x = p + q by TARSKI:def 1;

q in {q} by TARSKI:def 1;

hence x in p + {q} by A1; :: thesis: verum

assume x in p + {q} ; :: thesis: x in {(p + q)}

then consider v being Element of S such that

A2: x = p + v and

A3: v in {q} ;

v = q by A3, TARSKI:def 1;

hence x in {(p + q)} by A2, TARSKI:def 1; :: thesis: verum