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 (+) Y) (O) Y & X (-) Y = (X (-) Y) (o) Y )
let X, Y be Subset of T; :: thesis: ( X (+) Y = (X (+) Y) (O) Y & X (-) Y = (X (-) Y) (o) Y )
(X (+) Y) (O) Y = (X (o) Y) (+) Y ;
hence X (+) Y = (X (+) Y) (O) Y by Th50; :: thesis: X (-) Y = (X (-) Y) (o) Y
(X (-) Y) (o) Y = (X (O) Y) (-) Y ;
hence X (-) Y = (X (-) Y) (o) Y by Th50; :: thesis: verum