let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; 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; ( B = B (O) B1 implies X (O) B c= X (O) B1 )
assume A1:
B = B (O) B1
; X (O) B c= X (O) B1
let x be object ; TARSKI:def 3 ( not x in X (O) B or x in X (O) B1 )
assume
x in X (O) B
; 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; verum