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 A4, PARTFUN1:def 2;
i in dom (meet F) by A4, PARTFUN1:def 2;
then i in (dom J) /\ (dom (meet F)) by A5, XBOOLE_0:def 4;
then a5: i in dom (J .. (meet F)) by PRALG_1:def 19;
consider Q being Subset-Family of (A . i) such that
A6: Q = F . i and
A7: (meet F) . i = Intersect Q by A4, MSSUBFAM:def 1;

A8: now :: thesis: for x being set st x in Q holds
j . (Intersect Q) c= x

let x be set ; :: thesis: ( x in Q implies j . (Intersect Q) c= x )
assume A9: x in Q ; :: thesis: j . (Intersect Q) 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 . (Intersect Q) c= x by A4, A9, Th25, MSSUBFAM:2; :: thesis: verum

end;

(bool A) . i = bool (A . i) by A4, MBOOLEAN:def 1;
then j . (Intersect Q) in bool (A . i) by FUNCT_2:5;
then j . (Intersect Q) c= Intersect Q by A8, MSSUBFAM:4;
hence (J .. (meet F)) . i c= (meet F) . i by A7, PRALG_1:def 19, a5; :: 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 A3, PBOOLE:146;
hence meet F in D by A1, A10, Th28; :: thesis: verum

end;

hence MSClosureStr(# A,D #) is MSClosureSystem of S ; :: thesis: verum