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

proof

let y be object ; :: thesis: ( y in Union F implies y in bool Omega )
assume y in Union F ; :: thesis: y in bool Omega
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: verum

end;

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