defpred S₁[ 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₁[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₁[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