theorem Th1: :: POLYFORM:1

for X being set
for c, d being object st ex a, b being object st
( a <> b & X = {a,b} ) & c in X & d in X & c <> d holds
X = {c,d}