theorem Th1: :: TOPREAL8:1

for A, x, y being set st A c= {x,y} & x in A & not y in A holds
A = {x}