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 q being Point of T st
( x = q + (0. T) & q in X ) ;
hence x in X ; :: 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 x1 = x as Point of T ;
x1 = x1 + (0. T) ;
hence x in X + (0. T) by A1; :: thesis: verum