defpred S₁[ Element of Bool the Sorts of A] means ( C c= $1 & $1 in the Family of A );
{ X where X is Element of Bool the Sorts of A : S₁[X] } is Subset of (Bool the Sorts of A) from DOMAIN_1:sch 7();
then reconsider F = { X where X is Element of Bool the Sorts of A : ( C c= X & X in the Family of A ) } as SubsetFamily of the Sorts of A ;
reconsider IT = meet |:F:| as Element of Bool the Sorts of A by Def1;
take IT ; :: thesis: ex F being SubsetFamily of the Sorts of A st
( IT = meet |:F:| & F = { X where X is Element of Bool the Sorts of A : ( C c=' X & X in the Family of A ) } )
take F ; :: thesis: ( IT = meet |:F:| & F = { X where X is Element of Bool the Sorts of A : ( C c=' X & X in the Family of A ) } )
thus ( IT = meet |:F:| & F = { X where X is Element of Bool the Sorts of A : ( C c=' X & X in the Family of A ) } ) ; :: thesis: verum