defpred S_{1}[ object ] means ex E being finite Subset of I st $1 in sigUn (F,E);

consider X being set such that

A1: for x being object holds

( x in X iff ( x in bool Omega & S_{1}[x] ) )
from XBOOLE_0:sch 1();

for x being object st x in X holds

x in bool Omega by A1;

then reconsider X = X as Subset-Family of Omega by TARSKI:def 3;

take X ; :: thesis: for S being Subset of Omega holds

( S in X iff ex E being finite Subset of I st S in sigUn (F,E) )

let S be Subset of Omega; :: thesis: ( S in X iff ex E being finite Subset of I st S in sigUn (F,E) )

thus ( S in X iff ex E being finite Subset of I st S in sigUn (F,E) ) by A1; :: thesis: verum

consider X being set such that

A1: for x being object holds

( x in X iff ( x in bool Omega & S

for x being object st x in X holds

x in bool Omega by A1;

then reconsider X = X as Subset-Family of Omega by TARSKI:def 3;

take X ; :: thesis: for S being Subset of Omega holds

( S in X iff ex E being finite Subset of I st S in sigUn (F,E) )

let S be Subset of Omega; :: thesis: ( S in X iff ex E being finite Subset of I st S in sigUn (F,E) )

thus ( S in X iff ex E being finite Subset of I st S in sigUn (F,E) ) by A1; :: thesis: verum