let X be non empty addLoopStr ; :: thesis: for M being Subset of X
for x, y being Point of X st y in M holds
x + y in x + M
let M be Subset of X; :: thesis: for x, y being Point of X st y in M holds
x + y in x + M
let x, y be Point of X; :: thesis: ( y in M implies x + y in x + M )
x + M = { (x + u) where u is Point of X : u in M } by RUSUB_4:def 8;
hence ( y in M implies x + y in x + M ) ; :: thesis: verum