let S be 1-sorted ; :: thesis: for A being ManySortedSet of
for f being reflexive monotonic SetOp of A
for D being SubsetFamily of A st D = { x where x is Element of Bool A : f . x = x } holds
ClosureStr(# A,D #) is ClosureSystem of S
let A be ManySortedSet of ; :: thesis: for f being reflexive monotonic SetOp of A
for D being SubsetFamily of A st D = { x where x is Element of Bool A : f . x = x } holds
ClosureStr(# A,D #) is ClosureSystem of S
let f be reflexive monotonic SetOp of A; :: thesis: for D being SubsetFamily of A st D = { x where x is Element of Bool A : f . x = x } holds
ClosureStr(# A,D #) is ClosureSystem of S
let D be SubsetFamily of A; :: thesis: ( D = { x where x is Element of Bool A : f . x = x } implies ClosureStr(# A,D #) is ClosureSystem of S )
assume A1: D = { x where x is Element of Bool A : f . x = x } ; :: thesis: ClosureStr(# A,D #) is ClosureSystem of S
reconsider cs = ClosureStr(# A,D #) as ClosureStr of S ;
cs is absolutely-multiplicative

proof

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;
f . mf = mf

proof

now

let Z1 be ManySortedSet of ; :: thesis: ( Z1 in F implies f . mf c=' Z1 )
assume A3: Z1 in F ; :: thesis: f . mf c=' Z1
then Z1 in D by A2;
then consider a being Element of Bool A such that
A4: ( Z1 = a & f . a = a ) by A1;
reconsider y1 = Z1 as Element of Bool A by A3;
mf c=' y1 by A3, Th22, MSSUBFAM:43;
hence f . mf c=' Z1 by A4, Def13; :: thesis: verum

end;

hence f . mf c=' mf by Th25; :: according to PBOOLE:def 13 :: thesis: mf c=' f . mf
thus mf c=' f . mf by Def12; :: thesis: verum

end;

hence meet |:F:| in D by A1; :: thesis: verum

end;

hence the Family of cs is absolutely-multiplicative ; :: according to CLOSURE2:def 19 :: thesis: verum

end;

hence ClosureStr(# A,D #) is ClosureSystem of S ; :: thesis: verum