theorem Th10: :: HILB10_7:10
for x, y being object
for Y being set st not y in union Y holds
card Y = card (Ext (Y,x,y))