theorem Th3: :: NUMBER17:3

for a being object
for A being set st <*a*> is A -valued holds
a in A