let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for X, Y being Subset of T holds
( X (+) Y = (X (o) Y) (+) Y & X (-) Y = (X (O) Y) (-) Y )
let X, Y be Subset of T; :: thesis: ( X (+) Y = (X (o) Y) (+) Y & X (-) Y = (X (O) Y) (-) Y )
(X (o) Y) (+) Y = (X (+) Y) (O) Y ;
then A1: (X (o) Y) (+) Y c= X (+) Y by Th41;
X c= X (o) Y by Th41;
then X (+) Y c= (X (o) Y) (+) Y by Th9;
hence X (+) Y = (X (o) Y) (+) Y by A1; :: thesis: X (-) Y = (X (O) Y) (-) Y
(X (O) Y) (-) Y = (X (-) Y) (o) Y ;
hence X (-) Y c= (X (O) Y) (-) Y by Th41; :: according to XBOOLE_0:def 10 :: thesis: (X (O) Y) (-) Y c= X (-) Y
X (O) Y c= X by Th41;
hence (X (O) Y) (-) Y c= X (-) Y by Th9; :: thesis: verum