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 ex i being set st
( i in dom F & y in F . i ) by CARD_5:10;
hence y in bool Omega ; :: thesis: verum

end;

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