let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for X, B being Subset of T st 0. T in B holds
( X (-) B c= X & X c= X (+) B )
let X, B be Subset of T; :: thesis: ( 0. T in B implies ( X (-) B c= X & X c= X (+) B ) )
assume A1: 0. T in B ; :: thesis: ( X (-) B c= X & X c= X (+) B )
thus X (-) B c= X :: thesis: X c= X (+) B

proof

let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in X (-) B or p in X )
assume p in X (-) B ; :: thesis: p in X
then consider p1 being Point of T such that
A2: p = p1 and
A3: B + p1 c= X ;
(0. T) + p1 in { (q + p1) where q is Point of T : q in B } by A1;
then (0. T) + p1 in X by A3;
hence p in X by A2; :: thesis: verum

end;

let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in X or p in X (+) B )
assume A4: p in X ; :: thesis: p in X (+) B
then reconsider p = p as Point of T ;
p + (0. T) in { (x + b) where x, b is Point of T : ( x in X & b in B ) } by A1, A4;
hence p in X (+) B ; :: thesis: verum