defpred S_{1}[ set ] means ex Y2 being Subset of X st

( Y2 in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } & Y2 c= $1 );

set IT = { Y where Y is Subset of X : S_{1}[Y] } ;

X in F by Th5;

then X /\ Z in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } ;

then Z in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } by XBOOLE_1:28;

then A1: Z in { Y where Y is Subset of X : ex Y2 being Subset of X st

( Y2 in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } & Y2 c= Y ) } ;

{ Y where Y is Subset of X : S_{1}[Y] } is Subset-Family of X
from DOMAIN_1:sch 7();

hence { Y where Y is Subset of X : ex Y2 being Subset of X st

( Y2 in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } & Y2 c= Y ) } is non empty Subset-Family of X by A1; :: thesis: verum

( Y2 in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } & Y2 c= $1 );

set IT = { Y where Y is Subset of X : S

X in F by Th5;

then X /\ Z in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } ;

then Z in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } by XBOOLE_1:28;

then A1: Z in { Y where Y is Subset of X : ex Y2 being Subset of X st

( Y2 in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } & Y2 c= Y ) } ;

{ Y where Y is Subset of X : S

hence { Y where Y is Subset of X : ex Y2 being Subset of X st

( Y2 in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } & Y2 c= Y ) } is non empty Subset-Family of X by A1; :: thesis: verum