let X be non empty addLoopStr ; :: thesis: for M, N being Subset of X
for F being Subset-Family of X st F = { (x + N) where x is Point of X : x in M } holds
M + N = union F
let M, N be Subset of X; :: thesis: for F being Subset-Family of X st F = { (x + N) where x is Point of X : x in M } holds
M + N = union F
let F be Subset-Family of X; :: thesis: ( F = { (x + N) where x is Point of X : x in M } implies M + N = union F )
assume A1: F = { (x + N) where x is Point of X : x in M } ; :: thesis: M + N = union F
thus M + N c= union F :: according to XBOOLE_0:def 10 :: thesis: union F c= M + N

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in M + N or x in union F )
assume x in M + N ; :: thesis: x in union F
then x in { (u + v) where u, v is Point of X : ( u in M & v in N ) } by RUSUB_4:def 9;
then consider u, v being Point of X such that
A2: x = u + v and
A3: u in M and
A4: v in N ;
u + N = { (u + v9) where v9 is Point of X : v9 in N } by RUSUB_4:def 8;
then A5: x in u + N by A2, A4;
u + N in F by A1, A3;
hence x in union F by A5, TARSKI:def 4; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union F or x in M + N )
assume x in union F ; :: thesis: x in M + N
then consider Y being set such that
A6: x in Y and
A7: Y in F by TARSKI:def 4;
consider u being Point of X such that
A8: Y = u + N and
A9: u in M by A1, A7;
u + N = { (u + v) where v is Point of X : v in N } by RUSUB_4:def 8;
then ex v being Point of X st
( x = u + v & v in N ) by A6, A8;
then x in { (u9 + v9) where u9, v9 is Point of X : ( u9 in M & v9 in N ) } by A9;
hence x in M + N by RUSUB_4:def 9; :: thesis: verum