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

proof

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

now :: thesis: for Z1 being ManySortedSet of the carrier of S st Z1 in F holds
g . mf c=' Z1

let Z1 be ManySortedSet of the carrier of S; :: thesis: ( Z1 in F implies g . mf c=' Z1 )
assume A5: Z1 in F ; :: thesis: g . mf c=' Z1
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: verum

end;

then A7: g . mf c=' mf by Th24;
mf c=' g . mf by Def10;
then g . mf = mf by A7, PBOOLE:146;
hence meet |:F:| in D ; :: thesis: verum

end;

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