:: On the Closure Operator and the Closure System of Many Sorted Sets :: by Artur Korni{\l}owicz :: :: Received February 7, 1996 :: Copyright (c) 1996-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies PBOOLE, FUNCT_1, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, ZFMISC_1, FUNCT_2, CARD_3, FINSET_1, COMPLEX1, SETFAM_1, FUNCT_4, MSSUBFAM, FUNCOP_1, RELAT_2, MSAFREE2, BINOP_1, YELLOW_6, STRUCT_0, MSUALG_1, PRE_TOPC, CLOSURE2, SETLIM_2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, SETFAM_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, FINSET_1, FUNCT_4, PBOOLE, CARD_3, MSUALG_1, MBOOLEAN, MSSUBFAM; constructors SETFAM_1, FUNCT_4, MSSUBFAM, MSUALG_1, CARD_3, RELSET_1; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, FINSET_1, PBOOLE, MSUALG_1; requirements SUBSET, BOOLE; definitions XBOOLE_0, FUNCT_1, MSUALG_1, PBOOLE, CARD_3, TARSKI; equalities FUNCOP_1; expansions XBOOLE_0, FUNCT_1, MSUALG_1, PBOOLE, TARSKI; theorems FUNCOP_1, ENUMSET1, FUNCT_1, FUNCT_2, FUNCT_4, MBOOLEAN, PBOOLE, PZFMISC1, SETFAM_1, TARSKI, MSSUBFAM, ZFMISC_1, XBOOLE_0, XBOOLE_1, PARTFUN1, RELAT_1; schemes FRAENKEL, FUNCT_1, FUNCT_2, DOMAIN_1, XBOOLE_0; begin :: Preliminaries reserve i, x, I for set, A, B, M for ManySortedSet of I, f, f1 for Function; notation let I, A, B; synonym A in' B for A in B; end; notation let I, A, B; synonym A c=' B for A c= B; end; theorem for M being non empty set for X, Y being Element of M st X c= Y holds (id M).X c= (id M).Y; theorem Th2: for I being non empty set for A being ManySortedSet of I for B being ManySortedSubset of A holds rng B c= union rng bool A proof let I be non empty set, A be ManySortedSet of I, B be ManySortedSubset of A; let a be object; assume a in rng B; then consider i being object such that A1: i in I and A2: a = B.i by PBOOLE:138; i in dom bool A & bool (A.i) = (bool A).i by A1,MBOOLEAN:def 1,PARTFUN1:def 2 ; then A3: bool (A.i) in rng bool A by FUNCT_1:def 3; B c= A by PBOOLE:def 18; then B in bool A by MBOOLEAN:18; then B.i in (bool A).i by A1; then a in bool (A.i) by A1,A2,MBOOLEAN:def 1; hence thesis by A3,TARSKI:def 4; end; begin :: Set of Many Sorted Subsets of a Many Sorted Set definition let I, M; defpred f[object] means $1 is ManySortedSubset of M; func Bool M -> set means :Def1: for x being object holds x in it iff x is ManySortedSubset of M; existence proof per cases; suppose A1: I is non empty; consider X being set such that A2: for e being object holds e in X iff e in Funcs(I, union rng bool M) & f[e] from XBOOLE_0:sch 1; take X; let x be object; thus x in X implies x is ManySortedSubset of M by A2; assume A3: x is ManySortedSubset of M; now reconsider xx = x as ManySortedSubset of M by A3; dom xx = I & rng xx c= union rng bool M by A1,Th2,PARTFUN1:def 2; hence x in Funcs(I, union rng bool M) by FUNCT_2:def 2; thus f[ x ] by A3; end; hence thesis by A2; end; suppose A4: I is empty; take {EmptyMS {}}; let x be object; thus x in {EmptyMS {}} implies x is ManySortedSubset of M proof reconsider M9 = M as ManySortedSet of {} by A4; assume A5: x in {EmptyMS {}}; reconsider y = EmptyMS {} as ManySortedSubset of M9 by PBOOLE:def 18; y is ManySortedSubset of M by A4; hence thesis by A5,TARSKI:def 1; end; assume x is ManySortedSubset of M; then consider y being ManySortedSubset of M such that A6: y = x; y = EmptyMS {} by A4; hence thesis by A6,TARSKI:def 1; end; end; uniqueness proof thus for X1,X2 being set st (for x being object holds x in X1 iff f[ x ]) & ( for x being object holds x in X2 iff f[ x ]) holds X1 = X2 from XBOOLE_0:sch 3; end; end; registration let I, M; cluster Bool M -> non empty functional with_common_domain; coherence proof M is ManySortedSubset of M by PBOOLE:def 18; hence Bool M is non empty by Def1; thus Bool M is functional by Def1; let f, g be Function; assume that A1: f in Bool M and A2: g in Bool M; A3: g is ManySortedSubset of M by A2,Def1; f is ManySortedSubset of M by A1,Def1; hence dom f = I by PARTFUN1:def 2 .= dom g by A3,PARTFUN1:def 2; end; end; definition let I, M; mode SubsetFamily of M is Subset of Bool M; end; definition let I, M; redefine func Bool M -> SubsetFamily of M; coherence proof Bool M c= Bool M; hence thesis; end; end; registration let I, M; cluster non empty functional with_common_domain for SubsetFamily of M; existence proof take Bool M; thus thesis; end; end; registration let I, M; cluster empty finite for SubsetFamily of M; existence proof reconsider x = {} as SubsetFamily of M by XBOOLE_1:2; take x; thus thesis; end; end; reserve SF, SG for SubsetFamily of M; definition let I, M; let S be non empty SubsetFamily of M; redefine mode Element of S -> ManySortedSubset of M; coherence proof let e be Element of S; thus thesis by Def1; end; end; theorem Th3: :: MSSUBFAM:34 SF \/ SG is SubsetFamily of M; theorem :: MSSUBFAM:35 SF /\ SG is SubsetFamily of M; theorem :: MSSUBFAM:36 SF \ x is SubsetFamily of M; theorem :: MSSUBFAM:37 SF \+\ SG is SubsetFamily of M; theorem Th7: :: MSSUBFAM:38 A c= M implies {A} is SubsetFamily of M proof assume A c= M; then A is ManySortedSubset of M by PBOOLE:def 18; then A in Bool M by Def1; hence thesis by ZFMISC_1:31; end; theorem Th8: :: MSSUBFAM:39 A c= M & B c= M implies {A,B} is SubsetFamily of M proof assume A c= M & B c= M; then {A} is SubsetFamily of M & {B} is SubsetFamily of M by Th7; then {A} \/ {B} is SubsetFamily of M by Th3; hence thesis by ENUMSET1:1; end; reserve E, T for Element of Bool M; theorem Th9: E (/\) T in Bool M proof E c= M & T c= M by PBOOLE:def 18; then E (/\) T c= M (/\) M by PBOOLE:21; then E (/\) T is ManySortedSubset of M by PBOOLE:def 18; hence thesis by Def1; end; theorem Th10: E (\/) T in Bool M proof E c= M & T c= M by PBOOLE:def 18; then E (\/) T c= M (\/) M by PBOOLE:20; then E (\/) T is ManySortedSubset of M by PBOOLE:def 18; hence thesis by Def1; end; theorem E (\) A in Bool M proof E c= M by PBOOLE:def 18; then E (\) A c= M by MBOOLEAN:15; then E (\) A is ManySortedSubset of M by PBOOLE:def 18; hence thesis by Def1; end; theorem E (\+\) T in Bool M proof T c= M by PBOOLE:def 18; then A1: T (\) E c= M by MBOOLEAN:15; E c= M by PBOOLE:def 18; then E (\) T c= M by MBOOLEAN:15; then E (\+\) T c= M by A1,PBOOLE:91; then E (\+\) T is ManySortedSubset of M by PBOOLE:def 18; hence thesis by Def1; end; begin :: Many Sorted Operator corresponding :: to the Operator on Many Sorted Subsets definition let S be functional set; func |. S .| -> Function means :Def2: ex A being non empty functional set st A = S & dom it = meet the set of all dom x where x is Element of A & for i st i in dom it holds it.i = the set of all x.i where x is Element of A if S <> {} otherwise it = {}; existence proof thus S <> {} implies ex f being Function st ex A being non empty functional set st A = S & dom f = meet the set of all dom x where x is Element of A & for i st i in dom f holds f.i = the set of all x.i where x is Element of A proof assume S <> {}; then consider A being non empty functional set such that A1: A = S; deffunc F(object) = the set of all x.$1 where x is Element of A ; consider f being Function such that A2: dom f = meet the set of all dom x where x is Element of A & for i being object st i in meet the set of all dom x where x is Element of A holds f.i = F (i) from FUNCT_1:sch 3; take f, A; thus thesis by A1,A2; end; thus thesis; end; uniqueness proof let f, g be Function; defpred P[Function] means ex A being non empty functional set st A = S & dom $1 = meet the set of all dom x where x is Element of A & for i st i in dom $1 holds $1.i = the set of all x.i where x is Element of A ; thus S <> {} & P[f] & P[g] implies f = g proof assume that S <> {} and A3: P[f] and A4: P[g]; consider A being non empty functional set such that A5: A = S and A6: dom f = meet the set of all dom x where x is Element of A and A7: for i st i in dom f holds f.i = the set of all x.i where x is Element of A by A3; now let a be object; assume A8: a in meet the set of all dom x where x is Element of A ; hence f.a = the set of all x.a where x is Element of A by A6 ,A7 .= g.a by A4,A5,A8; end; hence thesis by A4,A5,A6; end; thus thesis; end; consistency; end; theorem Th13: for SF being non empty SubsetFamily of M holds dom |.SF.| = I proof let SF be non empty SubsetFamily of M; consider A being non empty functional set such that A1: A = SF and A2: dom |.SF.| = meet the set of all dom x where x is Element of A and for i st i in dom |.SF.| holds |.SF.|.i = the set of all x.i where x is Element of A by Def2; the set of all dom x where x is Element of A = {I} proof thus the set of all dom x where x is Element of A c= {I} proof let a be object; assume a in the set of all dom x where x is Element of A ; then consider x being Element of A such that A3: a = dom x; x is Element of SF by A1; then a = I by A3,PARTFUN1:def 2; hence thesis by TARSKI:def 1; end; set x = the Element of A; let a be object; assume a in {I}; then A4: a = I by TARSKI:def 1; x is Element of SF by A1; then dom x = I by PARTFUN1:def 2; hence thesis by A4; end; hence thesis by A2,SETFAM_1:10; end; registration let S be empty functional set; cluster |. S .| -> empty; coherence by Def2; end; definition let I, M; let S be SubsetFamily of M; func |: S :| -> ManySortedSet of I equals :Def3: |. S .| if S <> {} otherwise EmptyMS I; coherence proof thus S <> {} implies |.S.| is ManySortedSet of I proof assume S <> {}; then dom |.S.| = I by Th13; hence thesis by PARTFUN1:def 2,RELAT_1:def 18; end; thus thesis; end; consistency; end; registration let I, M; let S be empty SubsetFamily of M; cluster |: S :| -> empty-yielding; coherence proof |:S:| = EmptyMS I by Def3; hence thesis; end; end; theorem Th14: SF is non empty implies for i st i in I holds |:SF:|.i = { x.i where x is Element of Bool M : x in SF } proof A1: dom |:SF:| = I by PARTFUN1:def 2; assume A2: SF is non empty; then consider A being non empty functional set such that A3: A = SF and dom |.SF.| = meet the set of all dom x where x is Element of A and A4: for i st i in dom |.SF.| holds |.SF.|.i = the set of all x.i where x is Element of A by Def2; let i such that A5: i in I; set K = { x.i where x is Element of Bool M : x in SF }, N = the set of all x.i where x is Element of A ; A6: K = N proof thus K c= N proof let q be object; assume q in K; then ex x being Element of Bool M st q = x.i & x in SF; hence thesis by A3; end; let q be object; assume q in N; then consider x being Element of A such that A7: q = x.i; x in SF by A3; hence thesis by A7; end; |:SF:| = |.SF.| by A2,Def3; hence thesis by A4,A5,A1,A6; end; registration let I, M; let SF be non empty SubsetFamily of M; cluster |: SF :| -> non-empty; coherence proof let i be object; assume i in I; then A1: |:SF:|.i = { x.i where x is Element of Bool M : x in SF} by Th14; consider x being object such that A2: x in SF by XBOOLE_0:def 1; reconsider x as Element of Bool M by A2; x.i in |:SF:|.i by A1,A2; hence thesis; end; end; theorem Th15: dom |.{f}.| = dom f proof consider A being non empty functional set such that A1: A = {f} and A2: dom |.{f}.| = meet the set of all dom x where x is Element of A and for i st i in dom |.{f}.| holds |.{f}.|.i = the set of all x.i where x is Element of A by Def2; set m = the set of all dom x where x is Element of A ; m = {dom f} proof thus m c= {dom f} proof let q be object; assume q in m; then consider x being Element of A such that A3: q = dom x; x = f by A1,TARSKI:def 1; hence thesis by A3,TARSKI:def 1; end; let q be object; assume q in {dom f}; then A4: q = dom f by TARSKI:def 1; f is Element of A by A1,TARSKI:def 1; hence thesis by A4; end; hence thesis by A2,SETFAM_1:10; end; theorem dom |.{f,f1}.| = dom f /\ dom f1 proof consider A being non empty functional set such that A1: A = {f,f1} and A2: dom |.{f,f1}.| = meet the set of all dom x where x is Element of A and for i st i in dom |.{f,f1}.| holds |.{f,f1}.|.i = the set of all x.i where x is Element of A by Def2; set m = the set of all dom x where x is Element of A ; m = {dom f, dom f1} proof thus m c= {dom f, dom f1} proof let q be object; assume q in m; then consider x being Element of A such that A3: q = dom x; x = f or x = f1 by A1,TARSKI:def 2; hence thesis by A3,TARSKI:def 2; end; let q be object; assume q in {dom f, dom f1}; then A4: q = dom f or q = dom f1 by TARSKI:def 2; f is Element of A & f1 is Element of A by A1,TARSKI:def 2; hence thesis by A4; end; hence thesis by A2,SETFAM_1:11; end; theorem Th17: i in dom f implies |.{f}.|.i = {f.i} proof A1: f in {f} by TARSKI:def 1; consider A being non empty functional set such that A2: A = {f} and dom |.{f}.| = meet the set of all dom x where x is Element of A and A3: for i st i in dom |.{f}.| holds |.{f}.|.i = the set of all x.i where x is Element of A by Def2; assume i in dom f; then i in dom |.{f}.| by Th15; then A4: |.{f}.|.i = the set of all x.i where x is Element of A by A3; thus |.{f}.|.i c= { f.i } proof let q be object; assume q in |.{f}.|.i; then consider x being Element of A such that A5: q = x.i by A4; x = f by A2,TARSKI:def 1; hence thesis by A5,TARSKI:def 1; end; let q be object; assume q in { f.i }; then q = f.i by TARSKI:def 1; hence thesis by A2,A4,A1; end; theorem i in I & SF = {f} implies |:SF:|.i = {f.i} proof assume that A1: i in I and A2: SF = {f}; A3: |:SF:| = |.SF.| by A2,Def3; dom |:SF:| = I by PARTFUN1:def 2; then i in dom f by A1,A2,A3,Th15; hence thesis by A2,A3,Th17; end; theorem Th19: i in dom |.{f,f1}.| implies |.{f,f1}.|.i = { f.i, f1.i } proof A1: f in {f,f1} & f1 in {f,f1} by TARSKI:def 2; consider A being non empty functional set such that A2: A = {f,f1} and dom |.{f,f1}.| = meet the set of all dom x where x is Element of A and A3: for i st i in dom |.{f,f1}.| holds |.{f,f1}.|.i = the set of all x.i where x is Element of A by Def2; assume i in dom |.{f,f1}.|; then A4: |.{f,f1}.|.i = the set of all x.i where x is Element of A by A3; thus |.{f,f1}.|.i c= { f.i, f1.i } proof let q be object; assume q in |.{f,f1}.|.i; then consider x being Element of A such that A5: q = x.i by A4; per cases by A2,TARSKI:def 2; suppose x = f; hence thesis by A5,TARSKI:def 2; end; suppose x = f1; hence thesis by A5,TARSKI:def 2; end; end; let q be object; assume q in { f.i, f1.i }; then q = f.i or q = f1.i by TARSKI:def 2; hence thesis by A2,A4,A1; end; theorem Th20: i in I & SF = {f,f1} implies |:SF:|.i = { f.i, f1.i } proof assume that A1: i in I and A2: SF = {f,f1}; dom |:SF:| = I & |:SF:| = |.SF.| by A2,Def3,PARTFUN1:def 2; hence thesis by A1,A2,Th19; end; definition let I, M, SF; redefine func |:SF:| -> MSSubsetFamily of M; coherence proof per cases; suppose A1: SF is non empty; |:SF:| is ManySortedSubset of bool M proof let i be object; assume A2: i in I; then A3: |:SF:|.i = { x.i where x is Element of Bool M : x in SF } by A1,Th14; thus |:SF:|.i c= (bool M).i proof let x be object; assume x in |:SF:|.i; then consider a being Element of Bool M such that A4: x = a.i and a in SF by A3; a c= M by PBOOLE:def 18; then a.i c= M.i by A2; then x in bool (M.i) by A4; hence thesis by A2,MBOOLEAN:def 1; end; end; hence thesis; end; suppose SF is empty; then |:SF:| = EmptyMS I; hence thesis by MSSUBFAM:31; end; end; end; theorem Th21: A in SF implies A in' |:SF:| proof assume A1: A in SF; let i be object; assume i in I; then |:SF:|.i = { x.i where x is Element of Bool M : x in SF } by A1,Th14; hence thesis by A1; end; theorem Th22: SF = {A,B} implies union |:SF:| = A (\/) B proof assume A1: SF = {A,B}; now let i be object; assume A2: i in I; hence (union |:SF:|).i = union (|:SF:|.i) by MBOOLEAN:def 2 .= union { A.i, B.i } by A1,A2,Th20 .= A.i \/ B.i by ZFMISC_1:75 .= (A (\/) B).i by A2,PBOOLE:def 4; end; hence thesis; end; theorem Th23: :: SETFAM_1:12 SF = {E,T} implies meet |:SF:| = E (/\) T proof assume A1: SF = { E,T }; now reconsider sf1 = SF as non empty SubsetFamily of M by A1; let i be object such that A2: i in I; ex Q be Subset-Family of (M.i) st Q = |:sf1:|.i & (meet |:sf1:|).i = Intersect Q by A2,MSSUBFAM:def 1; hence (meet |:SF:|).i = meet (|:sf1:|.i) by A2,SETFAM_1:def 9 .= meet {E.i,T.i} by A1,A2,Th20 .= E.i /\ T.i by SETFAM_1:11 .= (E (/\) T).i by A2,PBOOLE:def 5; end; hence thesis; end; theorem Th24: :: MSSUBFAM:4 for Z being ManySortedSubset of M st for Z1 being ManySortedSet of I st Z1 in SF holds Z c=' Z1 holds Z c=' meet |:SF:| proof let Z be ManySortedSubset of M such that A1: for Z1 be ManySortedSet of I st Z1 in SF holds Z c=' Z1; let i be object such that A2: i in I; consider Q being Subset-Family of M.i such that A3: Q = |:SF:|.i and A4: (meet |:SF:|).i = Intersect Q by A2,MSSUBFAM:def 1; A5: now let q be set such that A6: q in Q; per cases; suppose SF is non empty; then |:SF:|.i = { x.i where x is Element of Bool M : x in SF } by A2,Th14 ; then consider a being Element of Bool M such that A7: q = a.i and A8: a in SF by A3,A6; Z c=' a by A1,A8; hence Z.i c= q by A2,A7; end; suppose SF is empty; then |:SF:| = EmptyMS I; hence Z.i c= q by A3,A6; end; end; Z c= M by PBOOLE:def 18; then Z.i is Subset of M.i by A2; hence thesis by A4,A5,MSSUBFAM:4; end; theorem |: Bool M :| = bool M proof now let i be object; assume A1: i in I; then A2: |:Bool M:|.i = { x.i where x is Element of Bool M : x in Bool M} by Th14; thus |: Bool M :|.i = (bool M).i proof thus |: Bool M :|.i c= (bool M).i by A1,PBOOLE:def 2,def 18; let a be object such that A3: a in (bool M).i; dom (EmptyMS I +* (i .--> a)) = I by A1,PZFMISC1:1; then reconsider X = EmptyMS I +* (i .--> a) as ManySortedSet of I by PARTFUN1:def 2,RELAT_1:def 18; A4: dom (i .--> a) = {i} by FUNCOP_1:13; i in {i} by TARSKI:def 1; then A5: X.i = (i .--> a).i by A4,FUNCT_4:13 .= a by FUNCOP_1:72; X is ManySortedSubset of M proof let s be object such that A6: s in I; per cases; suppose A7: s = i; then a in bool (M.s) by A3,A6,MBOOLEAN:def 1; hence thesis by A5,A7; end; suppose s <> i; then not s in dom (i .--> a) by A4,TARSKI:def 1; then X.s = EmptyMS I.s by FUNCT_4:11 .= {}; hence thesis; end; end; then X is Element of Bool M by Def1; hence thesis by A2,A5; end; end; hence thesis; end; definition let I, M; let IT be SubsetFamily of M; attr IT is additive means for A, B st A in IT & B in IT holds A (\/) B in IT; attr IT is absolutely-additive means for F be SubsetFamily of M st F c= IT holds union |:F:| in IT; attr IT is multiplicative means for A, B st A in IT & B in IT holds A (/\) B in IT; attr IT is absolutely-multiplicative means :Def7: for F be SubsetFamily of M st F c= IT holds meet |:F:| in IT; attr IT is properly-upper-bound means :Def8: M in IT; attr IT is properly-lower-bound means EmptyMS I in IT; end; Lm1: Bool M is additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound proof thus Bool M is additive by Th10; thus Bool M is absolutely-additive proof let F be SubsetFamily of M such that F c= Bool M; union |:F:| c= M by MSSUBFAM:40; then union |:F:| is ManySortedSubset of M by PBOOLE:def 18; hence thesis by Def1; end; thus Bool M is multiplicative by Th9; thus Bool M is absolutely-multiplicative by Def1; M is ManySortedSubset of M by PBOOLE:def 18; then M in Bool M by Def1; hence Bool M is properly-upper-bound; EmptyMS I c= M by PBOOLE:43; then EmptyMS I is ManySortedSubset of M by PBOOLE:def 18; hence EmptyMS I in Bool M by Def1; end; registration let I, M; cluster non empty functional with_common_domain additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound for SubsetFamily of M; existence proof take Bool M; thus thesis by Lm1; end; end; definition let I, M; redefine func Bool M -> additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound SubsetFamily of M; coherence by Lm1; end; registration let I, M; cluster absolutely-additive -> additive for SubsetFamily of M; coherence proof let SF be SubsetFamily of M such that A1: SF is absolutely-additive; let A, B; assume that A2: A in SF and A3: B in SF; B is ManySortedSubset of M by A3,Def1; then A4: B c= M by PBOOLE:def 18; A is ManySortedSubset of M by A2,Def1; then A c= M by PBOOLE:def 18; then reconsider ab = {A,B} as SubsetFamily of M by A4,Th8; {A} c= SF & {B} c= SF by A2,A3,ZFMISC_1:31; then {A} \/ {B} c= SF by XBOOLE_1:8; then {A,B} c= SF by ENUMSET1:1; then union |:ab:| in SF by A1; hence thesis by Th22; end; end; registration let I, M; cluster absolutely-multiplicative -> multiplicative for SubsetFamily of M; coherence proof let SF be SubsetFamily of M such that A1: SF is absolutely-multiplicative; let A, B; assume that A2: A in SF and A3: B in SF; B is ManySortedSubset of M by A3,Def1; then A4: B c= M by PBOOLE:def 18; A is ManySortedSubset of M by A2,Def1; then A c= M by PBOOLE:def 18; then reconsider ab = {A,B} as SubsetFamily of M by A4,Th8; {A} c= SF & {B} c= SF by A2,A3,ZFMISC_1:31; then {A} \/ {B} c= SF by XBOOLE_1:8; then {A,B} c= SF by ENUMSET1:1; then meet |:ab:| in SF by A1; hence thesis by A2,A3,Th23; end; end; registration let I, M; cluster absolutely-multiplicative -> properly-upper-bound for SubsetFamily of M; coherence proof reconsider a = {} as SubsetFamily of M by XBOOLE_1:2; let SF be SubsetFamily of M such that A1: SF is absolutely-multiplicative; |:a:| = EmptyMS I; then A2: meet |:a:| = M by MSSUBFAM:41; a c= SF; hence M in SF by A1,A2; end; end; registration let I, M; cluster properly-upper-bound -> non empty for SubsetFamily of M; coherence; end; registration let I, M; cluster absolutely-additive -> properly-lower-bound for SubsetFamily of M; coherence proof reconsider a = {} as SubsetFamily of M by XBOOLE_1:2; let SF be SubsetFamily of M such that A1: SF is absolutely-additive; |:a:| = EmptyMS I; then A2: union |:a:| = EmptyMS I by MBOOLEAN:21; a c= SF; hence EmptyMS I in SF by A1,A2; end; end; registration let I, M; cluster properly-lower-bound -> non empty for SubsetFamily of M; coherence; end; begin :: Properties of Closure Operators definition let I, M; mode SetOp of M is Function of Bool M, Bool M; end; definition let I, M; let f be SetOp of M; let x be Element of Bool M; redefine func f.x -> Element of Bool M; coherence proof f.x in Bool M; hence thesis; end; end; definition let I, M; let IT be SetOp of M; attr IT is reflexive means :Def10: for x being Element of Bool M holds x c=' IT.x; attr IT is monotonic means :Def11: for x, y being Element of Bool M st x c=' y holds IT.x c=' IT.y; attr IT is idempotent means :Def12: for x being Element of Bool M holds IT.x = IT.(IT.x); attr IT is topological means for x, y being Element of Bool M holds IT.(x (\/) y) = (IT.x) (\/) (IT.y); end; registration let I, M; cluster reflexive monotonic idempotent topological for SetOp of M; existence proof reconsider f = id (Bool M) as SetOp of M; take f; thus f is reflexive; thus f is monotonic; thus f is idempotent; thus f is topological proof let X, Y be Element of Bool M; X c= M & Y c= M by PBOOLE:def 18; then X (\/) Y c= M by PBOOLE:16; then X (\/) Y is ManySortedSubset of M by PBOOLE:def 18; then X (\/) Y in Bool M by Def1; hence f.(X (\/) Y) = X (\/) Y by FUNCT_1:18 .= f.X (\/) Y .= f.X (\/) f.Y; end; end; end; theorem :: CLOSURE:11 id (Bool A) is reflexive SetOp of A proof reconsider f = id (Bool A) as SetOp of A; f is reflexive; hence thesis; end; theorem :: CLOSURE:12 id (Bool A) is monotonic SetOp of A proof reconsider f = id (Bool A) as SetOp of A; f is monotonic; hence thesis; end; theorem :: CLOSURE:13 id (Bool A) is idempotent SetOp of A proof reconsider f = id (Bool A) as SetOp of A; f is idempotent; hence thesis; end; theorem :: CLOSURE:15 id (Bool A) is topological SetOp of A proof reconsider f = id (Bool A) as SetOp of A; f is topological proof let X, Y be Element of Bool A; X c= A & Y c= A by PBOOLE:def 18; then X (\/) Y c= A by PBOOLE:16; then X (\/) Y is ManySortedSubset of A by PBOOLE:def 18; then X (\/) Y in Bool A by Def1; hence f.(X (\/) Y) = X (\/) Y by FUNCT_1:18 .= f.X (\/) Y .= f.X (\/) f.Y; end; hence thesis; end; reserve g, h for SetOp of M; theorem :: CLOSURE:16 E = M & g is reflexive implies E = g.E proof assume A1: E = M; assume g is reflexive; then A2: E c= g.E; g.E c= E by A1,PBOOLE:def 18; hence thesis by A2,PBOOLE:146; end; theorem :: CLOSURE:17 (g is reflexive & for X being Element of Bool M holds g.X c= X) implies g is idempotent proof assume that A1: g is reflexive and A2: for X being Element of Bool M holds g.X c= X; let X be Element of Bool M; A3: g.X c= g.(g.X) by A1; g.(g.X) c= g.X by A2; hence thesis by A3,PBOOLE:146; end; theorem :: CLOSURE:18 for A being Element of Bool M st A = E (/\) T holds g is monotonic implies g.A c= g.E (/\) g.T proof let A be Element of Bool M such that A1: A = E (/\) T; assume A2: g is monotonic; E (/\) T c= T by PBOOLE:15; then A3: g.A c= g.T by A1,A2; E (/\) T c= E by PBOOLE:15; then g.A c= g.E by A1,A2; hence thesis by A3,PBOOLE:17; end; registration let I, M; cluster topological -> monotonic for SetOp of M; coherence proof let g be SetOp of M such that A1: g is topological; let X, Y be Element of Bool M such that A2: X c= Y; g.X (\/) g.Y = g.(X (\/) Y) by A1 .= g.Y by A2,PBOOLE:22; hence thesis by PBOOLE:26; end; end; theorem :: CLOSURE:19 for A being Element of Bool M st A = E (\) T holds g is topological implies g.E (\) g.T c= g.A proof let A be Element of Bool M such that A1: A = E (\) T; assume A2: g is topological; then g.E (\/) g.T = g.(E (\/) T) .= g.((E(\)T) (\/) T) by PBOOLE:67 .= (g.A) (\/) (g.T) by A1,A2; then g.E c= g.A (\/) g.T by PBOOLE:14; then g.E (\) g.T c= (g.A (\/) g.T) (\) g.T by PBOOLE:53; then A3: g.E (\) g.T c= g.A (\) g.T by PBOOLE:75; g.A (\) g.T c= g.A by PBOOLE:56; hence thesis by A3,PBOOLE:13; end; definition let I, M, h, g; redefine func g * h -> SetOp of M; coherence proof g * h is Function of Bool M, Bool M; hence thesis; end; end; theorem :: CLOSURE:21 g is reflexive & h is reflexive implies g * h is reflexive proof assume A1: g is reflexive & h is reflexive; let X be Element of Bool M; X c= h.X & h.X c= g.(h.X) by A1; then dom h = Bool M & X c= g.(h.X) by FUNCT_2:def 1,PBOOLE:13; hence thesis by FUNCT_1:13; end; theorem :: CLOSURE:22 g is monotonic & h is monotonic implies g * h is monotonic proof assume that A1: g is monotonic and A2: h is monotonic; A3: dom h = Bool M by FUNCT_2:def 1; let X, Y be Element of Bool M; assume X c= Y; then h.X c= h.Y by A2; then g.(h.X) c= g.(h.Y) by A1; then g.(h.X) c= (g*h).Y by A3,FUNCT_1:13; hence thesis by A3,FUNCT_1:13; end; theorem :: CLOSURE:23 g is idempotent & h is idempotent & g*h = h*g implies g * h is idempotent proof assume that A1: g is idempotent and A2: h is idempotent and A3: g*h = h*g; let X be Element of Bool M; A4: dom g = Bool M by FUNCT_2:def 1; A5: dom h = Bool M by FUNCT_2:def 1; hence (g*h).X = g.(h.X) by FUNCT_1:13 .= g.(h.(h.X)) by A2 .= g.(g.(h.(h.X))) by A1 .= g.((h*g).(h.X)) by A3,A5,FUNCT_1:13 .= g.(h.(g.(h.X))) by A4,FUNCT_1:13 .= g.(h.((g*h).X)) by A5,FUNCT_1:13 .= (g*h).((g*h).X) by A5,FUNCT_1:13; end; theorem :: CLOSURE:25 g is topological & h is topological implies g * h is topological proof assume that A1: g is topological and A2: h is topological; let X, Y be Element of Bool M; A3: dom h = Bool M by FUNCT_2:def 1; hence (g*h).(X (\/) Y) = g.(h.(X (\/) Y)) by Th10,FUNCT_1:13 .= g.(h.X (\/) h.Y) by A2 .= g.(h.X) (\/) g.(h.Y) by A1 .= (g*h).X (\/) g.(h.Y) by A3,FUNCT_1:13 .= (g*h).X (\/) (g*h).Y by A3,FUNCT_1:13; end; begin :: On the Closure Operator and the Closure System reserve S for 1-sorted; definition let S; struct(many-sorted over S) ClosureStr over S (# Sorts -> ManySortedSet of the carrier of S, Family -> SubsetFamily of the Sorts #); end; reserve MS for many-sorted over S; definition let S; let IT be ClosureStr over S; attr IT is additive means :Def14: the Family of IT is additive; attr IT is absolutely-additive means :Def15: the Family of IT is absolutely-additive; attr IT is multiplicative means :Def16: the Family of IT is multiplicative; attr IT is absolutely-multiplicative means :Def17: the Family of IT is absolutely-multiplicative; attr IT is properly-upper-bound means :Def18: the Family of IT is properly-upper-bound; attr IT is properly-lower-bound means :Def19: the Family of IT is properly-lower-bound; end; definition let S, MS; func Full MS -> ClosureStr over S equals ClosureStr (#the Sorts of MS, Bool the Sorts of MS#); correctness; end; registration let S, MS; cluster Full MS -> strict additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound; coherence; end; registration let S; let MS be non-empty many-sorted over S; cluster Full MS -> non-empty; coherence; end; registration let S; cluster strict non-empty additive absolutely-additive multiplicative absolutely-multiplicative properly-upper-bound properly-lower-bound for ClosureStr over S; existence proof set a = the non-empty many-sorted over S; take Full a; thus thesis; end; end; registration let S; let CS be additive ClosureStr over S; cluster the Family of CS -> additive; coherence by Def14; end; registration let S; let CS be absolutely-additive ClosureStr over S; cluster the Family of CS -> absolutely-additive; coherence by Def15; end; registration let S; let CS be multiplicative ClosureStr over S; cluster the Family of CS -> multiplicative; coherence by Def16; end; registration let S; let CS be absolutely-multiplicative ClosureStr over S; cluster the Family of CS -> absolutely-multiplicative; coherence by Def17; end; registration let S; let CS be properly-upper-bound ClosureStr over S; cluster the Family of CS -> properly-upper-bound; coherence by Def18; end; registration let S; let CS be properly-lower-bound ClosureStr over S; cluster the Family of CS -> properly-lower-bound; coherence by Def19; end; registration let S; let M be non-empty ManySortedSet of the carrier of S; let F be SubsetFamily of M; cluster ClosureStr (#M, F#) -> non-empty; coherence; end; registration let S, MS; let F be additive SubsetFamily of the Sorts of MS; cluster ClosureStr (#the Sorts of MS, F#) -> additive; coherence; end; registration let S, MS; let F be absolutely-additive SubsetFamily of the Sorts of MS; cluster ClosureStr (#the Sorts of MS, F#) -> absolutely-additive; coherence; end; registration let S, MS; let F be multiplicative SubsetFamily of the Sorts of MS; cluster ClosureStr (#the Sorts of MS, F#) -> multiplicative; coherence; end; registration let S, MS; let F be absolutely-multiplicative SubsetFamily of the Sorts of MS; cluster ClosureStr (#the Sorts of MS, F#) -> absolutely-multiplicative; coherence; end; registration let S, MS; let F be properly-upper-bound SubsetFamily of the Sorts of MS; cluster ClosureStr (#the Sorts of MS, F#) -> properly-upper-bound; coherence; end; registration let S, MS; let F be properly-lower-bound SubsetFamily of the Sorts of MS; cluster ClosureStr (#the Sorts of MS, F#) -> properly-lower-bound; coherence; end; registration let S; cluster absolutely-additive -> additive for ClosureStr over S; coherence; end; registration let S; cluster absolutely-multiplicative -> multiplicative for ClosureStr over S; coherence; end; registration let S; cluster absolutely-multiplicative -> properly-upper-bound for ClosureStr over S; coherence; end; registration let S; cluster absolutely-additive -> properly-lower-bound for ClosureStr over S; coherence; end; definition let S; mode ClosureSystem of S is absolutely-multiplicative ClosureStr over S; end; definition let I, M; mode ClosureOperator of M is reflexive monotonic idempotent SetOp of M; end; definition let S; let A be ManySortedSet of the carrier of S; let g be ClosureOperator of A; func ClOp->ClSys g -> strict ClosureStr over S means :Def21: the Sorts of it = A & the Family of it = { x where x is Element of Bool A : g.x = x }; existence proof defpred P[set] means g.$1 = $1; set SF = { x where x is Element of Bool A : P[ x ] }; SF is Subset of Bool A from DOMAIN_1:sch 7; then reconsider D = SF as SubsetFamily of A; take ClosureStr (#A, D#); thus thesis; end; uniqueness; end; registration let S; let A be ManySortedSet of the carrier of S; let g be ClosureOperator of A; cluster ClOp->ClSys g -> absolutely-multiplicative; coherence proof A1: the Sorts of ClOp->ClSys g = A by Def21; defpred P[set] means g.$1 = $1; set SF = { x where x is Element of Bool A : P[ x ] }; A2: SF = the Family of ClOp->ClSys g by Def21; SF is Subset of Bool A from DOMAIN_1:sch 7; then reconsider D = SF as SubsetFamily of A; A3: ClOp->ClSys g = ClosureStr (#A, D#) by A1,A2; D is absolutely-multiplicative proof let F be SubsetFamily of A such that A4: F c= D; reconsider mf = meet |:F:| as Element of Bool A by Def1; now let Z1 be ManySortedSet of the carrier of S; assume A5: Z1 in F; then reconsider y1 = Z1 as Element of Bool A; Z1 in D by A4,A5; then A6: ex a being Element of Bool A st Z1 = a & g.a = a; mf c=' y1 by A5,Th21,MSSUBFAM:43; hence g.mf c=' Z1 by A6,Def11; end; then A7: g.mf c=' mf by Th24; mf c=' g.mf by Def10; then g.mf = mf by A7,PBOOLE:146; hence thesis; end; hence ClOp->ClSys g is absolutely-multiplicative by A3; end; end; definition let S; let A be ClosureSystem of S; let C be ManySortedSubset of the Sorts of A; func Cl C -> Element of Bool the Sorts of A means :Def22: ex F being SubsetFamily of the Sorts of A st it = meet |:F:| & F = { X where X is Element of Bool the Sorts of A : C c=' X & X in the Family of A }; existence proof defpred P[Element of Bool the Sorts of A] means C c= $1 & $1 in the Family of A; { X where X is Element of Bool the Sorts of A : P[X] } is Subset of Bool the Sorts of A from DOMAIN_1:sch 7; then reconsider F = { X where X is Element of Bool the Sorts of A : C c= X & X in the Family of A } as SubsetFamily of the Sorts of A; reconsider IT = meet |:F:| as Element of Bool the Sorts of A by Def1; take IT,F; thus thesis; end; uniqueness; end; theorem Th38: for D being ClosureSystem of S for a being Element of Bool the Sorts of D for f being SetOp of the Sorts of D st a in the Family of D & for x being Element of Bool the Sorts of D holds f.x = Cl x holds f.a = a proof let D be ClosureSystem of S, a be Element of Bool the Sorts of D, f be SetOp of the Sorts of D such that A1: a in the Family of D and A2: for x being Element of Bool the Sorts of D holds f.x = Cl x; consider F being SubsetFamily of the Sorts of D such that A3: Cl a = meet |:F:| and A4: F = { X where X is Element of Bool the Sorts of D : a c=' X & X in the Family of D } by Def22; A5: f.a = meet |:F:| by A2,A3; a in F by A1,A4; then A6: f.a c= a by A5,Th21,MSSUBFAM:43; for Z1 being ManySortedSet of the carrier of S st Z1 in F holds a c=' Z1 proof let Z1 be ManySortedSet of the carrier of S; assume Z1 in F; then ex b being Element of Bool the Sorts of D st Z1 = b & a c=' b & b in the Family of D by A4; hence thesis; end; then a c= f.a by A5,Th24; hence thesis by A6,PBOOLE:146; end; theorem for D being ClosureSystem of S for a being Element of Bool the Sorts of D for f being SetOp of the Sorts of D st f.a = a & for x being Element of Bool the Sorts of D holds f.x = Cl x holds a in the Family of D proof deffunc F(set) = $1; let D be ClosureSystem of S, a be Element of Bool the Sorts of D, f be SetOp of the Sorts of D such that A1: f.a = a & for x being Element of Bool the Sorts of D holds f.x = Cl x; set F = the Family of D, M = the Sorts of D; defpred P[Element of Bool M] means a c=' $1; defpred R[Element of Bool M] means a c=' $1 & $1 in F; defpred S[Element of Bool M] means $1 in F & a c=' $1; A2: { F(w) where w is Element of Bool M : F(w) in F & P[w] } c= F from FRAENKEL:sch 17; A3: for q being Element of Bool M holds R[q] iff S[q]; A4: { F(s) where s is Element of Bool M : R[s] } = { F(b) where b is Element of Bool M : S[b] } from FRAENKEL:sch 3(A3); consider SF being SubsetFamily of M such that A5: Cl a = meet |:SF:| and A6: SF = { X where X is Element of Bool M : a c= X & X in F } by Def22; a = meet |:SF:| by A1,A5; hence thesis by A6,A2,A4,Def7; end; theorem Th40: for D being ClosureSystem of S for f being SetOp of the Sorts of D st for x being Element of Bool the Sorts of D holds f.x = Cl x holds f is reflexive monotonic idempotent proof let D be ClosureSystem of S, f be SetOp of the Sorts of D such that A1: for x being Element of Bool the Sorts of D holds f.x = Cl x; set M = the Sorts of D; A2: f is reflexive proof let x be Element of Bool M; consider F being SubsetFamily of M such that A3: Cl x = meet |:F:| and A4: F = { X where X is Element of Bool the Sorts of D : x c=' X & X in the Family of D } by Def22; A5: for Z1 being ManySortedSet of the carrier of S st Z1 in F holds x c=' Z1 proof let Z1 be ManySortedSet of the carrier of S; assume Z1 in F; then ex a being Element of Bool M st Z1 = a & x c=' a & a in the Family of D by A4; hence thesis; end; f.x = meet |:F:| by A1,A3; hence thesis by A5,Th24; end; A6: f is monotonic proof let x, y be Element of Bool M such that A7: x c=' y; consider Fy being SubsetFamily of M such that A8: Cl y = meet |:Fy:| and A9: Fy = { X where X is Element of Bool the Sorts of D : y c=' X & X in the Family of D } by Def22; consider Fx being SubsetFamily of M such that A10: Cl x = meet |:Fx:| and A11: Fx = { X where X is Element of Bool the Sorts of D : x c=' X & X in the Family of D } by Def22; |:Fy:| c=' |:Fx:| proof let i be object such that A12: i in the carrier of S; thus |:Fy:|.i c= |:Fx:|.i proof let q be object such that A13: q in |:Fy:|.i; per cases; suppose Fy is empty; then reconsider Fy9 = Fy as empty SubsetFamily of M; |:Fy9:|.i is empty; hence thesis by A13; end; suppose Fy is non empty; then |:Fy:|.i = { e.i where e is Element of Bool M : e in Fy } by A12 ,Th14; then consider w being Element of Bool M such that A14: q = w.i and A15: w in Fy by A13; A16: ex r being Element of Bool M st r = w & y c=' r & r in the Family of D by A9,A15; then x c=' w by A7,PBOOLE:13; then A17: w in Fx by A11,A16; then |:Fx:|.i = { e.i where e is Element of Bool M : e in Fx } by A12 ,Th14; hence thesis by A14,A17; end; end; end; then meet |:Fx:| c=' meet |:Fy:| by MSSUBFAM:46; then meet |:Fx:| c=' f.y by A1,A8; hence thesis by A1,A10; end; f is idempotent proof let x be Element of Bool M; consider F being SubsetFamily of M such that A18: Cl x = meet |:F:| and A19: F = { X where X is Element of Bool the Sorts of D : x c=' X & X in the Family of D } by Def22; F c= the Family of D proof let k be object; assume k in F; then ex q being Element of Bool M st k = q & x c=' q & q in the Family of D by A19; hence thesis; end; then A20: meet |:F:| in the Family of D by Def7; thus f.x = meet |:F:| by A1,A18 .= f.(meet |:F:|) by A1,A20,Th38 .= f.(f.x) by A1,A18; end; hence thesis by A2,A6; end; definition let S; let D be ClosureSystem of S; func ClSys->ClOp D -> ClosureOperator of the Sorts of D means :Def23: for x being Element of Bool the Sorts of D holds it.x = Cl x; existence proof set M = the Sorts of D; deffunc F(Element of Bool M) = Cl $1; consider f being Function of Bool M, Bool M such that A1: for x being Element of Bool M holds f.x = F(x) from FUNCT_2:sch 4; reconsider f as SetOp of M; reconsider f as ClosureOperator of M by A1,Th40; take f; thus thesis by A1; end; uniqueness proof let f, g be ClosureOperator of the Sorts of D such that A2: for x being Element of Bool the Sorts of D holds f.x = Cl x and A3: for x being Element of Bool the Sorts of D holds g.x = Cl x; now set X = Bool the Sorts of D; thus X = dom f by FUNCT_2:def 1; thus X = dom g by FUNCT_2:def 1; let x be object; assume x in X; then reconsider x1 = x as Element of Bool the Sorts of D; thus f.x = Cl x1 by A2 .= g.x by A3; end; hence f = g; end; end; theorem for A being ManySortedSet of the carrier of S for f being ClosureOperator of A holds ClSys->ClOp (ClOp->ClSys f) = f proof let A be ManySortedSet of the carrier of S, f be ClosureOperator of A; set D = ClOp->ClSys f, M = the Sorts of D, f1 = ClSys->ClOp D; A1: A = M by Def21; then reconsider ff = f as reflexive idempotent monotonic SetOp of M; for x being object st x in Bool A holds f1.x = ff.x proof let x be object; assume x in Bool A; then reconsider x1 = x as Element of Bool M by Def21; consider F being SubsetFamily of M such that A2: Cl x1 = meet |:F:| and A3: F = { X where X is Element of Bool M : x1 c=' X & X in the Family of D } by Def22; A4: now A5: x1 c=' ff.x1 by Def10; x1 c=' M & M in the Family of D by Def8,PBOOLE:def 18; then M in F by A3; then reconsider F9 = F as non empty SubsetFamily of M; let i be object; assume A6: i in the carrier of S; then consider Q be Subset-Family of (M.i) such that A7: Q = |:F:|.i and A8: (meet |:F:|).i = Intersect Q by MSSUBFAM:def 1; A9: Q = { q.i where q is Element of Bool M : q in F9 } by A6,A7,Th14; A10: the Family of D = { q where q is Element of Bool M : ff.q = q } by A1 ,Def21; A11: now let z be set; assume z in Q; then consider q being Element of Bool M such that A12: z = q.i and A13: q in F9 by A9; consider X being Element of Bool M such that A14: q = X and A15: x1 c=' X & X in the Family of D by A3,A13; (ex t being Element of Bool M st X = t & ff.t = t )& ff.x1 c=' ff .X by A10,A15,Def11; hence ff.x1.i c= z by A6,A12,A14; end; ff.(ff.x1) = ff.x1 by Def12; then ff.x1 in the Family of D by A10; then ff.x1 in F9 by A3,A5; then ff.x1.i in Q by A9; then A16: (meet |:F:|).i c= ff.x1.i by A8,MSSUBFAM:2; Q = |:F9:|.i by A7; then ff.x1.i c= (meet |:F:|).i by A6,A8,A11,MSSUBFAM:5; hence (meet |:F:|).i = ff.x1.i by A16; end; thus f1.x = Cl x1 by Def23 .= ff.x by A2,A4,PBOOLE:3; end; hence thesis by A1,FUNCT_2:12; end; deffunc F(set) = $1; theorem for D being ClosureSystem of S holds ClOp->ClSys (ClSys->ClOp D) = the ClosureStr of D proof let D be ClosureSystem of S; set M = the Sorts of D, F = the Family of D, d = the Family of ClOp->ClSys ( ClSys->ClOp D), f = ClSys->ClOp D; A1: d = { x where x is Element of Bool M : f.x = x } by Def21; F = d proof thus F c= d proof let q be object; assume A2: q in F; then reconsider q1 = q as Element of Bool M; consider SF being SubsetFamily of M such that A3: Cl q1 = meet |:SF:| and A4: SF = { X where X is Element of Bool M : q1 c= X & X in F } by Def22; q1 c=' M & M in F by Def8,PBOOLE:def 18; then M in SF by A4; then reconsider SF9 = SF as non empty SubsetFamily of M; now let i be object; assume A5: i in the carrier of S; then consider Q be Subset-Family of (M.i) such that A6: Q = |:SF9:|.i and A7: (meet |:SF9:|).i = Intersect Q by MSSUBFAM:def 1; A8: Q = { x.i where x is Element of Bool M : x in SF9 } by A5,A6,Th14; q1 in SF9 by A2,A4; then A9: q1.i in Q by A8; then A10: Intersect Q c= q1.i by MSSUBFAM:2; now let z be set; assume z in Q; then consider x being Element of Bool M such that A11: z = x.i and A12: x in SF9 by A8; ex xx being Element of Bool M st xx = x & q1 c=' xx & xx in F by A4 ,A12; hence q1.i c= z by A5,A11; end; then q1.i c= Intersect Q by A9,MSSUBFAM:5; then Intersect Q = q1.i by A10; hence f.q1.i = q1.i by A3,A7,Def23; end; then f.q1 = q1; hence thesis by A1; end; let q be object; assume q in d; then consider x being Element of Bool M such that A13: q = x & f.x = x by A1; defpred S[Element of Bool M] means $1 in F & x c=' $1; defpred R[Element of Bool M] means x c=' $1 & $1 in F; defpred P[Element of Bool M] means x c=' $1; A14: { F(w) where w is Element of Bool M : F(w) in F & P[w] } c= F from FRAENKEL:sch 17; A15: for a being Element of Bool M holds R[a] iff S[a]; A16: { F(a) where a is Element of Bool M : R[a] } = { F(b) where b is Element of Bool M : S[b] } from FRAENKEL:sch 3(A15); consider SF being SubsetFamily of M such that A17: Cl x = meet |:SF:| and A18: SF = { X where X is Element of Bool M : x c=' X & X in F } by Def22; meet |:SF:| = q by A13,A17,Def23; hence thesis by A18,A14,A16,Def7; end; hence thesis by Def21; end;