set s1 = the Element of S;
consider t1, t2 being Element of T such that
A1: t1 <> t2 by SUBSET_1:def 7;

per cases ( the Element of S = t1 or the Element of S <> t1 ) ;

suppose the Element of S = t1 ; :: thesis: not DiffElems (S,T) is empty

then [ the Element of S,t2] in DiffElems (S,T) by A1;
hence not DiffElems (S,T) is empty ; :: thesis: verum

end;

suppose the Element of S <> t1 ; :: thesis: not DiffElems (S,T) is empty

then [ the Element of S,t1] in DiffElems (S,T) ;
hence not DiffElems (S,T) is empty ; :: thesis: verum

end;

end;