theorem Th17: :: HILB10_7:17

for x, y being object
for X, Y being set st Y in Ext (X,x,y) & not y in union X holds
( x in Y iff y in Y )