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

now

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

end;

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