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) = (X (-) Y) (-) Z
let X, Y, Z be Subset of T; :: thesis: X (-) (Y (+) Z) = (X (-) Y) (-) Z
A1: (X (-) Y) (+) Y c= X by Lm3;
thus X (-) (Y (+) Z) c= (X (-) Y) (-) Z :: according to XBOOLE_0:def 10 :: thesis: (X (-) Y) (-) Z c= X (-) (Y (+) Z)
proof
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in X (-) (Y (+) Z) or p in (X (-) Y) (-) Z )
assume p in X (-) (Y (+) Z) ; :: thesis: p in (X (-) Y) (-) Z
then consider x being Point of T such that
A2: p = x and
A3: (Y (+) Z) + x c= X ;
(Y + x) (+) Z c= X by A3, Th15;
then Z (+) (Y + x) c= X by Th12;
then A4: (Z (+) (Y + x)) (-) (Y + x) c= X (-) (Y + x) by Th9;
Z c= (Z (+) (Y + x)) (-) (Y + x) by Th20;
then Z c= X (-) (Y + x) by A4;
then Z c= (X (-) Y) + (- x) by Th17;
then Z + x c= ((X (-) Y) + (- x)) + x by Th3;
then Z + x c= (X (-) Y) + ((- x) + x) by Th16;
then Z + x c= (X (-) Y) + (x - x) ;
then Z + x c= (X (-) Y) + (0. T) by RLVECT_1:15;
then Z + x c= X (-) Y by Th21;
hence p in (X (-) Y) (-) Z by A2; :: thesis: verum
end;
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in (X (-) Y) (-) Z or p in X (-) (Y (+) Z) )
assume p in (X (-) Y) (-) Z ; :: thesis: p in X (-) (Y (+) Z)
then consider y being Point of T such that
A5: p = y and
A6: Z + y c= X (-) Y ;
(Z + y) (+) Y c= (X (-) Y) (+) Y by A6, Th9;
then (Z + y) (+) Y c= X by A1;
then (Z (+) Y) + y c= X by Th15;
then p in X (-) (Z (+) Y) by A5;
hence p in X (-) (Y (+) Z) by Th12; :: thesis: verum