defpred S_{1}[ set ] means ex E being non empty finite Subset of I ex f being SigmaSection of E,F st

( E c= J & $1 = meet (rng f) );

consider X being set such that

A1: for x being set holds

( x in X iff ( x in bool Omega & S_{1}[x] ) )
from XFAMILY: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 x being Subset of Omega holds

( x in X iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st

( E c= J & x = meet (rng f) ) )

let x be Subset of Omega; :: thesis: ( x in X iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st

( E c= J & x = meet (rng f) ) )

thus ( x in X iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st

( E c= J & x = meet (rng f) ) ) by A1; :: thesis: verum

( E c= J & $1 = meet (rng f) );

consider X being set such that

A1: for x being set 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 x being Subset of Omega holds

( x in X iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st

( E c= J & x = meet (rng f) ) )

let x be Subset of Omega; :: thesis: ( x in X iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st

( E c= J & x = meet (rng f) ) )

thus ( x in X iff ex E being non empty finite Subset of I ex f being SigmaSection of E,F st

( E c= J & x = meet (rng f) ) ) by A1; :: thesis: verum