let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for X being Subset of T
for x being Point of T holds X (+) {x} = X + x
let X be Subset of T; :: thesis: for x being Point of T holds X (+) {x} = X + x
let x be Point of T; :: thesis: X (+) {x} = X + x
thus X (+) {x} c= X + x :: according to XBOOLE_0:def 10 :: thesis: X + x c= X (+) {x}
proof
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in X (+) {x} or p in X + x )
assume p in X (+) {x} ; :: thesis: p in X + x
then consider y, z being Point of T such that
A1: p = y + z and
A2: y in X and
A3: z in {x} ;
{z} c= {x} by A3, ZFMISC_1:31;
then p = y + x by A1, ZFMISC_1:18;
hence p in X + x by A2; :: thesis: verum
end;
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in X + x or p in X (+) {x} )
assume p in X + x ; :: thesis: p in X (+) {x}
then A4: ex q being Point of T st
( p = q + x & q in X ) ;
x in {x} by TARSKI:def 1;
hence p in X (+) {x} by A4; :: thesis: verum