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