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

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

hence
MSClosureStr(# A,D #) is MSClosureSystem of S
; :: thesis: verum
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

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;assume A2: F c= D ; :: thesis: meet F in D

A3: J .. (meet F) c= meet F

proof

meet F c= A
by PBOOLE:def 18;
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;

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;

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, A5, PRALG_1:def 17; :: thesis: verum

end;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;

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

(bool A) . i = bool (A . i)
by A4, MBOOLEAN:def 1;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;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

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, A5, PRALG_1:def 17; :: thesis: verum

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