:: CLOSURE3 semantic presentation begin registration let S be non empty 1-sorted ; cluster 1-sorted(# the carrier of S #) -> non empty ; coherence not 1-sorted(# the carrier of S #) is empty ; end; theorem Th1: :: CLOSURE3:1 for I being non empty set for M, N being ManySortedSet of I holds M +* N = N proof let I be non empty set ; ::_thesis: for M, N being ManySortedSet of I holds M +* N = N let M, N be ManySortedSet of I; ::_thesis: M +* N = N dom M = I by PARTFUN1:def_2 .= dom N by PARTFUN1:def_2 ; hence M +* N = N by FUNCT_4:19; ::_thesis: verum end; theorem :: CLOSURE3:2 for I being set for M, N being ManySortedSet of I for F being SubsetFamily of M st N in F holds meet |:F:| c=' N by CLOSURE2:21, MSSUBFAM:43; theorem Th3: :: CLOSURE3:3 for S being non empty non void ManySortedSign for MA being strict non-empty MSAlgebra over S for F being SubsetFamily of the Sorts of MA st F c= SubSort MA holds for B being MSSubset of MA st B = meet |:F:| holds B is opers_closed proof let S be non empty non void ManySortedSign ; ::_thesis: for MA being strict non-empty MSAlgebra over S for F being SubsetFamily of the Sorts of MA st F c= SubSort MA holds for B being MSSubset of MA st B = meet |:F:| holds B is opers_closed let MA be strict non-empty MSAlgebra over S; ::_thesis: for F being SubsetFamily of the Sorts of MA st F c= SubSort MA holds for B being MSSubset of MA st B = meet |:F:| holds B is opers_closed let F be SubsetFamily of the Sorts of MA; ::_thesis: ( F c= SubSort MA implies for B being MSSubset of MA st B = meet |:F:| holds B is opers_closed ) assume A1: F c= SubSort MA ; ::_thesis: for B being MSSubset of MA st B = meet |:F:| holds B is opers_closed let B be MSSubset of MA; ::_thesis: ( B = meet |:F:| implies B is opers_closed ) assume A2: B = meet |:F:| ; ::_thesis: B is opers_closed percases ( F = {} or F <> {} ) ; supposeA3: F = {} ; ::_thesis: B is opers_closed set Q = the Sorts of MA; reconsider FF = |:F:| as MSSubsetFamily of the Sorts of MA ; set I = the carrier of S; FF = [[0]] the carrier of S by A3, CLOSURE2:def_3; then A4: the Sorts of MA = B by A2, MSSUBFAM:41; reconsider Q = the Sorts of MA as MSSubset of MA by PBOOLE:def_18; for o being OperSymbol of S holds Q is_closed_on o proof let o be OperSymbol of S; ::_thesis: Q is_closed_on o A5: ( the ResultSort of S . o = the_result_sort_of o & dom the ResultSort of S = the carrier' of S ) by FUNCT_2:def_1, MSUALG_1:def_2; Result (o,MA) = (Q * the ResultSort of S) . o by MSUALG_1:def_5 .= Q . (the_result_sort_of o) by A5, FUNCT_1:13 ; then A6: rng ((Den (o,MA)) | ((Q #) . (the_arity_of o))) c= Q . (the_result_sort_of o) by RELAT_1:def_19; ( the Arity of S . o = the_arity_of o & dom the Arity of S = the carrier' of S ) by FUNCT_2:def_1, MSUALG_1:def_1; then A7: ((Q #) * the Arity of S) . o = (Q #) . (the_arity_of o) by FUNCT_1:13; (Q * the ResultSort of S) . o = Q . (the_result_sort_of o) by A5, FUNCT_1:13; hence Q is_closed_on o by A7, A6, MSUALG_2:def_5; ::_thesis: verum end; hence B is opers_closed by A4, MSUALG_2:def_6; ::_thesis: verum end; supposeA8: F <> {} ; ::_thesis: B is opers_closed set SS = S; let o be OperSymbol of S; :: according to MSUALG_2:def_6 ::_thesis: B is_closed_on o set i = the_result_sort_of o; A9: the ResultSort of S . o = the_result_sort_of o by MSUALG_1:def_2; A10: dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1; ( the Arity of S . o = the_arity_of o & dom the Arity of S = the carrier' of S ) by FUNCT_2:def_1, MSUALG_1:def_1; then A11: ((B #) * the Arity of S) . o = (B #) . (the_arity_of o) by FUNCT_1:13; Result (o,MA) = ( the Sorts of MA * the ResultSort of S) . o by MSUALG_1:def_5 .= the Sorts of MA . (the_result_sort_of o) by A9, A10, FUNCT_1:13 ; then A12: rng ((Den (o,MA)) | ((B #) . (the_arity_of o))) c= the Sorts of MA . (the_result_sort_of o) by RELAT_1:def_19; A13: rng ((Den (o,MA)) | ((B #) . (the_arity_of o))) c= B . (the_result_sort_of o) proof consider Q being Subset-Family of ( the Sorts of MA . (the_result_sort_of o)) such that A14: Q = |:F:| . (the_result_sort_of o) and A15: B . (the_result_sort_of o) = Intersect Q by A2, MSSUBFAM:def_1; let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in rng ((Den (o,MA)) | ((B #) . (the_arity_of o))) or v in B . (the_result_sort_of o) ) assume A16: v in rng ((Den (o,MA)) | ((B #) . (the_arity_of o))) ; ::_thesis: v in B . (the_result_sort_of o) then consider p being set such that A17: p in dom ((Den (o,MA)) | ((B #) . (the_arity_of o))) and A18: v = ((Den (o,MA)) | ((B #) . (the_arity_of o))) . p by FUNCT_1:def_3; for Y being set st Y in Q holds v in Y proof A19: |:F:| . (the_result_sort_of o) = { (xx . (the_result_sort_of o)) where xx is Element of Bool the Sorts of MA : xx in F } by A8, CLOSURE2:14; let Y be set ; ::_thesis: ( Y in Q implies v in Y ) assume Y in Q ; ::_thesis: v in Y then consider xx being Element of Bool the Sorts of MA such that A20: Y = xx . (the_result_sort_of o) and A21: xx in F by A14, A19; reconsider xx = xx as MSSubset of MA ; xx is opers_closed by A1, A21, MSUALG_2:14; then xx is_closed_on o by MSUALG_2:def_6; then A22: rng ((Den (o,MA)) | (((xx #) * the Arity of S) . o)) c= (xx * the ResultSort of S) . o by MSUALG_2:def_5; B c= xx by A2, A21, CLOSURE2:21, MSSUBFAM:43; then (Den (o,MA)) | (((B #) * the Arity of S) . o) c= (Den (o,MA)) | (((xx #) * the Arity of S) . o) by MSUALG_2:2, RELAT_1:75; then A23: dom ((Den (o,MA)) | (((B #) * the Arity of S) . o)) c= dom ((Den (o,MA)) | (((xx #) * the Arity of S) . o)) by RELAT_1:11; A24: v = (Den (o,MA)) . p by A17, A18, FUNCT_1:47; then v = ((Den (o,MA)) | (((xx #) * the Arity of S) . o)) . p by A11, A17, A23, FUNCT_1:47; then v in rng ((Den (o,MA)) | (((xx #) * the Arity of S) . o)) by A11, A17, A23, FUNCT_1:def_3; then (Den (o,MA)) . p in (xx * the ResultSort of S) . o by A22, A24; then (Den (o,MA)) . p in xx . ( the ResultSort of S . o) by A10, FUNCT_1:13; then (Den (o,MA)) . p in xx . (the_result_sort_of o) by MSUALG_1:def_2; hence v in Y by A17, A18, A20, FUNCT_1:47; ::_thesis: verum end; hence v in B . (the_result_sort_of o) by A12, A16, A15, SETFAM_1:43; ::_thesis: verum end; (B * the ResultSort of S) . o = B . (the_result_sort_of o) by A9, A10, FUNCT_1:13; hence B is_closed_on o by A11, A13, MSUALG_2:def_5; ::_thesis: verum end; end; end; begin theorem :: CLOSURE3:4 for A, B, C being set st A is_coarser_than B & B is_coarser_than C holds A is_coarser_than C proof let A, B, C be set ; ::_thesis: ( A is_coarser_than B & B is_coarser_than C implies A is_coarser_than C ) assume that A1: A is_coarser_than B and A2: B is_coarser_than C ; ::_thesis: A is_coarser_than C let a be set ; :: according to SETFAM_1:def_3 ::_thesis: ( not a in A or ex b1 being set st ( b1 in C & b1 c= a ) ) assume a in A ; ::_thesis: ex b1 being set st ( b1 in C & b1 c= a ) then consider b being set such that A3: b in B and A4: b c= a by A1, SETFAM_1:def_3; consider c being set such that A5: ( c in C & c c= b ) by A2, A3, SETFAM_1:def_3; take c ; ::_thesis: ( c in C & c c= a ) thus ( c in C & c c= a ) by A4, A5, XBOOLE_1:1; ::_thesis: verum end; LM: now__::_thesis:_for_I_being_non_empty_set_ for_M_being_ManySortedSet_of_I_holds_support_M_=__{__x_where_x_is_Element_of_I_:_M_._x_<>_{}__}_ let I be non empty set ; ::_thesis: for M being ManySortedSet of I holds support M = { x where x is Element of I : M . x <> {} } let M be ManySortedSet of I; ::_thesis: support M = { x where x is Element of I : M . x <> {} } set F = { x where x is Element of I : M . x <> {} } ; thus support M = { x where x is Element of I : M . x <> {} } ::_thesis: verum proof thus support M c= { x where x is Element of I : M . x <> {} } :: according to XBOOLE_0:def_10 ::_thesis: { x where x is Element of I : M . x <> {} } c= support M proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support M or x in { x where x is Element of I : M . x <> {} } ) A1: dom M = I by PARTFUN1:def_2; A2: support M c= dom M by PRE_POLY:37; assume A3: x in support M ; ::_thesis: x in { x where x is Element of I : M . x <> {} } then M . x <> {} by PRE_POLY:def_7; hence x in { x where x is Element of I : M . x <> {} } by A1, A2, A3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { x where x is Element of I : M . x <> {} } or x in support M ) assume x in { x where x is Element of I : M . x <> {} } ; ::_thesis: x in support M then ex i being Element of I st ( x = i & M . i <> {} ) ; hence x in support M by PRE_POLY:def_7; ::_thesis: verum end; end; definition let I be non empty set ; let M be ManySortedSet of I; :: original: support redefine func support M -> set equals :: CLOSURE3:def 1 { x where x is Element of I : M . x <> {} } ; compatibility for b1 being set holds ( b1 = support M iff b1 = { x where x is Element of I : M . x <> {} } ) by LM; end; :: deftheorem defines support CLOSURE3:def_1_:_ for I being non empty set for M being ManySortedSet of I holds support M = { x where x is Element of I : M . x <> {} } ; theorem :: CLOSURE3:5 for I being non empty set for M being V8() ManySortedSet of I holds M = ([[0]] I) +* (M | (support M)) proof let I be non empty set ; ::_thesis: for M being V8() ManySortedSet of I holds M = ([[0]] I) +* (M | (support M)) let M be V8() ManySortedSet of I; ::_thesis: M = ([[0]] I) +* (M | (support M)) set MM = M | (support M); A1: I c= support M proof let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in I or v in support M ) assume A2: v in I ; ::_thesis: v in support M then M . v <> {} ; hence v in support M by A2; ::_thesis: verum end; dom M = I by PARTFUN1:def_2; then M | (support M) = M by A1, RELAT_1:68; hence M = ([[0]] I) +* (M | (support M)) by Th1; ::_thesis: verum end; theorem :: CLOSURE3:6 for I being non empty set for M1, M2 being V8() ManySortedSet of I st M1 | (support M1) = M2 | (support M2) holds M1 = M2 proof let I be non empty set ; ::_thesis: for M1, M2 being V8() ManySortedSet of I st M1 | (support M1) = M2 | (support M2) holds M1 = M2 let M1, M2 be V8() ManySortedSet of I; ::_thesis: ( M1 | (support M1) = M2 | (support M2) implies M1 = M2 ) A1: dom M1 = I by PARTFUN1:def_2; A2: dom M2 = I by PARTFUN1:def_2; assume A3: M1 | (support M1) = M2 | (support M2) ; ::_thesis: M1 = M2 for x being set st x in I holds M1 . x = M2 . x proof let x be set ; ::_thesis: ( x in I implies M1 . x = M2 . x ) A4: dom (M2 | (support M2)) = (dom M2) /\ (support M2) by RELAT_1:61; assume A5: x in I ; ::_thesis: M1 . x = M2 . x then not M1 . x is empty ; then A6: x in support M1 by A5; not M2 . x is empty by A5; then x in support M2 by A5; then A7: x in dom (M2 | (support M2)) by A2, A5, A4, XBOOLE_0:def_4; dom (M1 | (support M1)) = (dom M1) /\ (support M1) by RELAT_1:61; then x in dom (M1 | (support M1)) by A1, A5, A6, XBOOLE_0:def_4; then M1 . x = (M2 | (support M2)) . x by A3, FUNCT_1:47 .= M2 . x by A7, FUNCT_1:47 ; hence M1 . x = M2 . x ; ::_thesis: verum end; hence M1 = M2 by A1, A2, FUNCT_1:2; ::_thesis: verum end; theorem :: CLOSURE3:7 canceled; theorem Th8: :: CLOSURE3:8 for I being non empty set for M being ManySortedSet of I for x being Element of Bool M for i being Element of I for y being set st y in x . i holds ex a being Element of Bool M st ( y in a . i & a is V42() & support a is finite & a c= x ) proof let I be non empty set ; ::_thesis: for M being ManySortedSet of I for x being Element of Bool M for i being Element of I for y being set st y in x . i holds ex a being Element of Bool M st ( y in a . i & a is V42() & support a is finite & a c= x ) let M be ManySortedSet of I; ::_thesis: for x being Element of Bool M for i being Element of I for y being set st y in x . i holds ex a being Element of Bool M st ( y in a . i & a is V42() & support a is finite & a c= x ) let x be Element of Bool M; ::_thesis: for i being Element of I for y being set st y in x . i holds ex a being Element of Bool M st ( y in a . i & a is V42() & support a is finite & a c= x ) let i be Element of I; ::_thesis: for y being set st y in x . i holds ex a being Element of Bool M st ( y in a . i & a is V42() & support a is finite & a c= x ) let y be set ; ::_thesis: ( y in x . i implies ex a being Element of Bool M st ( y in a . i & a is V42() & support a is finite & a c= x ) ) assume A1: y in x . i ; ::_thesis: ex a being Element of Bool M st ( y in a . i & a is V42() & support a is finite & a c= x ) set N = {i} --> {y}; set A = ([[0]] I) +* ({i} --> {y}); A2: dom ({i} --> {y}) = {i} by FUNCOP_1:13; then A3: i in dom ({i} --> {y}) by TARSKI:def_1; then A4: ({i} --> {y}) . i = {y} by A2, FUNCOP_1:7; then A5: (([[0]] I) +* ({i} --> {y})) . i = {y} by A3, FUNCT_4:13; A6: dom (([[0]] I) +* ({i} --> {y})) = (dom ([[0]] I)) \/ (dom ({i} --> {y})) by FUNCT_4:def_1 .= I \/ {i} by A2, PARTFUN1:def_2 .= I by ZFMISC_1:40 ; then reconsider A = ([[0]] I) +* ({i} --> {y}) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18; for j being set st j in I holds A . j c= M . j proof let j be set ; ::_thesis: ( j in I implies A . j c= M . j ) assume A7: j in I ; ::_thesis: A . j c= M . j percases ( i = j or i <> j ) ; supposeA8: i = j ; ::_thesis: A . j c= M . j reconsider x = x as ManySortedSubset of M ; let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in A . j or v in M . j ) assume v in A . j ; ::_thesis: v in M . j then v in {y} by A3, A4, A8, FUNCT_4:13; then A9: v in x . j by A1, A8, TARSKI:def_1; x c= M by PBOOLE:def_18; then x . j c= M . j by A7, PBOOLE:def_2; hence v in M . j by A9; ::_thesis: verum end; suppose i <> j ; ::_thesis: A . j c= M . j then A10: not j in {i} by TARSKI:def_1; j in (dom ([[0]] I)) \/ (dom ({i} --> {y})) by A6, A7, FUNCT_4:def_1; then A . j = (I --> {}) . j by A2, A10, FUNCT_4:def_1 .= {} by A7, FUNCOP_1:7 ; hence A . j c= M . j by XBOOLE_1:2; ::_thesis: verum end; end; end; then A c= M by PBOOLE:def_2; then reconsider AA = A as ManySortedSubset of M by PBOOLE:def_18; reconsider a = AA as Element of Bool M by CLOSURE2:def_1; A11: for j being set st j in I holds a . j c= x . j proof let j be set ; ::_thesis: ( j in I implies a . j c= x . j ) assume A12: j in I ; ::_thesis: a . j c= x . j percases ( i = j or j <> i ) ; supposeA13: i = j ; ::_thesis: a . j c= x . j let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in a . j or v in x . j ) assume A14: v in a . j ; ::_thesis: v in x . j a . j = {y} by A3, A4, A13, FUNCT_4:13; hence v in x . j by A1, A13, A14, TARSKI:def_1; ::_thesis: verum end; suppose j <> i ; ::_thesis: a . j c= x . j then A15: not j in {i} by TARSKI:def_1; j in (dom ([[0]] I)) \/ (dom ({i} --> {y})) by A6, A12, FUNCT_4:def_1; then a . j = (I --> {}) . j by A2, A15, FUNCT_4:def_1 .= {} by A12, FUNCOP_1:7 ; hence a . j c= x . j by XBOOLE_1:2; ::_thesis: verum end; end; end; A16: { b where b is Element of I : a . b <> {} } = {i} proof thus { b where b is Element of I : a . b <> {} } c= {i} :: according to XBOOLE_0:def_10 ::_thesis: {i} c= { b where b is Element of I : a . b <> {} } proof let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in { b where b is Element of I : a . b <> {} } or s in {i} ) assume s in { b where b is Element of I : a . b <> {} } ; ::_thesis: s in {i} then A17: ex b being Element of I st ( s = b & a . b <> {} ) ; assume A18: not s in {i} ; ::_thesis: contradiction reconsider s = s as Element of I by A17; s in dom a by A6; then s in (dom ([[0]] I)) \/ (dom ({i} --> {y})) by FUNCT_4:def_1; then a . s = (I --> {}) . s by A2, A18, FUNCT_4:def_1 .= {} by FUNCOP_1:7 ; hence contradiction by A17; ::_thesis: verum end; let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in {i} or s in { b where b is Element of I : a . b <> {} } ) assume A19: s in {i} ; ::_thesis: s in { b where b is Element of I : a . b <> {} } then A20: s = i by TARSKI:def_1; reconsider s = s as Element of I by A19, TARSKI:def_1; a . s = {y} by A3, A4, A20, FUNCT_4:13; hence s in { b where b is Element of I : a . b <> {} } ; ::_thesis: verum end; take a ; ::_thesis: ( y in a . i & a is V42() & support a is finite & a c= x ) for j being set st j in I holds a . j is finite proof let j be set ; ::_thesis: ( j in I implies a . j is finite ) assume A21: j in I ; ::_thesis: a . j is finite percases ( j = i or j <> i ) ; suppose j = i ; ::_thesis: a . j is finite hence a . j is finite by A3, A4, FUNCT_4:13; ::_thesis: verum end; suppose j <> i ; ::_thesis: a . j is finite then A22: not j in {i} by TARSKI:def_1; j in (dom ([[0]] I)) \/ (dom ({i} --> {y})) by A6, A21, FUNCT_4:def_1; then a . j = (I --> {}) . j by A2, A22, FUNCT_4:def_1 .= {} by A21, FUNCOP_1:7 ; hence a . j is finite ; ::_thesis: verum end; end; end; hence ( y in a . i & a is V42() & support a is finite & a c= x ) by A5, A16, A11, FINSET_1:def_5, PBOOLE:def_2, TARSKI:def_1; ::_thesis: verum end; definition let I be set ; let M be ManySortedSet of I; let A be SubsetFamily of M; func MSUnion A -> ManySortedSubset of M means :Def2: :: CLOSURE3:def 2 for i being set st i in I holds it . i = union { (f . i) where f is Element of Bool M : f in A } ; existence ex b1 being ManySortedSubset of M st for i being set st i in I holds b1 . i = union { (f . i) where f is Element of Bool M : f in A } proof defpred S1[ set , set ] means \$2 = union { (f . \$1) where f is Element of Bool M : f in A } ; A1: for x being set st x in I holds ex y being set st S1[x,y] ; consider IT being Function such that A2: dom IT = I and A3: for x being set st x in I holds S1[x,IT . x] from CLASSES1:sch_1(A1); reconsider IT = IT as ManySortedSet of I by A2, PARTFUN1:def_2, RELAT_1:def_18; for i being set st i in I holds IT . i c= M . i proof let i be set ; ::_thesis: ( i in I implies IT . i c= M . i ) assume A4: i in I ; ::_thesis: IT . i c= M . i for x being set st x in IT . i holds x in M . i proof let x be set ; ::_thesis: ( x in IT . i implies x in M . i ) assume A5: x in IT . i ; ::_thesis: x in M . i IT . i = union { (f . i) where f is Element of Bool M : f in A } by A3, A4; then consider Y being set such that A6: x in Y and A7: Y in { (f . i) where f is Element of Bool M : f in A } by A5, TARSKI:def_4; consider ff being Element of Bool M such that A8: ff . i = Y and ff in A by A7; reconsider ff = ff as ManySortedSubset of M ; ff c= M by PBOOLE:def_18; then ff . i c= M . i by A4, PBOOLE:def_2; hence x in M . i by A6, A8; ::_thesis: verum end; hence IT . i c= M . i by TARSKI:def_3; ::_thesis: verum end; then IT c= M by PBOOLE:def_2; then reconsider IT = IT as ManySortedSubset of M by PBOOLE:def_18; take IT ; ::_thesis: for i being set st i in I holds IT . i = union { (f . i) where f is Element of Bool M : f in A } thus for i being set st i in I holds IT . i = union { (f . i) where f is Element of Bool M : f in A } by A3; ::_thesis: verum end; uniqueness for b1, b2 being ManySortedSubset of M st ( for i being set st i in I holds b1 . i = union { (f . i) where f is Element of Bool M : f in A } ) & ( for i being set st i in I holds b2 . i = union { (f . i) where f is Element of Bool M : f in A } ) holds b1 = b2 proof let B1, B2 be ManySortedSubset of M; ::_thesis: ( ( for i being set st i in I holds B1 . i = union { (f . i) where f is Element of Bool M : f in A } ) & ( for i being set st i in I holds B2 . i = union { (f . i) where f is Element of Bool M : f in A } ) implies B1 = B2 ) assume that A9: for i being set st i in I holds B1 . i = union { (f . i) where f is Element of Bool M : f in A } and A10: for i being set st i in I holds B2 . i = union { (ff . i) where ff is Element of Bool M : ff in A } ; ::_thesis: B1 = B2 for i being set st i in I holds B1 . i = B2 . i proof let i be set ; ::_thesis: ( i in I implies B1 . i = B2 . i ) assume A11: i in I ; ::_thesis: B1 . i = B2 . i then B1 . i = union { (f . i) where f is Element of Bool M : f in A } by A9 .= B2 . i by A10, A11 ; hence B1 . i = B2 . i ; ::_thesis: verum end; hence B1 = B2 by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def2 defines MSUnion CLOSURE3:def_2_:_ for I being set for M being ManySortedSet of I for A being SubsetFamily of M for b4 being ManySortedSubset of M holds ( b4 = MSUnion A iff for i being set st i in I holds b4 . i = union { (f . i) where f is Element of Bool M : f in A } ); registration let I be set ; let M be ManySortedSet of I; let A be empty SubsetFamily of M; cluster MSUnion A -> V9() ; coherence MSUnion A is empty-yielding proof let i be set ; :: according to PBOOLE:def_12 ::_thesis: ( not i in I or (MSUnion A) . i is empty ) set MA = MSUnion A; assume i in I ; ::_thesis: (MSUnion A) . i is empty then A1: (MSUnion A) . i = union { (f . i) where f is Element of Bool M : f in A } by Def2; assume not (MSUnion A) . i is empty ; ::_thesis: contradiction then consider v being set such that A2: v in (MSUnion A) . i by XBOOLE_0:def_1; consider h being set such that v in h and A3: h in { (f . i) where f is Element of Bool M : f in A } by A1, A2, TARSKI:def_4; ex g being Element of Bool M st ( h = g . i & g in A ) by A3; hence contradiction ; ::_thesis: verum end; end; theorem :: CLOSURE3:9 for I being set for M being ManySortedSet of I for A being SubsetFamily of M holds MSUnion A = union |:A:| proof let I be set ; ::_thesis: for M being ManySortedSet of I for A being SubsetFamily of M holds MSUnion A = union |:A:| let M be ManySortedSet of I; ::_thesis: for A being SubsetFamily of M holds MSUnion A = union |:A:| let A be SubsetFamily of M; ::_thesis: MSUnion A = union |:A:| set AA = |:A:|; reconsider UA = union |:A:| as ManySortedSet of I ; percases ( not A is empty or A is empty SubsetFamily of M ) ; supposeA1: not A is empty ; ::_thesis: MSUnion A = union |:A:| for i being set st i in I holds (MSUnion A) . i = UA . i proof let i be set ; ::_thesis: ( i in I implies (MSUnion A) . i = UA . i ) assume A2: i in I ; ::_thesis: (MSUnion A) . i = UA . i then ( |:A:| . i = { (g . i) where g is Element of Bool M : g in A } & UA . i = union (|:A:| . i) ) by A1, CLOSURE2:14, MBOOLEAN:def_2; hence (MSUnion A) . i = UA . i by A2, Def2; ::_thesis: verum end; hence MSUnion A = union |:A:| by PBOOLE:3; ::_thesis: verum end; supposeA3: A is empty SubsetFamily of M ; ::_thesis: MSUnion A = union |:A:| for i being set st i in I holds (MSUnion A) . i = UA . i proof let i be set ; ::_thesis: ( i in I implies (MSUnion A) . i = UA . i ) assume i in I ; ::_thesis: (MSUnion A) . i = UA . i |:A:| = [[0]] I by A3, CLOSURE2:def_3; then UA = [[0]] I by MBOOLEAN:21; then UA . i is empty ; hence (MSUnion A) . i = UA . i by A3; ::_thesis: verum end; hence MSUnion A = union |:A:| by PBOOLE:3; ::_thesis: verum end; end; end; definition let I be set ; let M be ManySortedSet of I; let A, B be SubsetFamily of M; :: original: \/ redefine funcA \/ B -> SubsetFamily of M; correctness coherence A \/ B is SubsetFamily of M; by CLOSURE2:3; end; theorem :: CLOSURE3:10 for I being set for M being ManySortedSet of I for A, B being SubsetFamily of M holds MSUnion (A \/ B) = (MSUnion A) \/ (MSUnion B) proof let I be set ; ::_thesis: for M being ManySortedSet of I for A, B being SubsetFamily of M holds MSUnion (A \/ B) = (MSUnion A) \/ (MSUnion B) let M be ManySortedSet of I; ::_thesis: for A, B being SubsetFamily of M holds MSUnion (A \/ B) = (MSUnion A) \/ (MSUnion B) let A, B be SubsetFamily of M; ::_thesis: MSUnion (A \/ B) = (MSUnion A) \/ (MSUnion B) reconsider MAB = MSUnion (A \/ B) as ManySortedSubset of M ; reconsider MAB = MAB as ManySortedSet of I ; reconsider MA = MSUnion A as ManySortedSubset of M ; reconsider MA = MA as ManySortedSet of I ; reconsider MB = MSUnion B as ManySortedSubset of M ; reconsider MB = MB as ManySortedSet of I ; for i being set st i in I holds MAB . i = (MA \/ MB) . i proof let i be set ; ::_thesis: ( i in I implies MAB . i = (MA \/ MB) . i ) assume A1: i in I ; ::_thesis: MAB . i = (MA \/ MB) . i then A2: MAB . i = union { (f . i) where f is Element of Bool M : f in A \/ B } by Def2; A3: (MA \/ MB) . i = (MA . i) \/ (MB . i) by A1, PBOOLE:def_4; A4: for v being set st v in (MA \/ MB) . i holds v in MAB . i proof let v be set ; ::_thesis: ( v in (MA \/ MB) . i implies v in MAB . i ) assume v in (MA \/ MB) . i ; ::_thesis: v in MAB . i then A5: ( v in MA . i or v in MB . i ) by A3, XBOOLE_0:def_3; percases ( v in union { (f . i) where f is Element of Bool M : f in A } or v in union { (f . i) where f is Element of Bool M : f in B } ) by A1, A5, Def2; suppose v in union { (f . i) where f is Element of Bool M : f in A } ; ::_thesis: v in MAB . i then consider g being set such that A6: v in g and A7: g in { (f . i) where f is Element of Bool M : f in A } by TARSKI:def_4; consider h being Element of Bool M such that A8: g = h . i and A9: h in A by A7; h in A \/ B by A9, XBOOLE_0:def_3; then g in { (f . i) where f is Element of Bool M : f in A \/ B } by A8; hence v in MAB . i by A2, A6, TARSKI:def_4; ::_thesis: verum end; suppose v in union { (f . i) where f is Element of Bool M : f in B } ; ::_thesis: v in MAB . i then consider g being set such that A10: v in g and A11: g in { (f . i) where f is Element of Bool M : f in B } by TARSKI:def_4; consider h being Element of Bool M such that A12: g = h . i and A13: h in B by A11; h in A \/ B by A13, XBOOLE_0:def_3; then g in { (f . i) where f is Element of Bool M : f in A \/ B } by A12; hence v in MAB . i by A2, A10, TARSKI:def_4; ::_thesis: verum end; end; end; A14: ( MA . i = union { (f . i) where f is Element of Bool M : f in A } & MB . i = union { (f . i) where f is Element of Bool M : f in B } ) by A1, Def2; for v being set st v in MAB . i holds v in (MA \/ MB) . i proof let v be set ; ::_thesis: ( v in MAB . i implies v in (MA \/ MB) . i ) assume v in MAB . i ; ::_thesis: v in (MA \/ MB) . i then consider h being set such that A15: v in h and A16: h in { (f . i) where f is Element of Bool M : f in A \/ B } by A2, TARSKI:def_4; consider g being Element of Bool M such that A17: h = g . i and A18: g in A \/ B by A16; ( g in A or g in B ) by A18, XBOOLE_0:def_3; then ( h in { (f . i) where f is Element of Bool M : f in A } or h in { (f . i) where f is Element of Bool M : f in B } ) by A17; then ( v in union { (f . i) where f is Element of Bool M : f in A } or v in union { (f . i) where f is Element of Bool M : f in B } ) by A15, TARSKI:def_4; hence v in (MA \/ MB) . i by A3, A14, XBOOLE_0:def_3; ::_thesis: verum end; hence MAB . i = (MA \/ MB) . i by A4, TARSKI:1; ::_thesis: verum end; hence MSUnion (A \/ B) = (MSUnion A) \/ (MSUnion B) by PBOOLE:3; ::_thesis: verum end; theorem :: CLOSURE3:11 for I being set for M being ManySortedSet of I for A, B being SubsetFamily of M st A c= B holds MSUnion A c= MSUnion B proof let I be set ; ::_thesis: for M being ManySortedSet of I for A, B being SubsetFamily of M st A c= B holds MSUnion A c= MSUnion B let M be ManySortedSet of I; ::_thesis: for A, B being SubsetFamily of M st A c= B holds MSUnion A c= MSUnion B let A, B be SubsetFamily of M; ::_thesis: ( A c= B implies MSUnion A c= MSUnion B ) reconsider MA = MSUnion A as ManySortedSubset of M ; reconsider MA = MA as ManySortedSet of I ; reconsider MB = MSUnion B as ManySortedSubset of M ; reconsider MB = MB as ManySortedSet of I ; assume A1: A c= B ; ::_thesis: MSUnion A c= MSUnion B for i being set st i in I holds MA . i c= MB . i proof let i be set ; ::_thesis: ( i in I implies MA . i c= MB . i ) assume A2: i in I ; ::_thesis: MA . i c= MB . i for v being set st v in MA . i holds v in MB . i proof A3: MA . i = union { (f . i) where f is Element of Bool M : f in A } by A2, Def2; let v be set ; ::_thesis: ( v in MA . i implies v in MB . i ) assume v in MA . i ; ::_thesis: v in MB . i then consider h being set such that A4: v in h and A5: h in { (f . i) where f is Element of Bool M : f in A } by A3, TARSKI:def_4; ex g being Element of Bool M st ( h = g . i & g in A ) by A5; then h in { (k . i) where k is Element of Bool M : k in B } by A1; then v in union { (k . i) where k is Element of Bool M : k in B } by A4, TARSKI:def_4; hence v in MB . i by A2, Def2; ::_thesis: verum end; hence MA . i c= MB . i by TARSKI:def_3; ::_thesis: verum end; hence MSUnion A c= MSUnion B by PBOOLE:def_2; ::_thesis: verum end; definition let I be set ; let M be ManySortedSet of I; let A, B be SubsetFamily of M; :: original: /\ redefine funcA /\ B -> SubsetFamily of M; correctness coherence A /\ B is SubsetFamily of M; by CLOSURE2:4; end; theorem :: CLOSURE3:12 for I being set for M being ManySortedSet of I for A, B being SubsetFamily of M holds MSUnion (A /\ B) c= (MSUnion A) /\ (MSUnion B) proof let I be set ; ::_thesis: for M being ManySortedSet of I for A, B being SubsetFamily of M holds MSUnion (A /\ B) c= (MSUnion A) /\ (MSUnion B) let M be ManySortedSet of I; ::_thesis: for A, B being SubsetFamily of M holds MSUnion (A /\ B) c= (MSUnion A) /\ (MSUnion B) let A, B be SubsetFamily of M; ::_thesis: MSUnion (A /\ B) c= (MSUnion A) /\ (MSUnion B) reconsider MAB = MSUnion (A /\ B) as ManySortedSet of I ; reconsider MA = MSUnion A as ManySortedSet of I ; reconsider MB = MSUnion B as ManySortedSet of I ; for i being set st i in I holds MAB . i c= (MA /\ MB) . i proof let i be set ; ::_thesis: ( i in I implies MAB . i c= (MA /\ MB) . i ) assume A1: i in I ; ::_thesis: MAB . i c= (MA /\ MB) . i then A2: ( MA . i = union { (f . i) where f is Element of Bool M : f in A } & MB . i = union { (f . i) where f is Element of Bool M : f in B } ) by Def2; A3: MAB . i = union { (f . i) where f is Element of Bool M : f in A /\ B } by A1, Def2; for v being set st v in MAB . i holds v in (MA /\ MB) . i proof let v be set ; ::_thesis: ( v in MAB . i implies v in (MA /\ MB) . i ) assume v in MAB . i ; ::_thesis: v in (MA /\ MB) . i then consider w being set such that A4: v in w and A5: w in { (f . i) where f is Element of Bool M : f in A /\ B } by A3, TARSKI:def_4; consider g being Element of Bool M such that A6: w = g . i and A7: g in A /\ B by A5; g in B by A7, XBOOLE_0:def_4; then w in { (f . i) where f is Element of Bool M : f in B } by A6; then A8: v in union { (f . i) where f is Element of Bool M : f in B } by A4, TARSKI:def_4; g in A by A7, XBOOLE_0:def_4; then w in { (f . i) where f is Element of Bool M : f in A } by A6; then v in union { (f . i) where f is Element of Bool M : f in A } by A4, TARSKI:def_4; then v in (MA . i) /\ (MB . i) by A2, A8, XBOOLE_0:def_4; hence v in (MA /\ MB) . i by A1, PBOOLE:def_5; ::_thesis: verum end; hence MAB . i c= (MA /\ MB) . i by TARSKI:def_3; ::_thesis: verum end; hence MSUnion (A /\ B) c= (MSUnion A) /\ (MSUnion B) by PBOOLE:def_2; ::_thesis: verum end; theorem :: CLOSURE3:13 for I being set for M being ManySortedSet of I for AA being set st ( for x being set st x in AA holds x is SubsetFamily of M ) holds for A, B being SubsetFamily of M st B = { (MSUnion X) where X is SubsetFamily of M : X in AA } & A = union AA holds MSUnion B = MSUnion A proof let I be set ; ::_thesis: for M being ManySortedSet of I for AA being set st ( for x being set st x in AA holds x is SubsetFamily of M ) holds for A, B being SubsetFamily of M st B = { (MSUnion X) where X is SubsetFamily of M : X in AA } & A = union AA holds MSUnion B = MSUnion A let M be ManySortedSet of I; ::_thesis: for AA being set st ( for x being set st x in AA holds x is SubsetFamily of M ) holds for A, B being SubsetFamily of M st B = { (MSUnion X) where X is SubsetFamily of M : X in AA } & A = union AA holds MSUnion B = MSUnion A let AA be set ; ::_thesis: ( ( for x being set st x in AA holds x is SubsetFamily of M ) implies for A, B being SubsetFamily of M st B = { (MSUnion X) where X is SubsetFamily of M : X in AA } & A = union AA holds MSUnion B = MSUnion A ) assume A1: for x being set st x in AA holds x is SubsetFamily of M ; ::_thesis: for A, B being SubsetFamily of M st B = { (MSUnion X) where X is SubsetFamily of M : X in AA } & A = union AA holds MSUnion B = MSUnion A let A, B be SubsetFamily of M; ::_thesis: ( B = { (MSUnion X) where X is SubsetFamily of M : X in AA } & A = union AA implies MSUnion B = MSUnion A ) assume that A2: B = { (MSUnion X) where X is SubsetFamily of M : X in AA } and A3: A = union AA ; ::_thesis: MSUnion B = MSUnion A let i be set ; :: according to PBOOLE:def_10 ::_thesis: ( not i in I or (MSUnion B) . i = (MSUnion A) . i ) assume A4: i in I ; ::_thesis: (MSUnion B) . i = (MSUnion A) . i thus (MSUnion B) . i c= (MSUnion A) . i :: according to XBOOLE_0:def_10 ::_thesis: (MSUnion A) . i c= (MSUnion B) . i proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (MSUnion B) . i or a in (MSUnion A) . i ) thus ( a in (MSUnion B) . i implies a in (MSUnion A) . i ) ::_thesis: verum proof assume a in (MSUnion B) . i ; ::_thesis: a in (MSUnion A) . i then a in union { (f . i) where f is Element of Bool M : f in B } by A4, Def2; then consider Y being set such that A5: a in Y and A6: Y in { (f . i) where f is Element of Bool M : f in B } by TARSKI:def_4; consider f being Element of Bool M such that A7: f . i = Y and A8: f in B by A6; consider Q being SubsetFamily of M such that A9: f = MSUnion Q and A10: Q in AA by A2, A8; (MSUnion Q) . i = union { (g . i) where g is Element of Bool M : g in Q } by A4, Def2; then consider d being set such that A11: a in d and A12: d in { (g . i) where g is Element of Bool M : g in Q } by A5, A7, A9, TARSKI:def_4; consider g being Element of Bool M such that A13: d = g . i and A14: g in Q by A12; g in union AA by A10, A14, TARSKI:def_4; then d in { (h . i) where h is Element of Bool M : h in union AA } by A13; then a in union { (h . i) where h is Element of Bool M : h in union AA } by A11, TARSKI:def_4; hence a in (MSUnion A) . i by A3, A4, Def2; ::_thesis: verum end; end; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (MSUnion A) . i or a in (MSUnion B) . i ) assume a in (MSUnion A) . i ; ::_thesis: a in (MSUnion B) . i then a in union { (f . i) where f is Element of Bool M : f in A } by A4, Def2; then consider Y being set such that A15: a in Y and A16: Y in { (f . i) where f is Element of Bool M : f in A } by TARSKI:def_4; consider f being Element of Bool M such that A17: f . i = Y and A18: f in A by A16; consider c being set such that A19: f in c and A20: c in AA by A3, A18, TARSKI:def_4; reconsider c = c as SubsetFamily of M by A1, A20; f . i in { (v . i) where v is Element of Bool M : v in c } by A19; then A21: a in union { (v . i) where v is Element of Bool M : v in c } by A15, A17, TARSKI:def_4; (MSUnion c) . i = union { (v . i) where v is Element of Bool M : v in c } by A4, Def2; then consider cos being set such that A22: a in cos and A23: cos = (MSUnion c) . i by A21; MSUnion c in { (MSUnion X) where X is SubsetFamily of M : X in AA } by A20; then cos in { (t . i) where t is Element of Bool M : t in B } by A2, A23; then a in union { (t . i) where t is Element of Bool M : t in B } by A22, TARSKI:def_4; hence a in (MSUnion B) . i by A4, Def2; ::_thesis: verum end; begin definition let I be non empty set ; let M be ManySortedSet of I; let S be SetOp of M; attrS is algebraic means :: CLOSURE3:def 3 for x being Element of Bool M st x = S . x holds ex A being SubsetFamily of M st ( A = { (S . a) where a is Element of Bool M : ( a is V42() & support a is finite & a c= x ) } & x = MSUnion A ); end; :: deftheorem defines algebraic CLOSURE3:def_3_:_ for I being non empty set for M being ManySortedSet of I for S being SetOp of M holds ( S is algebraic iff for x being Element of Bool M st x = S . x holds ex A being SubsetFamily of M st ( A = { (S . a) where a is Element of Bool M : ( a is V42() & support a is finite & a c= x ) } & x = MSUnion A ) ); registration let I be non empty set ; let M be ManySortedSet of I; cluster non empty Relation-like Bool M -defined Bool M -valued Function-like V17( Bool M) quasi_total reflexive monotonic idempotent algebraic for Element of bool [:(Bool M),(Bool M):]; existence ex b1 being SetOp of M st ( b1 is algebraic & b1 is reflexive & b1 is monotonic & b1 is idempotent ) proof reconsider f = id (Bool M) as SetOp of M ; take f ; ::_thesis: ( f is algebraic & f is reflexive & f is monotonic & f is idempotent ) thus f is algebraic ::_thesis: ( f is reflexive & f is monotonic & f is idempotent ) proof let x be Element of Bool M; :: according to CLOSURE3:def_3 ::_thesis: ( x = f . x implies ex A being SubsetFamily of M st ( A = { (f . a) where a is Element of Bool M : ( a is V42() & support a is finite & a c= x ) } & x = MSUnion A ) ) assume x = f . x ; ::_thesis: ex A being SubsetFamily of M st ( A = { (f . a) where a is Element of Bool M : ( a is V42() & support a is finite & a c= x ) } & x = MSUnion A ) set A = { (f . a) where a is Element of Bool M : ( a is V42() & support a is finite & a c= x ) } ; { (f . a) where a is Element of Bool M : ( a is V42() & support a is finite & a c= x ) } c= Bool M proof let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in { (f . a) where a is Element of Bool M : ( a is V42() & support a is finite & a c= x ) } or v in Bool M ) assume v in { (f . a) where a is Element of Bool M : ( a is V42() & support a is finite & a c= x ) } ; ::_thesis: v in Bool M then ex a being Element of Bool M st ( v = f . a & a is V42() & support a is finite & a c= x ) ; hence v in Bool M ; ::_thesis: verum end; then reconsider A = { (f . a) where a is Element of Bool M : ( a is V42() & support a is finite & a c= x ) } as SubsetFamily of M ; take A ; ::_thesis: ( A = { (f . a) where a is Element of Bool M : ( a is V42() & support a is finite & a c= x ) } & x = MSUnion A ) thus A = { (f . a) where a is Element of Bool M : ( a is V42() & support a is finite & a c= x ) } ; ::_thesis: x = MSUnion A let i be Element of I; :: according to PBOOLE:def_21 ::_thesis: x . i = (MSUnion A) . i thus x . i c= (MSUnion A) . i :: according to XBOOLE_0:def_10 ::_thesis: (MSUnion A) . i c= x . i proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in x . i or y in (MSUnion A) . i ) assume y in x . i ; ::_thesis: y in (MSUnion A) . i then consider a being Element of Bool M such that A1: y in a . i and A2: ( a is V42() & support a is finite & a c= x ) by Th8; a = f . a by FUNCT_1:18; then a in A by A2; then a . i in { (g . i) where g is Element of Bool M : g in A } ; then y in union { (g . i) where g is Element of Bool M : g in A } by A1, TARSKI:def_4; hence y in (MSUnion A) . i by Def2; ::_thesis: verum end; let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in (MSUnion A) . i or v in x . i ) assume v in (MSUnion A) . i ; ::_thesis: v in x . i then v in union { (ff . i) where ff is Element of Bool M : ff in A } by Def2; then consider Y being set such that A3: v in Y and A4: Y in { (ff . i) where ff is Element of Bool M : ff in A } by TARSKI:def_4; consider ff being Element of Bool M such that A5: Y = ff . i and A6: ff in A by A4; consider a being Element of Bool M such that A7: ff = f . a and a is V42() and support a is finite and A8: a c= x by A6; ff = a by A7, FUNCT_1:18; then ff . i c= x . i by A8, PBOOLE:def_2; hence v in x . i by A3, A5; ::_thesis: verum end; thus f is reflexive ::_thesis: ( f is monotonic & f is idempotent ) proof let X be Element of Bool M; :: according to CLOSURE2:def_10 ::_thesis: X c= f . X thus X c= f . X by FUNCT_1:18; ::_thesis: verum end; thus f is monotonic ::_thesis: f is idempotent proof let X, Y be Element of Bool M; :: according to CLOSURE2:def_11 ::_thesis: ( not X c= Y or f . X c= f . Y ) assume A9: X c= Y ; ::_thesis: f . X c= f . Y f . X = X by FUNCT_1:18; hence f . X c= f . Y by A9, FUNCT_1:18; ::_thesis: verum end; thus f is idempotent ::_thesis: verum proof let X be Element of Bool M; :: according to CLOSURE2:def_12 ::_thesis: f . X = f . (f . X) thus f . (f . X) = f . X by FUNCT_1:18; ::_thesis: verum end; end; end; definition let S be non empty 1-sorted ; let IT be ClosureSystem of S; attrIT is algebraic means :: CLOSURE3:def 4 ClSys->ClOp IT is algebraic ; end; :: deftheorem defines algebraic CLOSURE3:def_4_:_ for S being non empty 1-sorted for IT being ClosureSystem of S holds ( IT is algebraic iff ClSys->ClOp IT is algebraic ); definition let S be non empty non void ManySortedSign ; let MA be non-empty MSAlgebra over S; func SubAlgCl MA -> strict ClosureStr over 1-sorted(# the carrier of S #) means :Def5: :: CLOSURE3:def 5 ( the Sorts of it = the Sorts of MA & the Family of it = SubSort MA ); existence ex b1 being strict ClosureStr over 1-sorted(# the carrier of S #) st ( the Sorts of b1 = the Sorts of MA & the Family of b1 = SubSort MA ) proof reconsider SS = the Sorts of MA as ManySortedSet of the carrier of 1-sorted(# the carrier of S #) ; SubSort MA c= Bool the Sorts of MA proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SubSort MA or x in Bool the Sorts of MA ) assume x in SubSort MA ; ::_thesis: x in Bool the Sorts of MA then x is ManySortedSubset of the Sorts of MA by MSUALG_2:def_11; hence x in Bool the Sorts of MA by CLOSURE2:def_1; ::_thesis: verum end; then reconsider SF = SubSort MA as SubsetFamily of SS ; take ClosureStr(# SS,SF #) ; ::_thesis: ( the Sorts of ClosureStr(# SS,SF #) = the Sorts of MA & the Family of ClosureStr(# SS,SF #) = SubSort MA ) thus ( the Sorts of ClosureStr(# SS,SF #) = the Sorts of MA & the Family of ClosureStr(# SS,SF #) = SubSort MA ) ; ::_thesis: verum end; uniqueness for b1, b2 being strict ClosureStr over 1-sorted(# the carrier of S #) st the Sorts of b1 = the Sorts of MA & the Family of b1 = SubSort MA & the Sorts of b2 = the Sorts of MA & the Family of b2 = SubSort MA holds b1 = b2 ; end; :: deftheorem Def5 defines SubAlgCl CLOSURE3:def_5_:_ for S being non empty non void ManySortedSign for MA being non-empty MSAlgebra over S for b3 being strict ClosureStr over 1-sorted(# the carrier of S #) holds ( b3 = SubAlgCl MA iff ( the Sorts of b3 = the Sorts of MA & the Family of b3 = SubSort MA ) ); theorem Th14: :: CLOSURE3:14 for S being non empty non void ManySortedSign for MA being strict non-empty MSAlgebra over S holds SubSort MA is absolutely-multiplicative SubsetFamily of the Sorts of MA proof let S be non empty non void ManySortedSign ; ::_thesis: for MA being strict non-empty MSAlgebra over S holds SubSort MA is absolutely-multiplicative SubsetFamily of the Sorts of MA let MA be strict non-empty MSAlgebra over S; ::_thesis: SubSort MA is absolutely-multiplicative SubsetFamily of the Sorts of MA SubSort MA c= Bool the Sorts of MA proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SubSort MA or x in Bool the Sorts of MA ) assume x in SubSort MA ; ::_thesis: x in Bool the Sorts of MA then x is ManySortedSubset of the Sorts of MA by MSUALG_2:def_11; hence x in Bool the Sorts of MA by CLOSURE2:def_1; ::_thesis: verum end; then reconsider SUBMA = SubSort MA as SubsetFamily of the Sorts of MA ; for F being SubsetFamily of the Sorts of MA st F c= SUBMA holds meet |:F:| in SUBMA proof set M = bool (Union the Sorts of MA); set I = the carrier of S; let F be SubsetFamily of the Sorts of MA; ::_thesis: ( F c= SUBMA implies meet |:F:| in SUBMA ) assume A1: F c= SUBMA ; ::_thesis: meet |:F:| in SUBMA set x = meet |:F:|; A2: dom (meet |:F:|) = the carrier of S by PARTFUN1:def_2; rng (meet |:F:|) c= bool (Union the Sorts of MA) proof let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in rng (meet |:F:|) or u in bool (Union the Sorts of MA) ) assume u in rng (meet |:F:|) ; ::_thesis: u in bool (Union the Sorts of MA) then consider i being set such that A3: i in dom (meet |:F:|) and A4: u = (meet |:F:|) . i by FUNCT_1:def_3; dom the Sorts of MA = the carrier of S by PARTFUN1:def_2; then the Sorts of MA . i in rng the Sorts of MA by A2, A3, FUNCT_1:def_3; then A5: the Sorts of MA . i c= union (rng the Sorts of MA) by ZFMISC_1:74; ex Q being Subset-Family of ( the Sorts of MA . i) st ( Q = |:F:| . i & u = Intersect Q ) by A2, A3, A4, MSSUBFAM:def_1; then u c= union (rng the Sorts of MA) by A5, XBOOLE_1:1; then u in bool (union (rng the Sorts of MA)) ; hence u in bool (Union the Sorts of MA) by CARD_3:def_4; ::_thesis: verum end; then A6: meet |:F:| in Funcs ( the carrier of S,(bool (Union the Sorts of MA))) by A2, FUNCT_2:def_2; reconsider x = meet |:F:| as MSSubset of MA ; for B being MSSubset of MA st B = x holds B is opers_closed by A1, Th3; hence meet |:F:| in SUBMA by A6, MSUALG_2:def_11; ::_thesis: verum end; hence SubSort MA is absolutely-multiplicative SubsetFamily of the Sorts of MA by CLOSURE2:def_7; ::_thesis: verum end; registration let S be non empty non void ManySortedSign ; let MA be strict non-empty MSAlgebra over S; cluster SubAlgCl MA -> strict absolutely-multiplicative ; coherence SubAlgCl MA is absolutely-multiplicative proof thus SubAlgCl MA is absolutely-multiplicative ::_thesis: verum proof reconsider SF = SubSort MA as absolutely-multiplicative SubsetFamily of the Sorts of MA by Th14; set F = the Family of (SubAlgCl MA); ( the Sorts of (SubAlgCl MA) = the Sorts of MA & the Family of (SubAlgCl MA) = SF ) by Def5; hence SubAlgCl MA is absolutely-multiplicative ; ::_thesis: verum end; end; end; registration let S be non empty non void ManySortedSign ; let MA be strict non-empty MSAlgebra over S; cluster SubAlgCl MA -> strict algebraic ; coherence SubAlgCl MA is algebraic proof set I = the carrier of S; set SS = ClSys->ClOp (SubAlgCl MA); set M = the Sorts of (SubAlgCl MA); let x be Element of Bool the Sorts of (SubAlgCl MA); :: according to CLOSURE3:def_3,CLOSURE3:def_4 ::_thesis: ( x = (ClSys->ClOp (SubAlgCl MA)) . x implies ex A being SubsetFamily of the Sorts of (SubAlgCl MA) st ( A = { ((ClSys->ClOp (SubAlgCl MA)) . a) where a is Element of Bool the Sorts of (SubAlgCl MA) : ( a is V42() & support a is finite & a c= x ) } & x = MSUnion A ) ) assume A1: x = (ClSys->ClOp (SubAlgCl MA)) . x ; ::_thesis: ex A being SubsetFamily of the Sorts of (SubAlgCl MA) st ( A = { ((ClSys->ClOp (SubAlgCl MA)) . a) where a is Element of Bool the Sorts of (SubAlgCl MA) : ( a is V42() & support a is finite & a c= x ) } & x = MSUnion A ) set A = { ((ClSys->ClOp (SubAlgCl MA)) . a) where a is Element of Bool the Sorts of (SubAlgCl MA) : ( a is V42() & support a is finite & a c= x ) } ; { ((ClSys->ClOp (SubAlgCl MA)) . a) where a is Element of Bool the Sorts of (SubAlgCl MA) : ( a is V42() & support a is finite & a c= x ) } c= Bool the Sorts of (SubAlgCl MA) proof let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in { ((ClSys->ClOp (SubAlgCl MA)) . a) where a is Element of Bool the Sorts of (SubAlgCl MA) : ( a is V42() & support a is finite & a c= x ) } or v in Bool the Sorts of (SubAlgCl MA) ) assume v in { ((ClSys->ClOp (SubAlgCl MA)) . a) where a is Element of Bool the Sorts of (SubAlgCl MA) : ( a is V42() & support a is finite & a c= x ) } ; ::_thesis: v in Bool the Sorts of (SubAlgCl MA) then ex a being Element of Bool the Sorts of (SubAlgCl MA) st ( v = (ClSys->ClOp (SubAlgCl MA)) . a & a is V42() & support a is finite & a c= x ) ; then reconsider vv = v as Element of Bool the Sorts of (SubAlgCl MA) ; vv in Bool the Sorts of (SubAlgCl MA) ; hence v in Bool the Sorts of (SubAlgCl MA) ; ::_thesis: verum end; then reconsider A = { ((ClSys->ClOp (SubAlgCl MA)) . a) where a is Element of Bool the Sorts of (SubAlgCl MA) : ( a is V42() & support a is finite & a c= x ) } as SubsetFamily of the Sorts of (SubAlgCl MA) ; take A ; ::_thesis: ( A = { ((ClSys->ClOp (SubAlgCl MA)) . a) where a is Element of Bool the Sorts of (SubAlgCl MA) : ( a is V42() & support a is finite & a c= x ) } & x = MSUnion A ) thus A = { ((ClSys->ClOp (SubAlgCl MA)) . b) where b is Element of Bool the Sorts of (SubAlgCl MA) : ( b is V42() & support b is finite & b c= x ) } ; ::_thesis: x = MSUnion A reconsider y = x, z = MSUnion A as ManySortedSet of the carrier of S ; y = z proof let i be Element of the carrier of S; :: according to PBOOLE:def_21 ::_thesis: y . i = z . i reconsider SS9 = ClSys->ClOp (SubAlgCl MA) as reflexive SetOp of the Sorts of (SubAlgCl MA) ; thus y . i c= z . i :: according to XBOOLE_0:def_10 ::_thesis: z . i c= y . i proof let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in y . i or v in z . i ) assume v in y . i ; ::_thesis: v in z . i then consider b being Element of Bool the Sorts of (SubAlgCl MA) such that A2: v in b . i and A3: ( b is V42() & support b is finite & b c= x ) by Th8; b c=' SS9 . b by CLOSURE2:def_10; then A4: b . i c= (SS9 . b) . i by PBOOLE:def_2; (ClSys->ClOp (SubAlgCl MA)) . b in A by A3; then (SS9 . b) . i in { (f . i) where f is Element of Bool the Sorts of (SubAlgCl MA) : f in A } ; then v in union { (f . i) where f is Element of Bool the Sorts of (SubAlgCl MA) : f in A } by A2, A4, TARSKI:def_4; hence v in z . i by Def2; ::_thesis: verum end; reconsider SS9 = ClSys->ClOp (SubAlgCl MA) as monotonic SetOp of the Sorts of (SubAlgCl MA) ; let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in z . i or v in y . i ) assume v in z . i ; ::_thesis: v in y . i then v in union { (ff . i) where ff is Element of Bool the Sorts of (SubAlgCl MA) : ff in A } by Def2; then consider Y being set such that A5: v in Y and A6: Y in { (ff . i) where ff is Element of Bool the Sorts of (SubAlgCl MA) : ff in A } by TARSKI:def_4; consider ff being Element of Bool the Sorts of (SubAlgCl MA) such that A7: Y = ff . i and A8: ff in A by A6; consider a being Element of Bool the Sorts of (SubAlgCl MA) such that A9: ff = (ClSys->ClOp (SubAlgCl MA)) . a and a is V42() and support a is finite and A10: a c=' x by A8; SS9 . a c=' SS9 . x by A10, CLOSURE2:def_11; then ff . i c= x . i by A1, A9, PBOOLE:def_2; hence v in y . i by A5, A7; ::_thesis: verum end; hence x = MSUnion A ; ::_thesis: verum end; end;