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

proof

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

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X (o) B or x in Y (o) B )
assume x in X (o) B ; :: thesis: x in Y (o) B
then consider x2 being Point of T such that
A7: x = x2 and
A8: B + x2 c= X (+) B ;
X (+) B c= Y (+) B by A1, Th9;
then B + x2 c= Y (+) B by A8;
hence x in Y (o) B by A7; :: thesis: verum