let V be non empty addLoopStr ; :: thesis: for M being empty Subset of V
for N being Subset of V holds M + N = {}
let M be empty Subset of V; :: thesis: for N being Subset of V holds M + N = {}
let N be Subset of V; :: thesis: M + N = {}

now

let x be Element of V; :: thesis: ( x in M + N implies x in {} )
assume x in M + N ; :: thesis: x in {}
then ex u, v being Element of V st
( x = u + v & u in {} & v in N ) ;
hence x in {} ; :: thesis: verum

end;

then M + N c= {} by SUBSET_1:2;
hence M + N = {} ; :: thesis: verum