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

consider X being set such that

A1: for x being set holds

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

A2: not X is empty

x in bool (bool Omega) by A1;

then reconsider X = X as non empty Subset-Family of (bool Omega) by A2, TARSKI:def 3;

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

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

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

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

consider X being set such that

A1: for x being set holds

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

A2: not X is empty

proof end;

for x being object st x in X holds x in bool (bool Omega) by A1;

then reconsider X = X as non empty Subset-Family of (bool Omega) by A2, TARSKI:def 3;

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

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

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

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