let E be non empty addLoopStr ; :: thesis: for A, B, C being Subset of E st B c= C holds

A + B c= A + C

let A, B, C be Subset of E; :: thesis: ( B c= C implies A + B c= A + C )

assume A1: B c= C ; :: thesis: A + B c= A + C

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A + B or x in A + C )

assume x in A + B ; :: thesis: x in A + C

then consider a, b being Element of E such that

A2: ( x = a + b & a in A & b in B ) ;

thus x in A + C by A1, A2; :: thesis: verum

A + B c= A + C

let A, B, C be Subset of E; :: thesis: ( B c= C implies A + B c= A + C )

assume A1: B c= C ; :: thesis: A + B c= A + C

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A + B or x in A + C )

assume x in A + B ; :: thesis: x in A + C

then consider a, b being Element of E such that

A2: ( x = a + b & a in A & b in B ) ;

thus x in A + C by A1, A2; :: thesis: verum