theorem Th1: :: RELSET_2:1

for y being object
for X being set holds
( y in {_{X}_} iff ex x being object st
( y = {x} & x in X ) )