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 (-) Z) (-) Y
let X, Y, Z be Subset of T; :: thesis: X (-) (Y (+) Z) = (X (-) Z) (-) Y
X (-) (Y (+) Z) = X (-) (Z (+) Y) by Th12
.= (X (-) Z) (-) Y by Th23 ;
hence X (-) (Y (+) Z) = (X (-) Z) (-) Y ; :: thesis: verum