A1: the Sorts of (ClOp->ClSys g) = A by Def21;
defpred S₁[ set ] means g . S = S;
set SF = { x where x is Element of Bool A : S₁[x] } ;
A2: { x where x is Element of Bool A : S₁[x] } = the Family of (ClOp->ClSys g) by Def21;
{ 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 ;
A3: ClOp->ClSys g = ClosureStr(# A,D #) by A1, A2;
D is absolutely-multiplicative

let F be SubsetFamily of A; :: according to CLOSURE2:def 7 :: thesis:
assume A4: F c= D ; :: thesis:
reconsider mf = meet |:F:| as Element of Bool A by Def1;

let Z1 be ManySortedSet of the carrier of S; :: thesis:
assume A5: Z1 in F ; :: thesis:
then reconsider y1 = Z1 as Element of Bool A ;
Z1 in D by A4, A5;
then A6: ex a being Element of Bool A st
( Z1 = a & g . a = a ) ;
mf c=' y1 by A5, Th21, MSSUBFAM:43;
hence g . mf c=' Z1 by A6, Def11; :: thesis:

end;

end;