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