let V be non empty addLoopStr ; :: thesis: for M, N being Subset of V st ( M is empty or N is empty ) holds
M + N is empty
let M, N be Subset of V; :: thesis: ( ( M is empty or N is empty ) implies M + N is empty )
assume A1: ( M is empty or N is empty ) ; :: thesis: M + N is empty
assume not M + N is empty ; :: thesis: contradiction
then consider x being set such that
A2: x in M + N by XBOOLE_0:def 1;
x in { (u + v) where u, v is Element of V : ( u in M & v in N ) } by A2, RUSUB_4:def 10;
then consider u, v being Element of V such that
A3: ( x = u + v & u in M & v in N ) ;
thus contradiction by A1, A3; :: thesis: verum