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