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}

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: p + {q} c= {(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;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in p + {q} or x in {(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