theorem Th1: :: TEX_2:1
for A being non empty set
for B being 1 -element set st A c= B holds
A = B