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 object such that
A2: x in M - N ;
ex u, v being Element of V st
( x = u - v & u in M & v in N ) by A2;
hence contradiction by A1; :: thesis: verum