let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for X being Subset of T holds X (-) {(0. T)} = X
let X be Subset of T; :: thesis: X (-) {(0. T)} = X
thus X (-) {(0. T)} c= X :: according to XBOOLE_0:def 10 :: thesis: X c= X (-) {(0. T)}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X (-) {(0. T)} or x in X )
assume x in X (-) {(0. T)} ; :: thesis: x in X
then ex y being Point of T st
( x = y & {(0. T)} + y c= X ) ;
then {x} c= X by Th2;
hence x in X by ZFMISC_1:31; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in X (-) {(0. T)} )
assume A1: x in X ; :: thesis: x in X (-) {(0. T)}
then reconsider xx = x as Point of T ;
{x} c= X by A1, ZFMISC_1:31;
then {(0. T)} + xx c= X by Th2;
hence x in X (-) {(0. T)} ; :: thesis: verum