let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for X, Y being Subset of T
for x, y being Point of T holds
( Y + y c= X + x iff Y + (y - x) c= X )
let X, Y be Subset of T; :: thesis: for x, y being Point of T holds
( Y + y c= X + x iff Y + (y - x) c= X )
let x, y be Point of T; :: thesis: ( Y + y c= X + x iff Y + (y - x) c= X )
thus ( Y + y c= X + x implies Y + (y - x) c= X ) :: thesis: ( Y + (y - x) c= X implies Y + y c= X + x )
proof
assume A1: Y + y c= X + x ; :: thesis: Y + (y - x) c= X
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in Y + (y - x) or p in X )
assume p in Y + (y - x) ; :: thesis: p in X
then consider q1 being Point of T such that
A2: p = q1 + (y - x) and
A3: q1 in Y ;
reconsider p = p as Point of T by A2;
p = (q1 + y) - x by A2, RLVECT_1:28;
then A4: p + x = q1 + y by Lm2;
q1 + y in { (q + y) where q is Point of T : q in Y } by A3;
then p + x in X + x by A1, A4;
then consider p1 being Point of T such that
A5: p + x = p1 + x and
A6: p1 in X ;
(p + x) - x = p1 by A5, Lm2;
hence p in X by A6, Lm2; :: thesis: verum
end;
assume A7: Y + (y - x) c= X ; :: thesis: Y + y c= X + x
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in Y + y or p in X + x )
assume p in Y + y ; :: thesis: p in X + x
then consider q1 being Point of T such that
A8: p = q1 + y and
A9: q1 in Y ;
reconsider p = p as Point of T by A8;
( p - x = q1 + (y - x) & q1 + (y - x) in { (q + (y - x)) where q is Point of T : q in Y } ) by A8, A9, RLVECT_1:28;
then (p - x) + x in { (q + x) where q is Point of T : q in X } by A7;
hence p in X + x by Lm2; :: thesis: verum