let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for X, B being Subset of T holds (X (-) B) (+) B c= X
let X, B be Subset of T; :: thesis: (X (-) B) (+) B c= X
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (X (-) B) (+) B or x in X )
assume x in (X (-) B) (+) B ; :: thesis: x in X
then consider y1, y2 being Point of T such that
A1: x = y1 + y2 and
A2: y1 in X (-) B and
A3: y2 in B ;
consider y being Point of T such that
A4: y1 = y and
A5: B + y c= X by A2;
x in B + y by A1, A3, A4;
hence x in X by A5; :: thesis: verum