for y being object st y in Union F holds

y in bool Omega

y in bool Omega

proof

hence
Union F is Subset-Family of Omega
by TARSKI:def 3; :: thesis: verum
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;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