theorem Lemma8: :: PREFER_1:10

for a, b being set holds
( a <> b iff {[a,b]} misses {[a,a],[b,b]} )