theorem Th30: :: HILB10_7:30

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