let y be object ; :: thesis:
assume y in Union F ; :: thesis:
then consider i being object such that
A1: ( i in dom F & y in F . i ) by CARD_5:2;
reconsider i = i as set by TARSKI:1;
( i in dom F & y in F . i ) by A1;
hence y in bool Omega ; :: thesis:

end;