defpred S₁[ set ] means g . $1 = $1;
set SF = { x where x is Element of Bool A : S₁[x] } ;
{ x where x is Element of Bool A : S₁[x] } is Subset of (Bool A) from DOMAIN_1:sch 7();
then reconsider D = { x where x is Element of Bool A : S₁[x] } as SubsetFamily of A ;
take ClosureStr(# A,D #) ; :: thesis: ( the Sorts of ClosureStr(# A,D #) = A & the Family of ClosureStr(# A,D #) = { x where x is Element of Bool A : g . x = x } )
thus ( the Sorts of ClosureStr(# A,D #) = A & the Family of ClosureStr(# A,D #) = { x where x is Element of Bool A : g . x = x } ) ; :: thesis: verum