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 y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in X (-) {x} or y in X + (- x) )
assume y in X (-) {x} ; :: thesis: y in X + (- x)
then consider p being Point of T such that
A1: p = y and
A2: {x} + p c= X ;
{p} + x c= X by A2, Lm1;
then ({p} + x) + (- x) c= X + (- x) by Th3;
then {p} + (x + (- x)) c= X + (- x) by Th16;
then {p} + (0. T) c= X + (- x) by RLVECT_1:5;
then {p} c= X + (- x) by Th21;
hence y in X + (- x) by A1, ZFMISC_1:31; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in X + (- x) or y in X (-) {x} )
assume y in X + (- x) ; :: thesis: y in X (-) {x}
then consider p being Point of T such that
A3: y = p + (- x) and
A4: p in X ;
reconsider y = y as Point of T by A3;
y = p - x by A3;
then A5: y + x = p by Lm2;
{x} + y c= X
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in {x} + y or q in X )
assume q in {x} + y ; :: thesis: q in X
then consider qq being Point of T such that
A6: q = qq + y and
A7: qq in {x} ;
{qq} c= {x} by A7, ZFMISC_1:31;
hence q in X by A4, A5, A6, ZFMISC_1:18; :: thesis: verum
end;
hence y in X (-) {x} ; :: thesis: verum