let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for X, B being Subset of T holds ((X `) (-) B) ` = X (+) (B !)
let X, B be Subset of T; :: thesis: ((X `) (-) B) ` = X (+) (B !)
thus ((X `) (-) B) ` c= X (+) (B !) :: according to XBOOLE_0:def 10 :: thesis: X (+) (B !) c= ((X `) (-) B) `

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ((X `) (-) B) ` or x in X (+) (B !) )
assume A1: x in ((X `) (-) B) ` ; :: thesis: x in X (+) (B !)
then reconsider x1 = x as Point of T ;
not x in (X `) (-) B by A1, XBOOLE_0:def 5;
then not B + x1 c= X ` ;
then B + x1 meets X by SUBSET_1:23;
then consider y being object such that
A2: y in B + x1 and
A3: y in X by XBOOLE_0:3;
reconsider y1 = y as Point of T by A2;
consider b1 being Point of T such that
A4: ( y = b1 + x1 & b1 in B ) by A2;
( x1 = y1 - b1 & - b1 in B ! ) by A4, Lm2;
hence x in X (+) (B !) by A3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X (+) (B !) or x in ((X `) (-) B) ` )
assume x in X (+) (B !) ; :: thesis: x in ((X `) (-) B) `
then consider x1, b1 being Point of T such that
A5: x = x1 + b1 and
A6: x1 in X and
A7: b1 in B ! ;
reconsider xx = x as Point of T by A5;
consider b2 being Point of T such that
A8: b1 = - b2 and
A9: b2 in B by A7;
x = x1 - b2 by A5, A8;
then A10: xx + b2 = x1 by Lm2;
b2 + xx in { (pb + xx) where pb is Point of T : pb in B } by A9;
then A11: B + xx meets X by A6, A10, XBOOLE_0:3;
not xx in (X `) (-) B

proof

assume xx in (X `) (-) B ; :: thesis: contradiction
then ex yy being Point of T st
( xx = yy & B + yy c= X ` ) ;
hence contradiction by A11, SUBSET_1:23; :: thesis: verum

end;

hence x in ((X `) (-) B) ` by XBOOLE_0:def 5; :: thesis: verum