let S be 1-sorted ; :: thesis: for A being ManySortedSet of the carrier of S
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 the carrier of S; :: 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
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 f . mf c=' Z1 )
assume A3: Z1 in F ; :: thesis: f . 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 & f . a = a ) by A1;
mf c=' y1 by A3, Th22, MSSUBFAM:43;
hence f . mf c=' Z1 by A4, Def13; :: thesis: verum

end;

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

end;

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