set t1 = the Element of T;
consider s1, s2 being Element of S such that
A1: s1 <> s2 by SUBSET_1:def 7;
per cases ( s1 = the Element of T or s1 <> the Element of T ) ;
suppose s1 = the Element of T ; :: thesis: not DiffElems (S,T) is empty
then [s2, the Element of T] in DiffElems (S,T) by A1;
hence not DiffElems (S,T) is empty ; :: thesis: verum
end;
suppose s1 <> the Element of T ; :: thesis: not DiffElems (S,T) is empty
then [s1, the Element of T] in DiffElems (S,T) ;
hence not DiffElems (S,T) is empty ; :: thesis: verum
end;
end;