A1: the Sorts of (ClOp->ClSys g) = A by Def23;
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 Def23;
{ 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

proof

let F be SubsetFamily of A; :: according to CLOSURE2:def 8 :: thesis: ( F c= D implies meet |:F:| in D )
assume A2: F c= D ; :: thesis: meet |:F:| in D
reconsider mf = meet |:F:| as Element of Bool A by Def1;

now

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

end;

then A5: g . mf c=' mf by Th25;
mf c=' g . mf by Def12;
then g . mf = mf by A5, PBOOLE:def 13;
hence meet |:F:| in D ; :: thesis: verum

end;

hence ClOp->ClSys g is absolutely-multiplicative by A3; :: thesis: verum