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

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