theorem Th29: :: HILB10_7:29

for x, y being object
for X being set st x in X holds
Ext ({X},x,y) = {(X \/ {y})}