theorem Th2: :: CAT_3:2

for I, x being set
for A being non empty set
for a being Element of A st x in I holds
(I --> a) /. x = a