let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for X, B being Subset of T holds
( X (O) B c= X & X c= X (o) B )
let X, B be Subset of T; :: thesis: ( X (O) B c= X & X c= X (o) B )
thus X (O) B c= X :: thesis: X c= X (o) B

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X (O) B or x in X )
assume x in X (O) B ; :: thesis: x in X
then consider y1, y2 being Point of T such that
A1: x = y1 + y2 and
A2: y1 in X (-) B and
A3: y2 in B ;
consider y being Point of T such that
A4: y1 = y and
A5: B + y c= X by A2;
x in B + y by A1, A3, A4;
hence x in X by A5; :: thesis: verum

end;

thus X c= X (o) B by Th20; :: thesis: verum