let V be non empty addLoopStr ; :: thesis: for M, N being non empty Subset of V holds not M + N is empty
let M, N be non empty Subset of V; :: thesis: not M + N is empty
consider x being object such that
A1: x in M by XBOOLE_0:def 1;
consider y being object such that
A2: y in N by XBOOLE_0:def 1;
reconsider x = x, y = y as Element of V by A1, A2;
x + y in { (u + v) where u, v is Element of V : ( u in M & v in N ) } by A1, A2;
hence not M + N is empty by RUSUB_4:def 9; :: thesis: verum