let S be 1-sorted ; :: thesis: for A being ManySortedSet of the carrier of S
for J being reflexive monotonic MSSetOp of A
for D being MSSubsetFamily of A st D = MSFixPoints J holds
MSClosureStr(# A,D #) is MSClosureSystem of S

let A be ManySortedSet of the carrier of S; :: thesis: for J being reflexive monotonic MSSetOp of A
for D being MSSubsetFamily of A st D = MSFixPoints J holds
MSClosureStr(# A,D #) is MSClosureSystem of S

let J be reflexive monotonic MSSetOp of A; :: thesis: for D being MSSubsetFamily of A st D = MSFixPoints J holds
MSClosureStr(# A,D #) is MSClosureSystem of S

let D be MSSubsetFamily of A; :: thesis: ( D = MSFixPoints J implies MSClosureStr(# A,D #) is MSClosureSystem of S )
assume A1: D = MSFixPoints J ; :: thesis: MSClosureStr(# A,D #) is MSClosureSystem of S
D is absolutely-multiplicative
proof
let F be MSSubsetFamily of A; :: according to MSSUBFAM:def 5 :: thesis: ( not F c= D or meet F in D )
assume A2: F c= D ; :: thesis: meet F in D
A3: J .. (meet F) c= meet F
proof
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in the carrier of S or (J .. (meet F)) . i c= (meet F) . i )
assume A4: i in the carrier of S ; :: thesis: (J .. (meet F)) . i c= (meet F) . i
then reconsider j = J . i as Function of ((bool A) . i),((bool A) . i) by PBOOLE:def 15;
A5: i in dom J by ;
consider Q being Subset-Family of (A . i) such that
A6: Q = F . i and
A7: (meet F) . i = Intersect Q by ;
A8: now :: thesis: for x being set st x in Q holds
j . () c= x
let x be set ; :: thesis: ( x in Q implies j . () c= x )
assume A9: x in Q ; :: thesis: j . () c= x
Q c= D . i by A2, A4, A6;
then ex jj being Function st
( jj = J . i & x in dom jj & jj . x = x ) by A1, A4, A9, Def12;
hence j . () c= x by ; :: thesis: verum
end;
(bool A) . i = bool (A . i) by ;
then j . () in bool (A . i) by FUNCT_2:5;
then j . () c= Intersect Q by ;
hence (J .. (meet F)) . i c= (meet F) . i by ; :: thesis: verum
end;
meet F c= A by PBOOLE:def 18;
then A10: meet F in bool A by MBOOLEAN:18;
then meet F is Element of bool A by MSSUBFAM:11;
then meet F c= J .. (meet F) by Def1;
then J .. (meet F) = meet F by ;
hence meet F in D by ; :: thesis: verum
end;
hence MSClosureStr(# A,D #) is MSClosureSystem of S ; :: thesis: verum