for y being set st y in Union F holds
y in bool Omega

proof

let y be set ; :: thesis: ( y in Union F implies y in bool Omega )
assume y in Union F ; :: thesis: y in bool Omega
then consider i being set such that
A0: ( i in dom F & y in F . i ) by CARD_5:10;
thus y in bool Omega by A0; :: thesis: verum

end;

hence Union F is Subset-Family of Omega by TARSKI:def 3; :: thesis: verum