let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for X, B, C being Subset of T st C c= B holds
X (O) B c= (X (-) C) (+) B
let X, B, C be Subset of T; :: thesis: ( C c= B implies X (O) B c= (X (-) C) (+) B )
assume A1: C c= B ; :: thesis: X (O) B c= (X (-) C) (+) B
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X (O) B or x in (X (-) C) (+) B )
assume x in X (O) B ; :: thesis: x in (X (-) C) (+) B
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 and
A6: B + x2 c= X by A3;
C + x2 c= B + x2 by A1, Th3;
then C + x2 c= X by A6;
then x1 in X (-) C by A5;
hence x in (X (-) C) (+) B by A2, A4; :: thesis: verum