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 {}

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

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

then
M + N c= {}
;
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;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

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