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 = {}
A1: M + N = { (u + v) where u, v is Element of V : ( u in {} & v in N ) } by RUSUB_4:def 9;
for x being Element of V st x in M + N holds
x in {}

proof

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 ) by A1;
hence x in {} ; :: thesis: verum

end;

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