let G be addGroup; :: thesis: for A, B, C, D being Subset of G st A c= B & C c= D holds
A + C c= B + D
let A, B, C, D be Subset of G; :: thesis: ( A c= B & C c= D implies A + C c= B + D )
assume that
A1: A c= B and
A2: C c= D ; :: thesis: A + C c= B + D
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A + C or x in B + D )
assume x in A + C ; :: thesis: x in B + D
then ex a, c being Element of G st
( x = a + c & a in A & c in C ) ;
hence x in B + D by A1, A2; :: thesis: verum