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:24;
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 q being Point of T such that
A8: b1 = - q and
A9: q in B by A7;
xx = x1 - q by A5, A8;
then A10: xx + q = x1 by Lm2;
q + xx in { (q1 + xx) where q1 is Point of T : q1 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:24; :: thesis: verum
end;
hence x in (X (-) B) ` by XBOOLE_0:def 5; :: thesis: verum