let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for X, B, C being Subset of T st B c= C holds
X (o) B c= (X (+) C) (-) B
let X, B, C be Subset of T; :: thesis: ( B c= C implies X (o) B c= (X (+) C) (-) B )
assume B c= C ; :: thesis: X (o) B c= (X (+) C) (-) B
then A1: X (+) B c= X (+) C by Th10;
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 x2 being Point of T such that
A2: x = x2 and
A3: B + x2 c= X (+) B ;
B + x2 c= X (+) C by A3, A1;
hence x in (X (+) C) (-) B by A2; :: thesis: verum