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 ;
reconsider a = ClosureStr(# A,D #) as strict ClosureSystem of S by Th39;
take a ; :: thesis: ( the Sorts of a = A & the Family of a = { x where x is Element of Bool A : g . x = x } )
thus ( the Sorts of a = A & the Family of a = { x where x is Element of Bool A : g . x = x } ) ; :: thesis: verum