defpred S_{1}[ 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 : S_{1}[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; :: thesis: verum

{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 : S

hence { S where S is Subset-Family of X : S is Filter of X } is non empty Subset-Family of (bool X) by A1; :: thesis: verum