let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for X, Y, Z being Subset of T holds X (+) (Y (-) Z) c= (X (+) Y) (-) Z
let X, Y, Z be Subset of T; :: thesis: X (+) (Y (-) Z) c= (X (+) Y) (-) Z
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X (+) (Y (-) Z) or x in (X (+) Y) (-) Z )
assume x in X (+) (Y (-) Z) ; :: thesis: x in (X (+) Y) (-) Z
then consider a, b being Point of T such that
A1: x = a + b and
A2: a in X and
A3: b in Y (-) Z ;
ex c being Point of T st
( b = c & Z + c c= Y ) by A3;
then (Z + b) + a c= Y + a by Th3;
then A4: Z + (b + a) c= Y + a by Th16;
Y + a c= Y (+) X by A2, Th19;
then Z + (b + a) c= Y (+) X by A4;
then x in (Y (+) X) (-) Z by A1;
hence x in (X (+) Y) (-) Z by Th12; :: thesis: verum