let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for X, B, B1 being Subset of T st B = B (O) B1 holds
X (O) B c= X (O) B1
let X, B, B1 be Subset of T; :: thesis: ( B = B (O) B1 implies X (O) B c= X (O) B1 )
assume A1: B = B (O) B1 ; :: thesis: X (O) B c= X (O) B1
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X (O) B or x in X (O) B1 )
assume x in X (O) B ; :: thesis: x in X (O) B1
then consider x1, b1 being Point of T such that
A2: x = x1 + b1 and
A3: x1 in X (-) B and
A4: b1 in B ;
consider x2 being Point of T such that
A5: ( x1 = x2 & B + x2 c= X ) by A3;
consider x3, b2 being Point of T such that
A6: b1 = x3 + b2 and
A7: x3 in B (-) B1 and
A8: b2 in B1 by A1, A4;
consider x4 being Point of T such that
A9: x3 = x4 and
A10: B1 + x4 c= B by A7;
(B1 + x4) + x2 c= B + x2 by A10, Th3;
then (B1 + x3) + x1 c= X by A5, A9;
then B1 + (x3 + x1) c= X by Th16;
then x1 + x3 in X (-) B1 ;
then (x1 + x3) + b2 in (X (-) B1) (+) B1 by A8;
hence x in X (O) B1 by A2, A6, RLVECT_1:def 3; :: thesis: verum