theorem Th18: :: FUNCT_7:18

for A being set
for x being object holds
( <*x*> in A * iff x in A )