consider s1, s2 being Element of S such that
A1: s1 <> s2 by YELLOW_8:def 1;
consider t1 being Element of T;

per cases ( s1 = t1 or s1 <> t1 ) ;

suppose s1 = t1 ; :: thesis: not DiffElems S,T is empty

then [s2,t1] in DiffElems S,T by A1;
hence not DiffElems S,T is empty ; :: thesis: verum

end;

suppose s1 <> t1 ; :: thesis: not DiffElems S,T is empty

then [s1,t1] in DiffElems S,T ;
hence not DiffElems S,T is empty ; :: thesis: verum

end;

end;