defpred S1[ set ] means $1 is Filter of X;
{X} is Filter of X
by Th4;
then A1:
{X} in { S where S is Subset-Family of X : S is Filter of X }
;
{ S where S is Subset-Family of X : S1[S] } is Subset-Family of (bool X)
from DOMAIN_1:sch 7();
hence
{ S where S is Subset-Family of X : S is Filter of X } is non empty Subset-Family of (bool X)
by A1; verum