theorem Th88: :: HILB10_7:88

for X being set
for F being finite set
for E being Enumeration of F st X misses union F holds
ex Ex being Enumeration of UNION (F,{X}) st
for i being Nat st i in dom E holds
Ex . i = X \/ (E . i)