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 consider y, z being Point of T such that
A1: ( x = y + z & y in X ) and
A2: z in {(0. T)} ;
{z} c= {(0. T)} by A2, ZFMISC_1:31;
then z = 0. T by ZFMISC_1:18;
hence x in X by A1; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in X (+) {(0. T)} )
assume A3: x in X ; :: thesis: x in X (+) {(0. T)}
then reconsider x = x as Point of T ;
0. T in {(0. T)} by TARSKI:def 1;
then x + (0. T) in { (y + z) where y, z is Point of T : ( y in X & z in {(0. T)} ) } by A3;
hence x in X (+) {(0. T)} ; :: thesis: verum