theorem Lemma3: :: PREFER_1:3

for A being 2 -element set
for a, b being Element of A st a <> b holds
A = {a,b}