:: OSALG_2 semantic presentation begin theorem Th1: :: OSALG_2:1 for R being non empty Poset for X, Y being OrderSortedSet of R holds X /\ Y is OrderSortedSet of R proof let R be non empty Poset; ::_thesis: for X, Y being OrderSortedSet of R holds X /\ Y is OrderSortedSet of R let X, Y be OrderSortedSet of R; ::_thesis: X /\ Y is OrderSortedSet of R reconsider M = X /\ Y as ManySortedSet of R ; M is order-sorted proof let s1, s2 be Element of R; :: according to OSALG_1:def_16 ::_thesis: ( not s1 <= s2 or M . s1 c= M . s2 ) assume s1 <= s2 ; ::_thesis: M . s1 c= M . s2 then A1: ( X . s1 c= X . s2 & Y . s1 c= Y . s2 ) by OSALG_1:def_16; ( (X /\ Y) . s1 = (X . s1) /\ (Y . s1) & (X /\ Y) . s2 = (X . s2) /\ (Y . s2) ) by PBOOLE:def_5; hence M . s1 c= M . s2 by A1, XBOOLE_1:27; ::_thesis: verum end; hence X /\ Y is OrderSortedSet of R ; ::_thesis: verum end; theorem Th2: :: OSALG_2:2 for R being non empty Poset for X, Y being OrderSortedSet of R holds X \/ Y is OrderSortedSet of R proof let R be non empty Poset; ::_thesis: for X, Y being OrderSortedSet of R holds X \/ Y is OrderSortedSet of R let X, Y be OrderSortedSet of R; ::_thesis: X \/ Y is OrderSortedSet of R reconsider M = X \/ Y as ManySortedSet of R ; M is order-sorted proof let s1, s2 be Element of R; :: according to OSALG_1:def_16 ::_thesis: ( not s1 <= s2 or M . s1 c= M . s2 ) assume s1 <= s2 ; ::_thesis: M . s1 c= M . s2 then A1: ( X . s1 c= X . s2 & Y . s1 c= Y . s2 ) by OSALG_1:def_16; ( (X \/ Y) . s1 = (X . s1) \/ (Y . s1) & (X \/ Y) . s2 = (X . s2) \/ (Y . s2) ) by PBOOLE:def_4; hence M . s1 c= M . s2 by A1, XBOOLE_1:13; ::_thesis: verum end; hence X \/ Y is OrderSortedSet of R ; ::_thesis: verum end; definition let R be non empty Poset; let M be OrderSortedSet of R; mode OrderSortedSubset of M -> ManySortedSubset of M means :Def1: :: OSALG_2:def 1 it is OrderSortedSet of R; existence ex b1 being ManySortedSubset of M st b1 is OrderSortedSet of R proof reconsider X = M as ManySortedSubset of M by PBOOLE:def_18; take X ; ::_thesis: X is OrderSortedSet of R thus X is OrderSortedSet of R ; ::_thesis: verum end; end; :: deftheorem Def1 defines OrderSortedSubset OSALG_2:def_1_:_ for R being non empty Poset for M being OrderSortedSet of R for b3 being ManySortedSubset of M holds ( b3 is OrderSortedSubset of M iff b3 is OrderSortedSet of R ); registration let R be non empty Poset; let M be V8() OrderSortedSet of R; cluster non empty Relation-like V8() the carrier of R -defined Function-like V17( the carrier of R) for OrderSortedSubset of M; existence not for b1 being OrderSortedSubset of M holds b1 is V8() proof reconsider N = M as ManySortedSubset of M by PBOOLE:def_18; reconsider N1 = N as OrderSortedSubset of M by Def1; take N1 ; ::_thesis: N1 is V8() thus N1 is V8() ; ::_thesis: verum end; end; begin definition let S be OrderSortedSign; let U0 be OSAlgebra of S; mode OSSubset of U0 -> ManySortedSubset of the Sorts of U0 means :Def2: :: OSALG_2:def 2 it is OrderSortedSet of S; existence ex b1 being ManySortedSubset of the Sorts of U0 st b1 is OrderSortedSet of S proof reconsider B = the Sorts of U0 as MSSubset of U0 by PBOOLE:def_18; take B ; ::_thesis: B is OrderSortedSet of S thus B is OrderSortedSet of S by OSALG_1:17; ::_thesis: verum end; end; :: deftheorem Def2 defines OSSubset OSALG_2:def_2_:_ for S being OrderSortedSign for U0 being OSAlgebra of S for b3 being ManySortedSubset of the Sorts of U0 holds ( b3 is OSSubset of U0 iff b3 is OrderSortedSet of S ); registration let S be OrderSortedSign; cluster strict non-empty order-sorted monotone for MSAlgebra over S; existence ex b1 being OSAlgebra of S st ( b1 is monotone & b1 is strict & b1 is non-empty ) proof set z1 = the Element of {{}}; take TrivialOSA (S,{{}}, the Element of {{}}) ; ::_thesis: ( TrivialOSA (S,{{}}, the Element of {{}}) is monotone & TrivialOSA (S,{{}}, the Element of {{}}) is strict & TrivialOSA (S,{{}}, the Element of {{}}) is non-empty ) thus ( TrivialOSA (S,{{}}, the Element of {{}}) is monotone & TrivialOSA (S,{{}}, the Element of {{}}) is strict & TrivialOSA (S,{{}}, the Element of {{}}) is non-empty ) ; ::_thesis: verum end; end; registration let S be OrderSortedSign; let U0 be non-empty OSAlgebra of S; cluster non empty Relation-like V8() the carrier of S -defined Function-like V17( the carrier of S) for OSSubset of U0; existence not for b1 being OSSubset of U0 holds b1 is V8() proof reconsider N = the Sorts of U0 as MSSubset of U0 by PBOOLE:def_18; the Sorts of U0 is OrderSortedSet of S by OSALG_1:17; then reconsider M = N as OSSubset of U0 by Def2; take M ; ::_thesis: M is V8() thus M is V8() ; ::_thesis: verum end; end; theorem Th3: :: OSALG_2:3 for S0 being non empty non void strict all-with_const_op ManySortedSign holds OSSign S0 is all-with_const_op proof let S0 be non empty non void strict all-with_const_op ManySortedSign ; ::_thesis: OSSign S0 is all-with_const_op let s be Element of (OSSign S0); :: according to MSUALG_2:def_2 ::_thesis: s is with_const_op reconsider s1 = s as Element of S0 by OSALG_1:def_5; s1 is with_const_op by MSUALG_2:def_2; then consider o being Element of the carrier' of S0 such that A1: ( the Arity of S0 . o = {} & the ResultSort of S0 . o = s1 ) by MSUALG_2:def_1; A2: o is Element of the carrier' of (OSSign S0) by OSALG_1:def_5; ( the Arity of (OSSign S0) . o = {} & the ResultSort of (OSSign S0) . o = s1 ) by A1, OSALG_1:def_5; hence s is with_const_op by A2, MSUALG_2:def_1; ::_thesis: verum end; registration cluster non empty non void V52() all-with_const_op V99() V100() V101() strict order-sorted discernable for OverloadedRSSign ; existence ex b1 being OrderSortedSign st ( b1 is all-with_const_op & b1 is strict ) proof set S0 = the non empty non void strict all-with_const_op ManySortedSign ; take OSSign the non empty non void strict all-with_const_op ManySortedSign ; ::_thesis: ( OSSign the non empty non void strict all-with_const_op ManySortedSign is all-with_const_op & OSSign the non empty non void strict all-with_const_op ManySortedSign is strict ) thus ( OSSign the non empty non void strict all-with_const_op ManySortedSign is all-with_const_op & OSSign the non empty non void strict all-with_const_op ManySortedSign is strict ) by Th3; ::_thesis: verum end; end; begin theorem Th4: :: OSALG_2:4 for S being OrderSortedSign for U0 being OSAlgebra of S holds MSAlgebra(# the Sorts of U0, the Charact of U0 #) is order-sorted proof let S be OrderSortedSign; ::_thesis: for U0 being OSAlgebra of S holds MSAlgebra(# the Sorts of U0, the Charact of U0 #) is order-sorted let U0 be OSAlgebra of S; ::_thesis: MSAlgebra(# the Sorts of U0, the Charact of U0 #) is order-sorted the Sorts of U0 is OrderSortedSet of S by OSALG_1:17; hence MSAlgebra(# the Sorts of U0, the Charact of U0 #) is order-sorted by OSALG_1:17; ::_thesis: verum end; registration let S be OrderSortedSign; let U0 be OSAlgebra of S; cluster order-sorted for MSSubAlgebra of U0; existence ex b1 being MSSubAlgebra of U0 st b1 is order-sorted proof reconsider U1 = MSAlgebra(# the Sorts of U0, the Charact of U0 #) as strict MSSubAlgebra of U0 by MSUALG_2:37; take U1 ; ::_thesis: U1 is order-sorted thus U1 is order-sorted by Th4; ::_thesis: verum end; end; definition let S be OrderSortedSign; let U0 be OSAlgebra of S; mode OSSubAlgebra of U0 is order-sorted MSSubAlgebra of U0; end; registration let S be OrderSortedSign; let U0 be OSAlgebra of S; cluster strict order-sorted for MSSubAlgebra of U0; existence ex b1 being OSSubAlgebra of U0 st b1 is strict proof reconsider U1 = MSAlgebra(# the Sorts of U0, the Charact of U0 #) as order-sorted MSSubAlgebra of U0 by Th4, MSUALG_2:37; take U1 ; ::_thesis: U1 is strict thus U1 is strict ; ::_thesis: verum end; end; registration let S be OrderSortedSign; let U0 be non-empty OSAlgebra of S; cluster strict non-empty order-sorted for MSSubAlgebra of U0; existence ex b1 being OSSubAlgebra of U0 st ( b1 is non-empty & b1 is strict ) proof set U1 = MSAlgebra(# the Sorts of U0, the Charact of U0 #); the Sorts of U0 is OrderSortedSet of S by OSALG_1:17; then reconsider U1 = MSAlgebra(# the Sorts of U0, the Charact of U0 #) as strict OSSubAlgebra of U0 by MSUALG_2:37, OSALG_1:17; take U1 ; ::_thesis: ( U1 is non-empty & U1 is strict ) thus ( U1 is non-empty & U1 is strict ) ; ::_thesis: verum end; end; theorem Th5: :: OSALG_2:5 for S being OrderSortedSign for U0 being OSAlgebra of S for U1 being MSAlgebra over S holds ( U1 is OSSubAlgebra of U0 iff ( the Sorts of U1 is OSSubset of U0 & ( for B being OSSubset of U0 st B = the Sorts of U1 holds ( B is opers_closed & the Charact of U1 = Opers (U0,B) ) ) ) ) proof let S be OrderSortedSign; ::_thesis: for U0 being OSAlgebra of S for U1 being MSAlgebra over S holds ( U1 is OSSubAlgebra of U0 iff ( the Sorts of U1 is OSSubset of U0 & ( for B being OSSubset of U0 st B = the Sorts of U1 holds ( B is opers_closed & the Charact of U1 = Opers (U0,B) ) ) ) ) let U0 be OSAlgebra of S; ::_thesis: for U1 being MSAlgebra over S holds ( U1 is OSSubAlgebra of U0 iff ( the Sorts of U1 is OSSubset of U0 & ( for B being OSSubset of U0 st B = the Sorts of U1 holds ( B is opers_closed & the Charact of U1 = Opers (U0,B) ) ) ) ) let U1 be MSAlgebra over S; ::_thesis: ( U1 is OSSubAlgebra of U0 iff ( the Sorts of U1 is OSSubset of U0 & ( for B being OSSubset of U0 st B = the Sorts of U1 holds ( B is opers_closed & the Charact of U1 = Opers (U0,B) ) ) ) ) hereby ::_thesis: ( the Sorts of U1 is OSSubset of U0 & ( for B being OSSubset of U0 st B = the Sorts of U1 holds ( B is opers_closed & the Charact of U1 = Opers (U0,B) ) ) implies U1 is OSSubAlgebra of U0 ) assume A1: U1 is OSSubAlgebra of U0 ; ::_thesis: ( the Sorts of U1 is OSSubset of U0 & ( for B being OSSubset of U0 st B = the Sorts of U1 holds ( B is opers_closed & the Charact of U1 = Opers (U0,B) ) ) ) then ( the Sorts of U1 is OrderSortedSet of S & the Sorts of U1 is MSSubset of U0 ) by MSUALG_2:def_9, OSALG_1:17; hence the Sorts of U1 is OSSubset of U0 by Def2; ::_thesis: for B being OSSubset of U0 st B = the Sorts of U1 holds ( B is opers_closed & the Charact of U1 = Opers (U0,B) ) let B be OSSubset of U0; ::_thesis: ( B = the Sorts of U1 implies ( B is opers_closed & the Charact of U1 = Opers (U0,B) ) ) assume B = the Sorts of U1 ; ::_thesis: ( B is opers_closed & the Charact of U1 = Opers (U0,B) ) hence ( B is opers_closed & the Charact of U1 = Opers (U0,B) ) by A1, MSUALG_2:def_9; ::_thesis: verum end; assume A2: the Sorts of U1 is OSSubset of U0 ; ::_thesis: ( ex B being OSSubset of U0 st ( B = the Sorts of U1 & not ( B is opers_closed & the Charact of U1 = Opers (U0,B) ) ) or U1 is OSSubAlgebra of U0 ) assume A3: for B being OSSubset of U0 st B = the Sorts of U1 holds ( B is opers_closed & the Charact of U1 = Opers (U0,B) ) ; ::_thesis: U1 is OSSubAlgebra of U0 A4: U1 is MSSubAlgebra of U0 proof thus the Sorts of U1 is MSSubset of U0 by A2; :: according to MSUALG_2:def_9 ::_thesis: for b1 being ManySortedSubset of the Sorts of U0 holds ( not b1 = the Sorts of U1 or ( b1 is opers_closed & the Charact of U1 = Opers (U0,b1) ) ) let B be MSSubset of U0; ::_thesis: ( not B = the Sorts of U1 or ( B is opers_closed & the Charact of U1 = Opers (U0,B) ) ) assume A5: B = the Sorts of U1 ; ::_thesis: ( B is opers_closed & the Charact of U1 = Opers (U0,B) ) reconsider B1 = B as OSSubset of U0 by A2, A5; B1 is opers_closed by A3, A5; hence ( B is opers_closed & the Charact of U1 = Opers (U0,B) ) by A3, A5; ::_thesis: verum end; the Sorts of U1 is OrderSortedSet of S by A2, Def2; hence U1 is OSSubAlgebra of U0 by A4, OSALG_1:17; ::_thesis: verum end; definition let S1 be OrderSortedSign; let OU0 be OSAlgebra of S1; let s be SortSymbol of S1; func OSConstants (OU0,s) -> Subset of ( the Sorts of OU0 . s) equals :: OSALG_2:def 3 union { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s } ; coherence union { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s } is Subset of ( the Sorts of OU0 . s) proof set Cs = { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s } ; for X being set st X in { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s } holds X c= the Sorts of OU0 . s proof let X be set ; ::_thesis: ( X in { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s } implies X c= the Sorts of OU0 . s ) assume X in { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s } ; ::_thesis: X c= the Sorts of OU0 . s then consider s2 being SortSymbol of S1 such that A1: X = Constants (OU0,s2) and A2: s2 <= s ; the Sorts of OU0 . s2 c= the Sorts of OU0 . s by A2, OSALG_1:def_17; hence X c= the Sorts of OU0 . s by A1, XBOOLE_1:1; ::_thesis: verum end; hence union { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s } is Subset of ( the Sorts of OU0 . s) by ZFMISC_1:76; ::_thesis: verum end; end; :: deftheorem defines OSConstants OSALG_2:def_3_:_ for S1 being OrderSortedSign for OU0 being OSAlgebra of S1 for s being SortSymbol of S1 holds OSConstants (OU0,s) = union { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s } ; theorem Th6: :: OSALG_2:6 for S1 being OrderSortedSign for OU0 being OSAlgebra of S1 for s being SortSymbol of S1 holds Constants (OU0,s) c= OSConstants (OU0,s) proof let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1 for s being SortSymbol of S1 holds Constants (OU0,s) c= OSConstants (OU0,s) let OU0 be OSAlgebra of S1; ::_thesis: for s being SortSymbol of S1 holds Constants (OU0,s) c= OSConstants (OU0,s) let s be SortSymbol of S1; ::_thesis: Constants (OU0,s) c= OSConstants (OU0,s) Constants (OU0,s) in { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s } ; hence Constants (OU0,s) c= OSConstants (OU0,s) by ZFMISC_1:74; ::_thesis: verum end; definition let S1 be OrderSortedSign; let M be ManySortedSet of the carrier of S1; func OSCl M -> OrderSortedSet of S1 means :Def4: :: OSALG_2:def 4 for s being SortSymbol of S1 holds it . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } ; existence ex b1 being OrderSortedSet of S1 st for s being SortSymbol of S1 holds b1 . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } proof deffunc H1( Element of S1) -> set = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= \$1 } ; consider f being Function such that A1: ( dom f = the carrier of S1 & ( for d being Element of S1 holds f . d = H1(d) ) ) from FUNCT_1:sch_4(); reconsider f = f as ManySortedSet of the carrier of S1 by A1, PARTFUN1:def_2, RELAT_1:def_18; reconsider f1 = f as ManySortedSet of S1 ; f1 is order-sorted proof let r1, r2 be Element of S1; :: according to OSALG_1:def_16 ::_thesis: ( not r1 <= r2 or f1 . r1 c= f1 . r2 ) assume A2: r1 <= r2 ; ::_thesis: f1 . r1 c= f1 . r2 let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f1 . r1 or x in f1 . r2 ) assume x in f1 . r1 ; ::_thesis: x in f1 . r2 then x in union { (M . s2) where s2 is SortSymbol of S1 : s2 <= r1 } by A1; then consider y being set such that A3: ( x in y & y in { (M . s2) where s2 is SortSymbol of S1 : s2 <= r1 } ) by TARSKI:def_4; consider s3 being SortSymbol of S1 such that A4: y = M . s3 and A5: s3 <= r1 by A3; s3 <= r2 by A2, A5, ORDERS_2:3; then y in { (M . s2) where s2 is SortSymbol of S1 : s2 <= r2 } by A4; then x in union { (M . s2) where s2 is SortSymbol of S1 : s2 <= r2 } by A3, TARSKI:def_4; hence x in f1 . r2 by A1; ::_thesis: verum end; then reconsider f2 = f1 as OrderSortedSet of S1 ; take f2 ; ::_thesis: for s being SortSymbol of S1 holds f2 . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } thus for s being SortSymbol of S1 holds f2 . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } by A1; ::_thesis: verum end; uniqueness for b1, b2 being OrderSortedSet of S1 st ( for s being SortSymbol of S1 holds b1 . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } ) & ( for s being SortSymbol of S1 holds b2 . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } ) holds b1 = b2 proof let W1, W2 be OrderSortedSet of S1; ::_thesis: ( ( for s being SortSymbol of S1 holds W1 . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } ) & ( for s being SortSymbol of S1 holds W2 . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } ) implies W1 = W2 ) assume A6: for s being SortSymbol of S1 holds W1 . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } ; ::_thesis: ( ex s being SortSymbol of S1 st not W2 . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } or W1 = W2 ) assume A7: for s being SortSymbol of S1 holds W2 . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } ; ::_thesis: W1 = W2 for s being set st s in the carrier of S1 holds W1 . s = W2 . s proof let s be set ; ::_thesis: ( s in the carrier of S1 implies W1 . s = W2 . s ) assume s in the carrier of S1 ; ::_thesis: W1 . s = W2 . s then reconsider t = s as SortSymbol of S1 ; W1 . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= t } by A6 .= W2 . s by A7 ; hence W1 . s = W2 . s ; ::_thesis: verum end; hence W1 = W2 by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def4 defines OSCl OSALG_2:def_4_:_ for S1 being OrderSortedSign for M being ManySortedSet of the carrier of S1 for b3 being OrderSortedSet of S1 holds ( b3 = OSCl M iff for s being SortSymbol of S1 holds b3 . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } ); theorem Th7: :: OSALG_2:7 for S1 being OrderSortedSign for M being ManySortedSet of the carrier of S1 holds M c= OSCl M proof let S1 be OrderSortedSign; ::_thesis: for M being ManySortedSet of the carrier of S1 holds M c= OSCl M let M be ManySortedSet of the carrier of S1; ::_thesis: M c= OSCl M let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S1 or M . i c= (OSCl M) . i ) assume i in the carrier of S1 ; ::_thesis: M . i c= (OSCl M) . i then reconsider s = i as SortSymbol of S1 ; M . s in { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } ; then M . s c= union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } by ZFMISC_1:74; hence M . i c= (OSCl M) . i by Def4; ::_thesis: verum end; theorem Th8: :: OSALG_2:8 for S1 being OrderSortedSign for M being ManySortedSet of the carrier of S1 for A being OrderSortedSet of S1 st M c= A holds OSCl M c= A proof let S1 be OrderSortedSign; ::_thesis: for M being ManySortedSet of the carrier of S1 for A being OrderSortedSet of S1 st M c= A holds OSCl M c= A let M be ManySortedSet of the carrier of S1; ::_thesis: for A being OrderSortedSet of S1 st M c= A holds OSCl M c= A let A be OrderSortedSet of S1; ::_thesis: ( M c= A implies OSCl M c= A ) assume A1: M c= A ; ::_thesis: OSCl M c= A assume not OSCl M c= A ; ::_thesis: contradiction then consider i being set such that A2: i in the carrier of S1 and A3: not (OSCl M) . i c= A . i by PBOOLE:def_2; reconsider s = i as SortSymbol of S1 by A2; consider x being set such that A4: x in (OSCl M) . i and A5: not x in A . i by A3, TARSKI:def_3; (OSCl M) . s = union { (M . s2) where s2 is SortSymbol of S1 : s2 <= s } by Def4; then consider X1 being set such that A6: x in X1 and A7: X1 in { (M . s2) where s2 is SortSymbol of S1 : s2 <= s } by A4, TARSKI:def_4; consider s1 being SortSymbol of S1 such that A8: X1 = M . s1 and A9: s1 <= s by A7; M . s1 c= A . s1 by A1, PBOOLE:def_2; then A10: x in A . s1 by A6, A8; A . s1 c= A . s by A9, OSALG_1:def_16; hence contradiction by A5, A10; ::_thesis: verum end; theorem :: OSALG_2:9 for S being OrderSortedSign for X being OrderSortedSet of S holds OSCl X = X proof let S be OrderSortedSign; ::_thesis: for X being OrderSortedSet of S holds OSCl X = X let X be OrderSortedSet of S; ::_thesis: OSCl X = X ( X c= OSCl X & OSCl X c= X ) by Th7, Th8; hence OSCl X = X by PBOOLE:146; ::_thesis: verum end; definition let S1 be OrderSortedSign; let OU0 be OSAlgebra of S1; func OSConstants OU0 -> OSSubset of OU0 means :Def5: :: OSALG_2:def 5 for s being SortSymbol of S1 holds it . s = OSConstants (OU0,s); existence ex b1 being OSSubset of OU0 st for s being SortSymbol of S1 holds b1 . s = OSConstants (OU0,s) proof deffunc H1( Element of S1) -> set = union { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= \$1 } ; consider f being Function such that A1: ( dom f = the carrier of S1 & ( for d being Element of S1 holds f . d = H1(d) ) ) from FUNCT_1:sch_4(); reconsider f = f as ManySortedSet of the carrier of S1 by A1, PARTFUN1:def_2, RELAT_1:def_18; f c= the Sorts of OU0 proof let s be set ; :: according to PBOOLE:def_2 ::_thesis: ( not s in the carrier of S1 or f . s c= the Sorts of OU0 . s ) assume s in the carrier of S1 ; ::_thesis: f . s c= the Sorts of OU0 . s then reconsider s1 = s as SortSymbol of S1 ; f . s1 = OSConstants (OU0,s1) by A1; hence f . s c= the Sorts of OU0 . s ; ::_thesis: verum end; then reconsider f = f as MSSubset of OU0 by PBOOLE:def_18; take f ; ::_thesis: ( f is OSSubset of OU0 & ( for s being SortSymbol of S1 holds f . s = OSConstants (OU0,s) ) ) reconsider f1 = f as ManySortedSet of S1 ; f1 is order-sorted proof let r1, r2 be Element of S1; :: according to OSALG_1:def_16 ::_thesis: ( not r1 <= r2 or f1 . r1 c= f1 . r2 ) assume A2: r1 <= r2 ; ::_thesis: f1 . r1 c= f1 . r2 let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f1 . r1 or x in f1 . r2 ) assume x in f1 . r1 ; ::_thesis: x in f1 . r2 then x in union { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= r1 } by A1; then consider y being set such that A3: ( x in y & y in { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= r1 } ) by TARSKI:def_4; consider s3 being SortSymbol of S1 such that A4: y = Constants (OU0,s3) and A5: s3 <= r1 by A3; s3 <= r2 by A2, A5, ORDERS_2:3; then y in { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= r2 } by A4; then x in union { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= r2 } by A3, TARSKI:def_4; hence x in f1 . r2 by A1; ::_thesis: verum end; hence f is OSSubset of OU0 by Def2; ::_thesis: for s being SortSymbol of S1 holds f . s = OSConstants (OU0,s) thus for s being SortSymbol of S1 holds f . s = OSConstants (OU0,s) by A1; ::_thesis: verum end; uniqueness for b1, b2 being OSSubset of OU0 st ( for s being SortSymbol of S1 holds b1 . s = OSConstants (OU0,s) ) & ( for s being SortSymbol of S1 holds b2 . s = OSConstants (OU0,s) ) holds b1 = b2 proof let W1, W2 be OSSubset of OU0; ::_thesis: ( ( for s being SortSymbol of S1 holds W1 . s = OSConstants (OU0,s) ) & ( for s being SortSymbol of S1 holds W2 . s = OSConstants (OU0,s) ) implies W1 = W2 ) assume that A6: for s being SortSymbol of S1 holds W1 . s = OSConstants (OU0,s) and A7: for s being SortSymbol of S1 holds W2 . s = OSConstants (OU0,s) ; ::_thesis: W1 = W2 for s being set st s in the carrier of S1 holds W1 . s = W2 . s proof let s be set ; ::_thesis: ( s in the carrier of S1 implies W1 . s = W2 . s ) assume s in the carrier of S1 ; ::_thesis: W1 . s = W2 . s then reconsider t = s as SortSymbol of S1 ; W1 . t = OSConstants (OU0,t) by A6; hence W1 . s = W2 . s by A7; ::_thesis: verum end; hence W1 = W2 by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def5 defines OSConstants OSALG_2:def_5_:_ for S1 being OrderSortedSign for OU0 being OSAlgebra of S1 for b3 being OSSubset of OU0 holds ( b3 = OSConstants OU0 iff for s being SortSymbol of S1 holds b3 . s = OSConstants (OU0,s) ); theorem Th10: :: OSALG_2:10 for S1 being OrderSortedSign for OU0 being OSAlgebra of S1 holds Constants OU0 c= OSConstants OU0 proof let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1 holds Constants OU0 c= OSConstants OU0 let OU0 be OSAlgebra of S1; ::_thesis: Constants OU0 c= OSConstants OU0 let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S1 or (Constants OU0) . i c= (OSConstants OU0) . i ) assume i in the carrier of S1 ; ::_thesis: (Constants OU0) . i c= (OSConstants OU0) . i then reconsider s = i as SortSymbol of S1 ; ( (Constants OU0) . s = Constants (OU0,s) & (OSConstants OU0) . s = OSConstants (OU0,s) ) by Def5, MSUALG_2:def_4; hence (Constants OU0) . i c= (OSConstants OU0) . i by Th6; ::_thesis: verum end; theorem Th11: :: OSALG_2:11 for S1 being OrderSortedSign for OU0 being OSAlgebra of S1 for A being OSSubset of OU0 st Constants OU0 c= A holds OSConstants OU0 c= A proof let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1 for A being OSSubset of OU0 st Constants OU0 c= A holds OSConstants OU0 c= A let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0 st Constants OU0 c= A holds OSConstants OU0 c= A let A be OSSubset of OU0; ::_thesis: ( Constants OU0 c= A implies OSConstants OU0 c= A ) assume A1: Constants OU0 c= A ; ::_thesis: OSConstants OU0 c= A assume not OSConstants OU0 c= A ; ::_thesis: contradiction then consider i being set such that A2: i in the carrier of S1 and A3: not (OSConstants OU0) . i c= A . i by PBOOLE:def_2; reconsider s = i as SortSymbol of S1 by A2; consider x being set such that A4: x in (OSConstants OU0) . i and A5: not x in A . i by A3, TARSKI:def_3; (OSConstants OU0) . s = OSConstants (OU0,s) by Def5 .= union { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s } ; then consider X1 being set such that A6: x in X1 and A7: X1 in { (Constants (OU0,s2)) where s2 is SortSymbol of S1 : s2 <= s } by A4, TARSKI:def_4; consider s1 being SortSymbol of S1 such that A8: X1 = Constants (OU0,s1) and A9: s1 <= s by A7; A10: (Constants OU0) . s1 c= A . s1 by A1, PBOOLE:def_2; x in (Constants OU0) . s1 by A6, A8, MSUALG_2:def_4; then A11: x in A . s1 by A10; A is OrderSortedSet of S1 by Def2; then A . s1 c= A . s by A9, OSALG_1:def_16; hence contradiction by A5, A11; ::_thesis: verum end; theorem :: OSALG_2:12 for S1 being OrderSortedSign for OU0 being OSAlgebra of S1 for A being OSSubset of OU0 holds OSConstants OU0 = OSCl (Constants OU0) proof let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1 for A being OSSubset of OU0 holds OSConstants OU0 = OSCl (Constants OU0) let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0 holds OSConstants OU0 = OSCl (Constants OU0) let A be OSSubset of OU0; ::_thesis: OSConstants OU0 = OSCl (Constants OU0) A1: now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S1_holds_ (OSConstants_OU0)_._i_=_(OSCl_(Constants_OU0))_._i let i be set ; ::_thesis: ( i in the carrier of S1 implies (OSConstants OU0) . i = (OSCl (Constants OU0)) . i ) assume i in the carrier of S1 ; ::_thesis: (OSConstants OU0) . i = (OSCl (Constants OU0)) . i then reconsider s = i as SortSymbol of S1 ; set c1 = { ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s } ; set c2 = { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } ; for x being set holds ( x in { ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s } iff x in { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } ) proof let x be set ; ::_thesis: ( x in { ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s } iff x in { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } ) hereby ::_thesis: ( x in { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } implies x in { ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s } ) assume x in { ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s } ; ::_thesis: x in { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } then consider s1 being SortSymbol of S1 such that A2: x = (Constants OU0) . s1 and A3: s1 <= s ; x = Constants (OU0,s1) by A2, MSUALG_2:def_4; hence x in { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } by A3; ::_thesis: verum end; assume x in { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } ; ::_thesis: x in { ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s } then consider s1 being SortSymbol of S1 such that A4: x = Constants (OU0,s1) and A5: s1 <= s ; x = (Constants OU0) . s1 by A4, MSUALG_2:def_4; hence x in { ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s } by A5; ::_thesis: verum end; then A6: { ((Constants OU0) . s1) where s1 is SortSymbol of S1 : s1 <= s } = { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } by TARSKI:1; (OSConstants OU0) . s = OSConstants (OU0,s) by Def5 .= (OSCl (Constants OU0)) . s by A6, Def4 ; hence (OSConstants OU0) . i = (OSCl (Constants OU0)) . i ; ::_thesis: verum end; then for i being set st i in the carrier of S1 holds (OSCl (Constants OU0)) . i c= (OSConstants OU0) . i ; then A7: OSCl (Constants OU0) c= OSConstants OU0 by PBOOLE:def_2; for i being set st i in the carrier of S1 holds (OSConstants OU0) . i c= (OSCl (Constants OU0)) . i by A1; then OSConstants OU0 c= OSCl (Constants OU0) by PBOOLE:def_2; hence OSConstants OU0 = OSCl (Constants OU0) by A7, PBOOLE:146; ::_thesis: verum end; theorem Th13: :: OSALG_2:13 for S1 being OrderSortedSign for OU0 being OSAlgebra of S1 for OU1 being OSSubAlgebra of OU0 holds OSConstants OU0 is OSSubset of OU1 proof let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1 for OU1 being OSSubAlgebra of OU0 holds OSConstants OU0 is OSSubset of OU1 let OU0 be OSAlgebra of S1; ::_thesis: for OU1 being OSSubAlgebra of OU0 holds OSConstants OU0 is OSSubset of OU1 let OU1 be OSSubAlgebra of OU0; ::_thesis: OSConstants OU0 is OSSubset of OU1 OSConstants OU0 c= the Sorts of OU1 proof let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S1 or (OSConstants OU0) . i c= the Sorts of OU1 . i ) assume i in the carrier of S1 ; ::_thesis: (OSConstants OU0) . i c= the Sorts of OU1 . i then reconsider s = i as SortSymbol of S1 ; Constants OU0 is MSSubset of OU1 by MSUALG_2:10; then A1: Constants OU0 c= the Sorts of OU1 by PBOOLE:def_18; A2: for s2, s3 being SortSymbol of S1 st s2 <= s3 holds (Constants OU0) . s2 c= the Sorts of OU1 . s3 proof let s2, s3 be SortSymbol of S1; ::_thesis: ( s2 <= s3 implies (Constants OU0) . s2 c= the Sorts of OU1 . s3 ) assume s2 <= s3 ; ::_thesis: (Constants OU0) . s2 c= the Sorts of OU1 . s3 then A3: the Sorts of OU1 . s2 c= the Sorts of OU1 . s3 by OSALG_1:def_17; (Constants OU0) . s2 c= the Sorts of OU1 . s2 by A1, PBOOLE:def_2; hence (Constants OU0) . s2 c= the Sorts of OU1 . s3 by A3, XBOOLE_1:1; ::_thesis: verum end; A4: for X being set st X in { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } holds X c= the Sorts of OU1 . s proof let X be set ; ::_thesis: ( X in { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } implies X c= the Sorts of OU1 . s ) assume X in { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } ; ::_thesis: X c= the Sorts of OU1 . s then consider s4 being SortSymbol of S1 such that A5: ( X = Constants (OU0,s4) & s4 <= s ) ; Constants (OU0,s4) = (Constants OU0) . s4 by MSUALG_2:def_4; hence X c= the Sorts of OU1 . s by A2, A5; ::_thesis: verum end; (OSConstants OU0) . i = OSConstants (OU0,s) by Def5 .= union { (Constants (OU0,s1)) where s1 is SortSymbol of S1 : s1 <= s } ; hence (OSConstants OU0) . i c= the Sorts of OU1 . i by A4, ZFMISC_1:76; ::_thesis: verum end; then A6: OSConstants OU0 is ManySortedSubset of the Sorts of OU1 by PBOOLE:def_18; OSConstants OU0 is OrderSortedSet of S1 by Def2; hence OSConstants OU0 is OSSubset of OU1 by A6, Def2; ::_thesis: verum end; theorem :: OSALG_2:14 for S being all-with_const_op OrderSortedSign for OU0 being non-empty OSAlgebra of S for OU1 being non-empty OSSubAlgebra of OU0 holds OSConstants OU0 is V8() OSSubset of OU1 proof let S be all-with_const_op OrderSortedSign; ::_thesis: for OU0 being non-empty OSAlgebra of S for OU1 being non-empty OSSubAlgebra of OU0 holds OSConstants OU0 is V8() OSSubset of OU1 let OU0 be non-empty OSAlgebra of S; ::_thesis: for OU1 being non-empty OSSubAlgebra of OU0 holds OSConstants OU0 is V8() OSSubset of OU1 let OU1 be non-empty OSSubAlgebra of OU0; ::_thesis: OSConstants OU0 is V8() OSSubset of OU1 Constants OU0 c= OSConstants OU0 by Th10; hence OSConstants OU0 is V8() OSSubset of OU1 by Th13, PBOOLE:131; ::_thesis: verum end; begin theorem Th15: :: OSALG_2:15 for I being set for M being ManySortedSet of I for x being set holds ( x is ManySortedSubset of M iff x in product (bool M) ) proof let I be set ; ::_thesis: for M being ManySortedSet of I for x being set holds ( x is ManySortedSubset of M iff x in product (bool M) ) let M be ManySortedSet of I; ::_thesis: for x being set holds ( x is ManySortedSubset of M iff x in product (bool M) ) let x be set ; ::_thesis: ( x is ManySortedSubset of M iff x in product (bool M) ) A1: I = dom (bool M) by PARTFUN1:def_2; hereby ::_thesis: ( x in product (bool M) implies x is ManySortedSubset of M ) assume x is ManySortedSubset of M ; ::_thesis: x in product (bool M) then reconsider x1 = x as ManySortedSubset of M ; A2: for i being set st i in dom (bool M) holds x1 . i in (bool M) . i proof let i be set ; ::_thesis: ( i in dom (bool M) implies x1 . i in (bool M) . i ) assume A3: i in dom (bool M) ; ::_thesis: x1 . i in (bool M) . i x1 c= M by PBOOLE:def_18; then x1 . i c= M . i by A1, A3, PBOOLE:def_2; then x1 . i in bool (M . i) ; hence x1 . i in (bool M) . i by A1, A3, MBOOLEAN:def_1; ::_thesis: verum end; dom x1 = I by PARTFUN1:def_2 .= dom (bool M) by PARTFUN1:def_2 ; hence x in product (bool M) by A2, CARD_3:def_5; ::_thesis: verum end; assume x in product (bool M) ; ::_thesis: x is ManySortedSubset of M then consider x1 being Function such that A4: x = x1 and A5: dom x1 = dom (bool M) and A6: for i being set st i in dom (bool M) holds x1 . i in (bool M) . i by CARD_3:def_5; dom x1 = I by A5, PARTFUN1:def_2; then reconsider x2 = x1 as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18; x2 c= M proof let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or x2 . i c= M . i ) assume A7: i in I ; ::_thesis: x2 . i c= M . i x2 . i in (bool M) . i by A1, A6, A7; then x2 . i in bool (M . i) by A7, MBOOLEAN:def_1; hence x2 . i c= M . i ; ::_thesis: verum end; hence x is ManySortedSubset of M by A4, PBOOLE:def_18; ::_thesis: verum end; definition let R be non empty Poset; let M be OrderSortedSet of R; func OSbool M -> set means :: OSALG_2:def 6 for x being set holds ( x in it iff x is OrderSortedSubset of M ); existence ex b1 being set st for x being set holds ( x in b1 iff x is OrderSortedSubset of M ) proof defpred S1[ set ] means \$1 is OrderSortedSubset of M; set f = product (bool M); consider X being set such that A1: for y being set holds ( y in X iff ( y in product (bool M) & S1[y] ) ) from XBOOLE_0:sch_1(); take X ; ::_thesis: for x being set holds ( x in X iff x is OrderSortedSubset of M ) let y be set ; ::_thesis: ( y in X iff y is OrderSortedSubset of M ) thus ( y in X implies y is OrderSortedSubset of M ) by A1; ::_thesis: ( y is OrderSortedSubset of M implies y in X ) assume A2: y is OrderSortedSubset of M ; ::_thesis: y in X then y in product (bool M) by Th15; hence y in X by A1, A2; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff x is OrderSortedSubset of M ) ) & ( for x being set holds ( x in b2 iff x is OrderSortedSubset of M ) ) holds b1 = b2 proof defpred S1[ set ] means \$1 is OrderSortedSubset of M; thus for X1, X2 being set st ( for x being set holds ( x in X1 iff S1[x] ) ) & ( for x being set holds ( x in X2 iff S1[x] ) ) holds X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum end; end; :: deftheorem defines OSbool OSALG_2:def_6_:_ for R being non empty Poset for M being OrderSortedSet of R for b3 being set holds ( b3 = OSbool M iff for x being set holds ( x in b3 iff x is OrderSortedSubset of M ) ); definition let S be OrderSortedSign; let U0 be OSAlgebra of S; let A be OSSubset of U0; func OSSubSort A -> set equals :: OSALG_2:def 7 { x where x is Element of SubSort A : x is OrderSortedSet of S } ; correctness coherence { x where x is Element of SubSort A : x is OrderSortedSet of S } is set ; ; end; :: deftheorem defines OSSubSort OSALG_2:def_7_:_ for S being OrderSortedSign for U0 being OSAlgebra of S for A being OSSubset of U0 holds OSSubSort A = { x where x is Element of SubSort A : x is OrderSortedSet of S } ; theorem Th16: :: OSALG_2:16 for S1 being OrderSortedSign for OU0 being OSAlgebra of S1 for A being OSSubset of OU0 holds OSSubSort A c= SubSort A proof let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1 for A being OSSubset of OU0 holds OSSubSort A c= SubSort A let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0 holds OSSubSort A c= SubSort A let A be OSSubset of OU0; ::_thesis: OSSubSort A c= SubSort A let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in OSSubSort A or x in SubSort A ) assume x in OSSubSort A ; ::_thesis: x in SubSort A then ex y being Element of SubSort A st ( x = y & y is OrderSortedSet of S1 ) ; hence x in SubSort A ; ::_thesis: verum end; theorem Th17: :: OSALG_2:17 for S1 being OrderSortedSign for OU0 being OSAlgebra of S1 for A being OSSubset of OU0 holds the Sorts of OU0 in OSSubSort A proof let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1 for A being OSSubset of OU0 holds the Sorts of OU0 in OSSubSort A let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0 holds the Sorts of OU0 in OSSubSort A let A be OSSubset of OU0; ::_thesis: the Sorts of OU0 in OSSubSort A reconsider X = the Sorts of OU0 as Element of SubSort A by MSUALG_2:38; the Sorts of OU0 is OrderSortedSet of S1 by OSALG_1:17; then X in { x where x is Element of SubSort A : x is OrderSortedSet of S1 } ; hence the Sorts of OU0 in OSSubSort A ; ::_thesis: verum end; registration let S1 be OrderSortedSign; let OU0 be OSAlgebra of S1; let A be OSSubset of OU0; cluster OSSubSort A -> non empty ; coherence not OSSubSort A is empty by Th17; end; definition let S1 be OrderSortedSign; let OU0 be OSAlgebra of S1; func OSSubSort OU0 -> set equals :: OSALG_2:def 8 { x where x is Element of SubSort OU0 : x is OrderSortedSet of S1 } ; correctness coherence { x where x is Element of SubSort OU0 : x is OrderSortedSet of S1 } is set ; ; end; :: deftheorem defines OSSubSort OSALG_2:def_8_:_ for S1 being OrderSortedSign for OU0 being OSAlgebra of S1 holds OSSubSort OU0 = { x where x is Element of SubSort OU0 : x is OrderSortedSet of S1 } ; theorem Th18: :: OSALG_2:18 for S1 being OrderSortedSign for OU0 being OSAlgebra of S1 for A being OSSubset of OU0 holds OSSubSort A c= OSSubSort OU0 proof let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1 for A being OSSubset of OU0 holds OSSubSort A c= OSSubSort OU0 let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0 holds OSSubSort A c= OSSubSort OU0 let A be OSSubset of OU0; ::_thesis: OSSubSort A c= OSSubSort OU0 let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in OSSubSort A or x in OSSubSort OU0 ) assume x in OSSubSort A ; ::_thesis: x in OSSubSort OU0 then consider x1 being Element of SubSort A such that A1: x1 = x and A2: x1 is OrderSortedSet of S1 ; ( x1 in SubSort A & SubSort A c= SubSort OU0 ) by MSUALG_2:39; then reconsider x2 = x1 as Element of SubSort OU0 ; x2 in { y where y is Element of SubSort OU0 : y is OrderSortedSet of S1 } by A2; hence x in OSSubSort OU0 by A1; ::_thesis: verum end; registration let S1 be OrderSortedSign; let OU0 be OSAlgebra of S1; cluster OSSubSort OU0 -> non empty ; coherence not OSSubSort OU0 is empty proof set A = the OSSubset of OU0; OSSubSort the OSSubset of OU0 c= OSSubSort OU0 by Th18; hence not OSSubSort OU0 is empty ; ::_thesis: verum end; end; definition let S1 be OrderSortedSign; let OU0 be OSAlgebra of S1; let e be Element of OSSubSort OU0; func @ e -> OSSubset of OU0 equals :: OSALG_2:def 9 e; coherence e is OSSubset of OU0 proof e in { x where x is Element of SubSort OU0 : x is OrderSortedSet of S1 } ; then consider e1 being Element of SubSort OU0 such that A1: e = e1 and A2: e1 is OrderSortedSet of S1 ; reconsider e2 = @ e1 as OSSubset of OU0 by A2, Def2; e2 = e by A1; hence e is OSSubset of OU0 ; ::_thesis: verum end; end; :: deftheorem defines @ OSALG_2:def_9_:_ for S1 being OrderSortedSign for OU0 being OSAlgebra of S1 for e being Element of OSSubSort OU0 holds @ e = e; theorem Th19: :: OSALG_2:19 for S1 being OrderSortedSign for OU0 being OSAlgebra of S1 for A, B being OSSubset of OU0 holds ( B in OSSubSort A iff ( B is opers_closed & OSConstants OU0 c= B & A c= B ) ) proof let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1 for A, B being OSSubset of OU0 holds ( B in OSSubSort A iff ( B is opers_closed & OSConstants OU0 c= B & A c= B ) ) let OU0 be OSAlgebra of S1; ::_thesis: for A, B being OSSubset of OU0 holds ( B in OSSubSort A iff ( B is opers_closed & OSConstants OU0 c= B & A c= B ) ) let A, B be OSSubset of OU0; ::_thesis: ( B in OSSubSort A iff ( B is opers_closed & OSConstants OU0 c= B & A c= B ) ) thus ( B in OSSubSort A implies ( B is opers_closed & OSConstants OU0 c= B & A c= B ) ) ::_thesis: ( B is opers_closed & OSConstants OU0 c= B & A c= B implies B in OSSubSort A ) proof assume B in OSSubSort A ; ::_thesis: ( B is opers_closed & OSConstants OU0 c= B & A c= B ) then A1: ex B1 being Element of SubSort A st ( B1 = B & B1 is OrderSortedSet of S1 ) ; then Constants OU0 c= B by MSUALG_2:13; hence ( B is opers_closed & OSConstants OU0 c= B & A c= B ) by A1, Th11, MSUALG_2:13; ::_thesis: verum end; assume that A2: B is opers_closed and A3: OSConstants OU0 c= B and A4: A c= B ; ::_thesis: B in OSSubSort A Constants OU0 c= OSConstants OU0 by Th10; then Constants OU0 c= B by A3, PBOOLE:13; then A5: B in SubSort A by A2, A4, MSUALG_2:13; B is OrderSortedSet of S1 by Def2; hence B in OSSubSort A by A5; ::_thesis: verum end; theorem Th20: :: OSALG_2:20 for S1 being OrderSortedSign for OU0 being OSAlgebra of S1 for B being OSSubset of OU0 holds ( B in OSSubSort OU0 iff B is opers_closed ) proof let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1 for B being OSSubset of OU0 holds ( B in OSSubSort OU0 iff B is opers_closed ) let OU0 be OSAlgebra of S1; ::_thesis: for B being OSSubset of OU0 holds ( B in OSSubSort OU0 iff B is opers_closed ) let B be OSSubset of OU0; ::_thesis: ( B in OSSubSort OU0 iff B is opers_closed ) A1: ( B in SubSort OU0 iff B is opers_closed ) by MSUALG_2:14; thus ( B in OSSubSort OU0 implies B is opers_closed ) ::_thesis: ( B is opers_closed implies B in OSSubSort OU0 ) proof assume B in OSSubSort OU0 ; ::_thesis: B is opers_closed then ex B1 being Element of SubSort OU0 st ( B1 = B & B1 is OrderSortedSet of S1 ) ; hence B is opers_closed by MSUALG_2:14; ::_thesis: verum end; assume A2: B is opers_closed ; ::_thesis: B in OSSubSort OU0 B is OrderSortedSet of S1 by Def2; hence B in OSSubSort OU0 by A1, A2; ::_thesis: verum end; definition let S1 be OrderSortedSign; let OU0 be OSAlgebra of S1; let A be OSSubset of OU0; let s be Element of S1; func OSSubSort (A,s) -> set means :Def10: :: OSALG_2:def 10 for x being set holds ( x in it iff ex B being OSSubset of OU0 st ( B in OSSubSort A & x = B . s ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ex B being OSSubset of OU0 st ( B in OSSubSort A & x = B . s ) ) proof defpred S1[ set ] means ex B being OSSubset of OU0 st ( B in OSSubSort A & \$1 = B . s ); set C = bool (Union the Sorts of OU0); consider X being set such that A1: for x being set holds ( x in X iff ( x in bool (Union the Sorts of OU0) & S1[x] ) ) from XBOOLE_0:sch_1(); take X ; ::_thesis: for x being set holds ( x in X iff ex B being OSSubset of OU0 st ( B in OSSubSort A & x = B . s ) ) A2: bool (Union the Sorts of OU0) = bool (union (rng the Sorts of OU0)) by CARD_3:def_4; for x being set holds ( x in X iff ex B being OSSubset of OU0 st ( B in OSSubSort A & x = B . s ) ) proof dom the Sorts of OU0 = the carrier of S1 by PARTFUN1:def_2; then the Sorts of OU0 . s in rng the Sorts of OU0 by FUNCT_1:def_3; then A3: the Sorts of OU0 . s c= union (rng the Sorts of OU0) by ZFMISC_1:74; let x be set ; ::_thesis: ( x in X iff ex B being OSSubset of OU0 st ( B in OSSubSort A & x = B . s ) ) thus ( x in X implies ex B being OSSubset of OU0 st ( B in OSSubSort A & x = B . s ) ) by A1; ::_thesis: ( ex B being OSSubset of OU0 st ( B in OSSubSort A & x = B . s ) implies x in X ) given B being OSSubset of OU0 such that A4: B in OSSubSort A and A5: x = B . s ; ::_thesis: x in X B c= the Sorts of OU0 by PBOOLE:def_18; then B . s c= the Sorts of OU0 . s by PBOOLE:def_2; then x c= union (rng the Sorts of OU0) by A5, A3, XBOOLE_1:1; hence x in X by A2, A1, A4, A5; ::_thesis: verum end; hence for x being set holds ( x in X iff ex B being OSSubset of OU0 st ( B in OSSubSort A & x = B . s ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ex B being OSSubset of OU0 st ( B in OSSubSort A & x = B . s ) ) ) & ( for x being set holds ( x in b2 iff ex B being OSSubset of OU0 st ( B in OSSubSort A & x = B . s ) ) ) holds b1 = b2 proof defpred S1[ set ] means ex B being OSSubset of OU0 st ( B in OSSubSort A & \$1 = B . s ); thus for X1, X2 being set st ( for x being set holds ( x in X1 iff S1[x] ) ) & ( for x being set holds ( x in X2 iff S1[x] ) ) holds X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum end; end; :: deftheorem Def10 defines OSSubSort OSALG_2:def_10_:_ for S1 being OrderSortedSign for OU0 being OSAlgebra of S1 for A being OSSubset of OU0 for s being Element of S1 for b5 being set holds ( b5 = OSSubSort (A,s) iff for x being set holds ( x in b5 iff ex B being OSSubset of OU0 st ( B in OSSubSort A & x = B . s ) ) ); theorem Th21: :: OSALG_2:21 for S1 being OrderSortedSign for OU0 being OSAlgebra of S1 for A being OSSubset of OU0 for s1, s2 being SortSymbol of S1 st s1 <= s2 holds OSSubSort (A,s2) is_coarser_than OSSubSort (A,s1) proof let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1 for A being OSSubset of OU0 for s1, s2 being SortSymbol of S1 st s1 <= s2 holds OSSubSort (A,s2) is_coarser_than OSSubSort (A,s1) let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0 for s1, s2 being SortSymbol of S1 st s1 <= s2 holds OSSubSort (A,s2) is_coarser_than OSSubSort (A,s1) let A be OSSubset of OU0; ::_thesis: for s1, s2 being SortSymbol of S1 st s1 <= s2 holds OSSubSort (A,s2) is_coarser_than OSSubSort (A,s1) let s1, s2 be SortSymbol of S1; ::_thesis: ( s1 <= s2 implies OSSubSort (A,s2) is_coarser_than OSSubSort (A,s1) ) assume A1: s1 <= s2 ; ::_thesis: OSSubSort (A,s2) is_coarser_than OSSubSort (A,s1) for Y being set st Y in OSSubSort (A,s2) holds ex X being set st ( X in OSSubSort (A,s1) & X c= Y ) proof let x be set ; ::_thesis: ( x in OSSubSort (A,s2) implies ex X being set st ( X in OSSubSort (A,s1) & X c= x ) ) assume x in OSSubSort (A,s2) ; ::_thesis: ex X being set st ( X in OSSubSort (A,s1) & X c= x ) then consider B being OSSubset of OU0 such that A2: ( B in OSSubSort A & x = B . s2 ) by Def10; take B . s1 ; ::_thesis: ( B . s1 in OSSubSort (A,s1) & B . s1 c= x ) B is OrderSortedSet of S1 by Def2; hence ( B . s1 in OSSubSort (A,s1) & B . s1 c= x ) by A1, A2, Def10, OSALG_1:def_16; ::_thesis: verum end; hence OSSubSort (A,s2) is_coarser_than OSSubSort (A,s1) by SETFAM_1:def_3; ::_thesis: verum end; theorem Th22: :: OSALG_2:22 for S1 being OrderSortedSign for OU0 being OSAlgebra of S1 for A being OSSubset of OU0 for s being SortSymbol of S1 holds OSSubSort (A,s) c= SubSort (A,s) proof let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1 for A being OSSubset of OU0 for s being SortSymbol of S1 holds OSSubSort (A,s) c= SubSort (A,s) let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0 for s being SortSymbol of S1 holds OSSubSort (A,s) c= SubSort (A,s) let A be OSSubset of OU0; ::_thesis: for s being SortSymbol of S1 holds OSSubSort (A,s) c= SubSort (A,s) let s be SortSymbol of S1; ::_thesis: OSSubSort (A,s) c= SubSort (A,s) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in OSSubSort (A,s) or x in SubSort (A,s) ) assume x in OSSubSort (A,s) ; ::_thesis: x in SubSort (A,s) then A1: ex B being OSSubset of OU0 st ( B in OSSubSort A & x = B . s ) by Def10; OSSubSort A c= SubSort A by Th16; hence x in SubSort (A,s) by A1, MSUALG_2:def_13; ::_thesis: verum end; theorem Th23: :: OSALG_2:23 for S1 being OrderSortedSign for OU0 being OSAlgebra of S1 for A being OSSubset of OU0 for s being SortSymbol of S1 holds the Sorts of OU0 . s in OSSubSort (A,s) proof let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1 for A being OSSubset of OU0 for s being SortSymbol of S1 holds the Sorts of OU0 . s in OSSubSort (A,s) let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0 for s being SortSymbol of S1 holds the Sorts of OU0 . s in OSSubSort (A,s) let A be OSSubset of OU0; ::_thesis: for s being SortSymbol of S1 holds the Sorts of OU0 . s in OSSubSort (A,s) let s be SortSymbol of S1; ::_thesis: the Sorts of OU0 . s in OSSubSort (A,s) ( the Sorts of OU0 is ManySortedSubset of the Sorts of OU0 & the Sorts of OU0 is OrderSortedSet of S1 ) by OSALG_1:17, PBOOLE:def_18; then reconsider B = the Sorts of OU0 as OSSubset of OU0 by Def2; the Sorts of OU0 in OSSubSort A by Th17; then B . s in OSSubSort (A,s) by Def10; hence the Sorts of OU0 . s in OSSubSort (A,s) ; ::_thesis: verum end; registration let S1 be OrderSortedSign; let OU0 be OSAlgebra of S1; let A be OSSubset of OU0; let s be SortSymbol of S1; cluster OSSubSort (A,s) -> non empty ; coherence not OSSubSort (A,s) is empty by Th23; end; definition let S1 be OrderSortedSign; let OU0 be OSAlgebra of S1; let A be OSSubset of OU0; func OSMSubSort A -> OSSubset of OU0 means :Def11: :: OSALG_2:def 11 for s being SortSymbol of S1 holds it . s = meet (OSSubSort (A,s)); existence ex b1 being OSSubset of OU0 st for s being SortSymbol of S1 holds b1 . s = meet (OSSubSort (A,s)) proof deffunc H1( Element of S1) -> set = meet (OSSubSort (A,\$1)); consider f being Function such that A1: ( dom f = the carrier of S1 & ( for s being Element of S1 holds f . s = H1(s) ) ) from FUNCT_1:sch_4(); reconsider f = f as ManySortedSet of the carrier of S1 by A1, PARTFUN1:def_2, RELAT_1:def_18; f c= the Sorts of OU0 proof reconsider u0 = the Sorts of OU0 as MSSubset of OU0 by PBOOLE:def_18; let x be set ; :: according to PBOOLE:def_2 ::_thesis: ( not x in the carrier of S1 or f . x c= the Sorts of OU0 . x ) assume x in the carrier of S1 ; ::_thesis: f . x c= the Sorts of OU0 . x then reconsider s = x as SortSymbol of S1 ; A2: f . s = meet (OSSubSort (A,s)) by A1; u0 is OrderSortedSet of S1 by OSALG_1:17; then A3: u0 is OSSubset of OU0 by Def2; u0 in OSSubSort A by Th17; then the Sorts of OU0 . s in OSSubSort (A,s) by A3, Def10; hence f . x c= the Sorts of OU0 . x by A2, SETFAM_1:3; ::_thesis: verum end; then reconsider f = f as MSSubset of OU0 by PBOOLE:def_18; take f ; ::_thesis: ( f is OSSubset of OU0 & ( for s being SortSymbol of S1 holds f . s = meet (OSSubSort (A,s)) ) ) reconsider f1 = f as ManySortedSet of S1 ; for s1, s2 being Element of S1 st s1 <= s2 holds f1 . s1 c= f1 . s2 proof let s1, s2 be Element of S1; ::_thesis: ( s1 <= s2 implies f1 . s1 c= f1 . s2 ) assume s1 <= s2 ; ::_thesis: f1 . s1 c= f1 . s2 then A4: meet (OSSubSort (A,s1)) c= meet (OSSubSort (A,s2)) by Th21, SETFAM_1:14; f1 . s1 = meet (OSSubSort (A,s1)) by A1; hence f1 . s1 c= f1 . s2 by A1, A4; ::_thesis: verum end; then f is OrderSortedSet of S1 by OSALG_1:def_16; hence ( f is OSSubset of OU0 & ( for s being SortSymbol of S1 holds f . s = meet (OSSubSort (A,s)) ) ) by A1, Def2; ::_thesis: verum end; uniqueness for b1, b2 being OSSubset of OU0 st ( for s being SortSymbol of S1 holds b1 . s = meet (OSSubSort (A,s)) ) & ( for s being SortSymbol of S1 holds b2 . s = meet (OSSubSort (A,s)) ) holds b1 = b2 proof let W1, W2 be OSSubset of OU0; ::_thesis: ( ( for s being SortSymbol of S1 holds W1 . s = meet (OSSubSort (A,s)) ) & ( for s being SortSymbol of S1 holds W2 . s = meet (OSSubSort (A,s)) ) implies W1 = W2 ) assume that A5: for s being SortSymbol of S1 holds W1 . s = meet (OSSubSort (A,s)) and A6: for s being SortSymbol of S1 holds W2 . s = meet (OSSubSort (A,s)) ; ::_thesis: W1 = W2 for s being set st s in the carrier of S1 holds W1 . s = W2 . s proof let s be set ; ::_thesis: ( s in the carrier of S1 implies W1 . s = W2 . s ) assume s in the carrier of S1 ; ::_thesis: W1 . s = W2 . s then reconsider s = s as SortSymbol of S1 ; W1 . s = meet (OSSubSort (A,s)) by A5; hence W1 . s = W2 . s by A6; ::_thesis: verum end; hence W1 = W2 by PBOOLE:3; ::_thesis: verum end; end; :: deftheorem Def11 defines OSMSubSort OSALG_2:def_11_:_ for S1 being OrderSortedSign for OU0 being OSAlgebra of S1 for A, b4 being OSSubset of OU0 holds ( b4 = OSMSubSort A iff for s being SortSymbol of S1 holds b4 . s = meet (OSSubSort (A,s)) ); registration let S1 be OrderSortedSign; let OU0 be OSAlgebra of S1; cluster non empty Relation-like the carrier of S1 -defined Function-like V17( the carrier of S1) opers_closed for OSSubset of OU0; existence ex b1 being OSSubset of OU0 st b1 is opers_closed proof set x = the Element of OSSubSort OU0; the Element of OSSubSort OU0 in { y where y is Element of SubSort OU0 : y is OrderSortedSet of S1 } ; then consider x1 being Element of SubSort OU0 such that the Element of OSSubSort OU0 = x1 and A1: x1 is OrderSortedSet of S1 ; reconsider x2 = x1 as MSSubset of OU0 by MSUALG_2:def_11; reconsider x3 = x2 as OSSubset of OU0 by A1, Def2; take x3 ; ::_thesis: x3 is opers_closed thus x3 is opers_closed by MSUALG_2:def_11; ::_thesis: verum end; end; theorem Th24: :: OSALG_2:24 for S1 being OrderSortedSign for OU0 being OSAlgebra of S1 for A being OSSubset of OU0 holds (OSConstants OU0) \/ A c= OSMSubSort A proof let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1 for A being OSSubset of OU0 holds (OSConstants OU0) \/ A c= OSMSubSort A let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0 holds (OSConstants OU0) \/ A c= OSMSubSort A let A be OSSubset of OU0; ::_thesis: (OSConstants OU0) \/ A c= OSMSubSort A let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S1 or ((OSConstants OU0) \/ A) . i c= (OSMSubSort A) . i ) assume i in the carrier of S1 ; ::_thesis: ((OSConstants OU0) \/ A) . i c= (OSMSubSort A) . i then reconsider s = i as SortSymbol of S1 ; A1: for Z being set st Z in OSSubSort (A,s) holds ((OSConstants OU0) \/ A) . s c= Z proof let Z be set ; ::_thesis: ( Z in OSSubSort (A,s) implies ((OSConstants OU0) \/ A) . s c= Z ) assume Z in OSSubSort (A,s) ; ::_thesis: ((OSConstants OU0) \/ A) . s c= Z then consider B being OSSubset of OU0 such that A2: B in OSSubSort A and A3: Z = B . s by Def10; ( OSConstants OU0 c= B & A c= B ) by A2, Th19; then (OSConstants OU0) \/ A c= B by PBOOLE:16; hence ((OSConstants OU0) \/ A) . s c= Z by A3, PBOOLE:def_2; ::_thesis: verum end; (OSMSubSort A) . s = meet (OSSubSort (A,s)) by Def11; hence ((OSConstants OU0) \/ A) . i c= (OSMSubSort A) . i by A1, SETFAM_1:5; ::_thesis: verum end; theorem :: OSALG_2:25 for S1 being OrderSortedSign for OU0 being OSAlgebra of S1 for A being OSSubset of OU0 st (OSConstants OU0) \/ A is V8() holds OSMSubSort A is V8() proof let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1 for A being OSSubset of OU0 st (OSConstants OU0) \/ A is V8() holds OSMSubSort A is V8() let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0 st (OSConstants OU0) \/ A is V8() holds OSMSubSort A is V8() let A be OSSubset of OU0; ::_thesis: ( (OSConstants OU0) \/ A is V8() implies OSMSubSort A is V8() ) assume A1: (OSConstants OU0) \/ A is V8() ; ::_thesis: OSMSubSort A is V8() now__::_thesis:_for_i_being_set_st_i_in_the_carrier_of_S1_holds_ not_(OSMSubSort_A)_._i_is_empty let i be set ; ::_thesis: ( i in the carrier of S1 implies not (OSMSubSort A) . i is empty ) assume i in the carrier of S1 ; ::_thesis: not (OSMSubSort A) . i is empty then reconsider s = i as SortSymbol of S1 ; for Z being set st Z in OSSubSort (A,s) holds ((OSConstants OU0) \/ A) . s c= Z proof let Z be set ; ::_thesis: ( Z in OSSubSort (A,s) implies ((OSConstants OU0) \/ A) . s c= Z ) assume Z in OSSubSort (A,s) ; ::_thesis: ((OSConstants OU0) \/ A) . s c= Z then consider B being OSSubset of OU0 such that A2: B in OSSubSort A and A3: Z = B . s by Def10; ( OSConstants OU0 c= B & A c= B ) by A2, Th19; then (OSConstants OU0) \/ A c= B by PBOOLE:16; hence ((OSConstants OU0) \/ A) . s c= Z by A3, PBOOLE:def_2; ::_thesis: verum end; then A4: ((OSConstants OU0) \/ A) . s c= meet (OSSubSort (A,s)) by SETFAM_1:5; ex x being set st x in ((OSConstants OU0) \/ A) . s by A1, XBOOLE_0:def_1; hence not (OSMSubSort A) . i is empty by A4, Def11; ::_thesis: verum end; hence OSMSubSort A is V8() by PBOOLE:def_13; ::_thesis: verum end; theorem Th26: :: OSALG_2:26 for S1 being OrderSortedSign for OU0 being OSAlgebra of S1 for o being OperSymbol of S1 for A, B being OSSubset of OU0 st B in OSSubSort A holds (((OSMSubSort A) #) * the Arity of S1) . o c= ((B #) * the Arity of S1) . o proof let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1 for o being OperSymbol of S1 for A, B being OSSubset of OU0 st B in OSSubSort A holds (((OSMSubSort A) #) * the Arity of S1) . o c= ((B #) * the Arity of S1) . o let OU0 be OSAlgebra of S1; ::_thesis: for o being OperSymbol of S1 for A, B being OSSubset of OU0 st B in OSSubSort A holds (((OSMSubSort A) #) * the Arity of S1) . o c= ((B #) * the Arity of S1) . o let o be OperSymbol of S1; ::_thesis: for A, B being OSSubset of OU0 st B in OSSubSort A holds (((OSMSubSort A) #) * the Arity of S1) . o c= ((B #) * the Arity of S1) . o let A, B be OSSubset of OU0; ::_thesis: ( B in OSSubSort A implies (((OSMSubSort A) #) * the Arity of S1) . o c= ((B #) * the Arity of S1) . o ) assume A1: B in OSSubSort A ; ::_thesis: (((OSMSubSort A) #) * the Arity of S1) . o c= ((B #) * the Arity of S1) . o OSMSubSort A c= B proof let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S1 or (OSMSubSort A) . i c= B . i ) assume i in the carrier of S1 ; ::_thesis: (OSMSubSort A) . i c= B . i then reconsider s = i as SortSymbol of S1 ; ( (OSMSubSort A) . s = meet (OSSubSort (A,s)) & B . s in OSSubSort (A,s) ) by A1, Def10, Def11; hence (OSMSubSort A) . i c= B . i by SETFAM_1:3; ::_thesis: verum end; hence (((OSMSubSort A) #) * the Arity of S1) . o c= ((B #) * the Arity of S1) . o by MSUALG_2:2; ::_thesis: verum end; theorem Th27: :: OSALG_2:27 for S1 being OrderSortedSign for OU0 being OSAlgebra of S1 for o being OperSymbol of S1 for A, B being OSSubset of OU0 st B in OSSubSort A holds rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o proof let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1 for o being OperSymbol of S1 for A, B being OSSubset of OU0 st B in OSSubSort A holds rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o let OU0 be OSAlgebra of S1; ::_thesis: for o being OperSymbol of S1 for A, B being OSSubset of OU0 st B in OSSubSort A holds rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o let o be OperSymbol of S1; ::_thesis: for A, B being OSSubset of OU0 st B in OSSubSort A holds rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o let A, B be OSSubset of OU0; ::_thesis: ( B in OSSubSort A implies rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o ) set m = (((OSMSubSort A) #) * the Arity of S1) . o; set b = ((B #) * the Arity of S1) . o; set d = Den (o,OU0); assume A1: B in OSSubSort A ; ::_thesis: rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o then B is opers_closed by Th19; then B is_closed_on o by MSUALG_2:def_6; then A2: rng ((Den (o,OU0)) | (((B #) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o by MSUALG_2:def_5; (((B #) * the Arity of S1) . o) /\ ((((OSMSubSort A) #) * the Arity of S1) . o) = (((OSMSubSort A) #) * the Arity of S1) . o by A1, Th26, XBOOLE_1:28; then (Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o) = ((Den (o,OU0)) | (((B #) * the Arity of S1) . o)) | ((((OSMSubSort A) #) * the Arity of S1) . o) by RELAT_1:71; then rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= rng ((Den (o,OU0)) | (((B #) * the Arity of S1) . o)) by RELAT_1:70; hence rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o by A2, XBOOLE_1:1; ::_thesis: verum end; theorem Th28: :: OSALG_2:28 for S1 being OrderSortedSign for OU0 being OSAlgebra of S1 for o being OperSymbol of S1 for A being OSSubset of OU0 holds rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= ((OSMSubSort A) * the ResultSort of S1) . o proof let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1 for o being OperSymbol of S1 for A being OSSubset of OU0 holds rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= ((OSMSubSort A) * the ResultSort of S1) . o let OU0 be OSAlgebra of S1; ::_thesis: for o being OperSymbol of S1 for A being OSSubset of OU0 holds rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= ((OSMSubSort A) * the ResultSort of S1) . o let o be OperSymbol of S1; ::_thesis: for A being OSSubset of OU0 holds rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= ((OSMSubSort A) * the ResultSort of S1) . o let A be OSSubset of OU0; ::_thesis: rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= ((OSMSubSort A) * the ResultSort of S1) . o let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) or x in ((OSMSubSort A) * the ResultSort of S1) . o ) assume that A1: x in rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) and A2: not x in ((OSMSubSort A) * the ResultSort of S1) . o ; ::_thesis: contradiction set r = the_result_sort_of o; A3: ( the_result_sort_of o = the ResultSort of S1 . o & dom the ResultSort of S1 = the carrier' of S1 ) by FUNCT_2:def_1, MSUALG_1:def_2; then ((OSMSubSort A) * the ResultSort of S1) . o = (OSMSubSort A) . (the_result_sort_of o) by FUNCT_1:13 .= meet (OSSubSort (A,(the_result_sort_of o))) by Def11 ; then consider X being set such that A4: X in OSSubSort (A,(the_result_sort_of o)) and A5: not x in X by A2, SETFAM_1:def_1; consider B being OSSubset of OU0 such that A6: B in OSSubSort A and A7: B . (the_result_sort_of o) = X by A4, Def10; rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= (B * the ResultSort of S1) . o by A6, Th27; then x in (B * the ResultSort of S1) . o by A1; hence contradiction by A3, A5, A7, FUNCT_1:13; ::_thesis: verum end; theorem Th29: :: OSALG_2:29 for S1 being OrderSortedSign for OU0 being OSAlgebra of S1 for A being OSSubset of OU0 holds ( OSMSubSort A is opers_closed & A c= OSMSubSort A ) proof let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1 for A being OSSubset of OU0 holds ( OSMSubSort A is opers_closed & A c= OSMSubSort A ) let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0 holds ( OSMSubSort A is opers_closed & A c= OSMSubSort A ) let A be OSSubset of OU0; ::_thesis: ( OSMSubSort A is opers_closed & A c= OSMSubSort A ) thus OSMSubSort A is opers_closed ::_thesis: A c= OSMSubSort A proof let o1 be Element of the carrier' of S1; :: according to MSUALG_2:def_6 ::_thesis: OSMSubSort A is_closed_on o1 reconsider o = o1 as OperSymbol of S1 ; rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= ((OSMSubSort A) * the ResultSort of S1) . o by Th28; hence OSMSubSort A is_closed_on o1 by MSUALG_2:def_5; ::_thesis: verum end; ( A c= (OSConstants OU0) \/ A & (OSConstants OU0) \/ A c= OSMSubSort A ) by Th24, PBOOLE:14; hence A c= OSMSubSort A by PBOOLE:13; ::_thesis: verum end; registration let S1 be OrderSortedSign; let OU0 be OSAlgebra of S1; let A be OSSubset of OU0; cluster OSMSubSort A -> opers_closed ; coherence OSMSubSort A is opers_closed by Th29; end; begin registration let S1 be OrderSortedSign; let OU0 be OSAlgebra of S1; let A be opers_closed OSSubset of OU0; clusterOU0 | A -> order-sorted ; coherence OU0 | A is order-sorted proof set M = MSAlgebra(# A,(Opers (OU0,A)) #); ( OU0 | A = MSAlgebra(# A,(Opers (OU0,A)) #) & A is OrderSortedSet of S1 ) by Def2, MSUALG_2:def_15; hence OU0 | A is order-sorted by OSALG_1:17; ::_thesis: verum end; end; registration let S1 be OrderSortedSign; let OU0 be OSAlgebra of S1; let OU1, OU2 be OSSubAlgebra of OU0; clusterOU1 /\ OU2 -> order-sorted ; coherence OU1 /\ OU2 is order-sorted proof reconsider M1 = the Sorts of OU1, M2 = the Sorts of OU2 as OrderSortedSet of S1 by OSALG_1:17; M1 /\ M2 is OrderSortedSet of S1 by Th1; then the Sorts of (OU1 /\ OU2) is OrderSortedSet of S1 by MSUALG_2:def_16; hence OU1 /\ OU2 is order-sorted by OSALG_1:17; ::_thesis: verum end; end; definition let S1 be OrderSortedSign; let OU0 be OSAlgebra of S1; let A be OSSubset of OU0; func GenOSAlg A -> strict OSSubAlgebra of OU0 means :Def12: :: OSALG_2:def 12 ( A is OSSubset of it & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds it is OSSubAlgebra of OU1 ) ); existence ex b1 being strict OSSubAlgebra of OU0 st ( A is OSSubset of b1 & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds b1 is OSSubAlgebra of OU1 ) ) proof set a = OSMSubSort A; reconsider u1 = OU0 | (OSMSubSort A) as strict OSSubAlgebra of OU0 ; take u1 ; ::_thesis: ( A is OSSubset of u1 & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds u1 is OSSubAlgebra of OU1 ) ) A1: u1 = MSAlgebra(# (OSMSubSort A),(Opers (OU0,(OSMSubSort A))) #) by MSUALG_2:def_15; A2: A is OrderSortedSet of S1 by Def2; A c= OSMSubSort A by Th29; then A is MSSubset of u1 by A1, PBOOLE:def_18; hence A is OSSubset of u1 by A2, Def2; ::_thesis: for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds u1 is OSSubAlgebra of OU1 let U2 be OSSubAlgebra of OU0; ::_thesis: ( A is OSSubset of U2 implies u1 is OSSubAlgebra of U2 ) reconsider B1 = the Sorts of U2 as MSSubset of OU0 by MSUALG_2:def_9; B1 is OrderSortedSet of S1 by OSALG_1:17; then reconsider B = B1 as OSSubset of OU0 by Def2; assume A is OSSubset of U2 ; ::_thesis: u1 is OSSubAlgebra of U2 then A3: ( B is opers_closed & A c= B ) by MSUALG_2:def_9, PBOOLE:def_18; OSConstants OU0 is OSSubset of U2 by Th13; then OSConstants OU0 c= B by PBOOLE:def_18; then A4: B in OSSubSort A by A3, Th19; the Sorts of u1 c= the Sorts of U2 proof let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S1 or the Sorts of u1 . i c= the Sorts of U2 . i ) assume i in the carrier of S1 ; ::_thesis: the Sorts of u1 . i c= the Sorts of U2 . i then reconsider s = i as SortSymbol of S1 ; ( the Sorts of u1 . s = meet (OSSubSort (A,s)) & B . s in OSSubSort (A,s) ) by A1, A4, Def10, Def11; hence the Sorts of u1 . i c= the Sorts of U2 . i by SETFAM_1:3; ::_thesis: verum end; hence u1 is OSSubAlgebra of U2 by MSUALG_2:8; ::_thesis: verum end; uniqueness for b1, b2 being strict OSSubAlgebra of OU0 st A is OSSubset of b1 & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds b1 is OSSubAlgebra of OU1 ) & A is OSSubset of b2 & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds b2 is OSSubAlgebra of OU1 ) holds b1 = b2 proof let W1, W2 be strict OSSubAlgebra of OU0; ::_thesis: ( A is OSSubset of W1 & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds W1 is OSSubAlgebra of OU1 ) & A is OSSubset of W2 & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds W2 is OSSubAlgebra of OU1 ) implies W1 = W2 ) assume ( A is OSSubset of W1 & ( for U1 being OSSubAlgebra of OU0 st A is OSSubset of U1 holds W1 is OSSubAlgebra of U1 ) & A is OSSubset of W2 & ( for U2 being OSSubAlgebra of OU0 st A is OSSubset of U2 holds W2 is OSSubAlgebra of U2 ) ) ; ::_thesis: W1 = W2 then ( W1 is strict OSSubAlgebra of W2 & W2 is strict OSSubAlgebra of W1 ) ; hence W1 = W2 by MSUALG_2:7; ::_thesis: verum end; end; :: deftheorem Def12 defines GenOSAlg OSALG_2:def_12_:_ for S1 being OrderSortedSign for OU0 being OSAlgebra of S1 for A being OSSubset of OU0 for b4 being strict OSSubAlgebra of OU0 holds ( b4 = GenOSAlg A iff ( A is OSSubset of b4 & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds b4 is OSSubAlgebra of OU1 ) ) ); theorem Th30: :: OSALG_2:30 for S1 being OrderSortedSign for OU0 being OSAlgebra of S1 for A being OSSubset of OU0 holds ( GenOSAlg A = OU0 | (OSMSubSort A) & the Sorts of (GenOSAlg A) = OSMSubSort A ) proof let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1 for A being OSSubset of OU0 holds ( GenOSAlg A = OU0 | (OSMSubSort A) & the Sorts of (GenOSAlg A) = OSMSubSort A ) let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0 holds ( GenOSAlg A = OU0 | (OSMSubSort A) & the Sorts of (GenOSAlg A) = OSMSubSort A ) let A be OSSubset of OU0; ::_thesis: ( GenOSAlg A = OU0 | (OSMSubSort A) & the Sorts of (GenOSAlg A) = OSMSubSort A ) set a = OSMSubSort A; reconsider u1 = OU0 | (OSMSubSort A) as strict OSSubAlgebra of OU0 ; A1: u1 = MSAlgebra(# (OSMSubSort A),(Opers (OU0,(OSMSubSort A))) #) by MSUALG_2:def_15; A2: A c= OSMSubSort A by Th29; A3: A is OrderSortedSet of S1 by Def2; A4: ( A is OSSubset of u1 & ( for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds u1 is OSSubAlgebra of OU1 ) ) proof A is MSSubset of u1 by A2, A1, PBOOLE:def_18; hence A is OSSubset of u1 by A3, Def2; ::_thesis: for OU1 being OSSubAlgebra of OU0 st A is OSSubset of OU1 holds u1 is OSSubAlgebra of OU1 let U2 be OSSubAlgebra of OU0; ::_thesis: ( A is OSSubset of U2 implies u1 is OSSubAlgebra of U2 ) reconsider B1 = the Sorts of U2 as MSSubset of OU0 by MSUALG_2:def_9; B1 is OrderSortedSet of S1 by OSALG_1:17; then reconsider B = B1 as OSSubset of OU0 by Def2; assume A is OSSubset of U2 ; ::_thesis: u1 is OSSubAlgebra of U2 then A5: ( B is opers_closed & A c= B ) by MSUALG_2:def_9, PBOOLE:def_18; OSConstants OU0 is OSSubset of U2 by Th13; then OSConstants OU0 c= B by PBOOLE:def_18; then A6: B in OSSubSort A by A5, Th19; the Sorts of u1 c= the Sorts of U2 proof let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S1 or the Sorts of u1 . i c= the Sorts of U2 . i ) assume i in the carrier of S1 ; ::_thesis: the Sorts of u1 . i c= the Sorts of U2 . i then reconsider s = i as SortSymbol of S1 ; ( the Sorts of u1 . s = meet (OSSubSort (A,s)) & B . s in OSSubSort (A,s) ) by A1, A6, Def10, Def11; hence the Sorts of u1 . i c= the Sorts of U2 . i by SETFAM_1:3; ::_thesis: verum end; hence u1 is OSSubAlgebra of U2 by MSUALG_2:8; ::_thesis: verum end; hence GenOSAlg A = OU0 | (OSMSubSort A) by Def12; ::_thesis: the Sorts of (GenOSAlg A) = OSMSubSort A thus the Sorts of (GenOSAlg A) = OSMSubSort A by A1, A4, Def12; ::_thesis: verum end; theorem Th31: :: OSALG_2:31 for S being non empty non void ManySortedSign for U0 being MSAlgebra over S for A being MSSubset of U0 holds ( GenMSAlg A = U0 | (MSSubSort A) & the Sorts of (GenMSAlg A) = MSSubSort A ) proof let S be non empty non void ManySortedSign ; ::_thesis: for U0 being MSAlgebra over S for A being MSSubset of U0 holds ( GenMSAlg A = U0 | (MSSubSort A) & the Sorts of (GenMSAlg A) = MSSubSort A ) let U0 be MSAlgebra over S; ::_thesis: for A being MSSubset of U0 holds ( GenMSAlg A = U0 | (MSSubSort A) & the Sorts of (GenMSAlg A) = MSSubSort A ) let A be MSSubset of U0; ::_thesis: ( GenMSAlg A = U0 | (MSSubSort A) & the Sorts of (GenMSAlg A) = MSSubSort A ) set a = MSSubSort A; reconsider u1 = U0 | (MSSubSort A) as strict MSSubAlgebra of U0 ; A1: u1 = MSAlgebra(# (MSSubSort A),(Opers (U0,(MSSubSort A))) #) by MSUALG_2:20, MSUALG_2:def_15; A2: A c= MSSubSort A by MSUALG_2:20; A3: ( A is MSSubset of u1 & ( for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds u1 is MSSubAlgebra of U1 ) ) proof thus A is MSSubset of u1 by A2, A1, PBOOLE:def_18; ::_thesis: for U1 being MSSubAlgebra of U0 st A is MSSubset of U1 holds u1 is MSSubAlgebra of U1 let U2 be MSSubAlgebra of U0; ::_thesis: ( A is MSSubset of U2 implies u1 is MSSubAlgebra of U2 ) reconsider B = the Sorts of U2 as MSSubset of U0 by MSUALG_2:def_9; Constants U0 is MSSubset of U2 by MSUALG_2:10; then A4: Constants U0 c= B by PBOOLE:def_18; assume A is MSSubset of U2 ; ::_thesis: u1 is MSSubAlgebra of U2 then ( B is opers_closed & A c= B ) by MSUALG_2:def_9, PBOOLE:def_18; then A5: B in SubSort A by A4, MSUALG_2:13; the Sorts of u1 c= the Sorts of U2 proof let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S or the Sorts of u1 . i c= the Sorts of U2 . i ) assume i in the carrier of S ; ::_thesis: the Sorts of u1 . i c= the Sorts of U2 . i then reconsider s = i as SortSymbol of S ; ( the Sorts of u1 . s = meet (SubSort (A,s)) & B . s in SubSort (A,s) ) by A1, A5, MSUALG_2:def_13, MSUALG_2:def_14; hence the Sorts of u1 . i c= the Sorts of U2 . i by SETFAM_1:3; ::_thesis: verum end; hence u1 is MSSubAlgebra of U2 by MSUALG_2:8; ::_thesis: verum end; hence GenMSAlg A = U0 | (MSSubSort A) by MSUALG_2:def_17; ::_thesis: the Sorts of (GenMSAlg A) = MSSubSort A thus the Sorts of (GenMSAlg A) = MSSubSort A by A1, A3, MSUALG_2:def_17; ::_thesis: verum end; theorem Th32: :: OSALG_2:32 for S1 being OrderSortedSign for OU0 being OSAlgebra of S1 for A being OSSubset of OU0 holds the Sorts of (GenMSAlg A) c= the Sorts of (GenOSAlg A) proof let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1 for A being OSSubset of OU0 holds the Sorts of (GenMSAlg A) c= the Sorts of (GenOSAlg A) let OU0 be OSAlgebra of S1; ::_thesis: for A being OSSubset of OU0 holds the Sorts of (GenMSAlg A) c= the Sorts of (GenOSAlg A) let A be OSSubset of OU0; ::_thesis: the Sorts of (GenMSAlg A) c= the Sorts of (GenOSAlg A) set GM = GenMSAlg A; set GO = GenOSAlg A; let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in the carrier of S1 or the Sorts of (GenMSAlg A) . i c= the Sorts of (GenOSAlg A) . i ) assume i in the carrier of S1 ; ::_thesis: the Sorts of (GenMSAlg A) . i c= the Sorts of (GenOSAlg A) . i then reconsider s = i as SortSymbol of S1 ; the Sorts of (GenMSAlg A) = MSSubSort A by Th31; then A1: the Sorts of (GenMSAlg A) . s = meet (SubSort (A,s)) by MSUALG_2:def_14; the Sorts of (GenOSAlg A) = OSMSubSort A by Th30; then the Sorts of (GenOSAlg A) . s = meet (OSSubSort (A,s)) by Def11; hence the Sorts of (GenMSAlg A) . i c= the Sorts of (GenOSAlg A) . i by A1, Th22, SETFAM_1:6; ::_thesis: verum end; theorem :: OSALG_2:33 for S1 being OrderSortedSign for OU0 being OSAlgebra of S1 for A being OSSubset of OU0 holds GenMSAlg A is MSSubAlgebra of GenOSAlg A by Th32, MSUALG_2:8; theorem Th34: :: OSALG_2:34 for S1 being OrderSortedSign for OU0 being strict OSAlgebra of S1 for B being OSSubset of OU0 st B = the Sorts of OU0 holds GenOSAlg B = OU0 proof let S1 be OrderSortedSign; ::_thesis: for OU0 being strict OSAlgebra of S1 for B being OSSubset of OU0 st B = the Sorts of OU0 holds GenOSAlg B = OU0 let OU0 be strict OSAlgebra of S1; ::_thesis: for B being OSSubset of OU0 st B = the Sorts of OU0 holds GenOSAlg B = OU0 let B be OSSubset of OU0; ::_thesis: ( B = the Sorts of OU0 implies GenOSAlg B = OU0 ) assume B = the Sorts of OU0 ; ::_thesis: GenOSAlg B = OU0 then A1: GenMSAlg B = OU0 by MSUALG_2:21; GenMSAlg B is strict MSSubAlgebra of GenOSAlg B by Th32, MSUALG_2:8; hence GenOSAlg B = OU0 by A1, MSUALG_2:7; ::_thesis: verum end; theorem Th35: :: OSALG_2:35 for S1 being OrderSortedSign for OU0 being OSAlgebra of S1 for OU1 being strict OSSubAlgebra of OU0 for B being OSSubset of OU0 st B = the Sorts of OU1 holds GenOSAlg B = OU1 proof let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1 for OU1 being strict OSSubAlgebra of OU0 for B being OSSubset of OU0 st B = the Sorts of OU1 holds GenOSAlg B = OU1 let OU0 be OSAlgebra of S1; ::_thesis: for OU1 being strict OSSubAlgebra of OU0 for B being OSSubset of OU0 st B = the Sorts of OU1 holds GenOSAlg B = OU1 let OU1 be strict OSSubAlgebra of OU0; ::_thesis: for B being OSSubset of OU0 st B = the Sorts of OU1 holds GenOSAlg B = OU1 let B be OSSubset of OU0; ::_thesis: ( B = the Sorts of OU1 implies GenOSAlg B = OU1 ) set W = GenOSAlg B; assume A1: B = the Sorts of OU1 ; ::_thesis: GenOSAlg B = OU1 then A2: B is MSSubset of OU1 by PBOOLE:def_18; B is OSSubset of GenOSAlg B by Def12; then the Sorts of OU1 c= the Sorts of (GenOSAlg B) by A1, PBOOLE:def_18; then A3: OU1 is strict MSSubAlgebra of GenOSAlg B by MSUALG_2:8; B is OrderSortedSet of S1 by Def2; then B is OSSubset of OU1 by A2, Def2; then GenOSAlg B is strict OSSubAlgebra of OU1 by Def12; hence GenOSAlg B = OU1 by A3, MSUALG_2:7; ::_thesis: verum end; theorem Th36: :: OSALG_2:36 for S1 being OrderSortedSign for U0 being non-empty OSAlgebra of S1 for U1 being OSSubAlgebra of U0 holds (GenOSAlg (OSConstants U0)) /\ U1 = GenOSAlg (OSConstants U0) proof let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1 for U1 being OSSubAlgebra of U0 holds (GenOSAlg (OSConstants U0)) /\ U1 = GenOSAlg (OSConstants U0) let U0 be non-empty OSAlgebra of S1; ::_thesis: for U1 being OSSubAlgebra of U0 holds (GenOSAlg (OSConstants U0)) /\ U1 = GenOSAlg (OSConstants U0) let U1 be OSSubAlgebra of U0; ::_thesis: (GenOSAlg (OSConstants U0)) /\ U1 = GenOSAlg (OSConstants U0) set C = OSConstants U0; set G = GenOSAlg (OSConstants U0); OSConstants U0 is OSSubset of U1 by Th13; then GenOSAlg (OSConstants U0) is strict OSSubAlgebra of U1 by Def12; then the Sorts of (GenOSAlg (OSConstants U0)) is MSSubset of U1 by MSUALG_2:def_9; then ( the Sorts of ((GenOSAlg (OSConstants U0)) /\ U1) = the Sorts of (GenOSAlg (OSConstants U0)) /\ the Sorts of U1 & the Sorts of (GenOSAlg (OSConstants U0)) c= the Sorts of U1 ) by MSUALG_2:def_16, PBOOLE:def_18; then the Sorts of ((GenOSAlg (OSConstants U0)) /\ U1) = the Sorts of (GenOSAlg (OSConstants U0)) by PBOOLE:23; hence (GenOSAlg (OSConstants U0)) /\ U1 = GenOSAlg (OSConstants U0) by MSUALG_2:9; ::_thesis: verum end; definition let S1 be OrderSortedSign; let U0 be non-empty OSAlgebra of S1; let U1, U2 be OSSubAlgebra of U0; funcU1 "\/"_os U2 -> strict OSSubAlgebra of U0 means :Def13: :: OSALG_2:def 13 for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds it = GenOSAlg A; existence ex b1 being strict OSSubAlgebra of U0 st for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds b1 = GenOSAlg A proof set B = the Sorts of U1 \/ the Sorts of U2; the Sorts of U2 is MSSubset of U0 by MSUALG_2:def_9; then A1: the Sorts of U2 c= the Sorts of U0 by PBOOLE:def_18; the Sorts of U1 is MSSubset of U0 by MSUALG_2:def_9; then the Sorts of U1 c= the Sorts of U0 by PBOOLE:def_18; then the Sorts of U1 \/ the Sorts of U2 c= the Sorts of U0 by A1, PBOOLE:16; then reconsider B = the Sorts of U1 \/ the Sorts of U2 as MSSubset of U0 by PBOOLE:def_18; reconsider B1 = the Sorts of U1, B2 = the Sorts of U2 as OrderSortedSet of S1 by OSALG_1:17; B = B1 \/ B2 ; then B is OrderSortedSet of S1 by Th2; then reconsider B0 = B as OSSubset of U0 by Def2; take GenOSAlg B0 ; ::_thesis: for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds GenOSAlg B0 = GenOSAlg A thus for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds GenOSAlg B0 = GenOSAlg A ; ::_thesis: verum end; uniqueness for b1, b2 being strict OSSubAlgebra of U0 st ( for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds b1 = GenOSAlg A ) & ( for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds b2 = GenOSAlg A ) holds b1 = b2 proof reconsider B1 = the Sorts of U1, B2 = the Sorts of U2 as OrderSortedSet of S1 by OSALG_1:17; set B = the Sorts of U1 \/ the Sorts of U2; the Sorts of U2 is MSSubset of U0 by MSUALG_2:def_9; then A2: the Sorts of U2 c= the Sorts of U0 by PBOOLE:def_18; the Sorts of U1 is MSSubset of U0 by MSUALG_2:def_9; then the Sorts of U1 c= the Sorts of U0 by PBOOLE:def_18; then the Sorts of U1 \/ the Sorts of U2 c= the Sorts of U0 by A2, PBOOLE:16; then reconsider B = the Sorts of U1 \/ the Sorts of U2 as MSSubset of U0 by PBOOLE:def_18; let W1, W2 be strict OSSubAlgebra of U0; ::_thesis: ( ( for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds W1 = GenOSAlg A ) & ( for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds W2 = GenOSAlg A ) implies W1 = W2 ) assume that A3: for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds W1 = GenOSAlg A and A4: for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds W2 = GenOSAlg A ; ::_thesis: W1 = W2 B = B1 \/ B2 ; then B is OrderSortedSet of S1 by Th2; then reconsider B0 = B as OSSubset of U0 by Def2; W1 = GenOSAlg B0 by A3; hence W1 = W2 by A4; ::_thesis: verum end; end; :: deftheorem Def13 defines "\/"_os OSALG_2:def_13_:_ for S1 being OrderSortedSign for U0 being non-empty OSAlgebra of S1 for U1, U2 being OSSubAlgebra of U0 for b5 being strict OSSubAlgebra of U0 holds ( b5 = U1 "\/"_os U2 iff for A being OSSubset of U0 st A = the Sorts of U1 \/ the Sorts of U2 holds b5 = GenOSAlg A ); theorem Th37: :: OSALG_2:37 for S1 being OrderSortedSign for U0 being non-empty OSAlgebra of S1 for U1 being OSSubAlgebra of U0 for A, B being OSSubset of U0 st B = A \/ the Sorts of U1 holds (GenOSAlg A) "\/"_os U1 = GenOSAlg B proof let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1 for U1 being OSSubAlgebra of U0 for A, B being OSSubset of U0 st B = A \/ the Sorts of U1 holds (GenOSAlg A) "\/"_os U1 = GenOSAlg B let U0 be non-empty OSAlgebra of S1; ::_thesis: for U1 being OSSubAlgebra of U0 for A, B being OSSubset of U0 st B = A \/ the Sorts of U1 holds (GenOSAlg A) "\/"_os U1 = GenOSAlg B let U1 be OSSubAlgebra of U0; ::_thesis: for A, B being OSSubset of U0 st B = A \/ the Sorts of U1 holds (GenOSAlg A) "\/"_os U1 = GenOSAlg B let A, B be OSSubset of U0; ::_thesis: ( B = A \/ the Sorts of U1 implies (GenOSAlg A) "\/"_os U1 = GenOSAlg B ) assume A1: B = A \/ the Sorts of U1 ; ::_thesis: (GenOSAlg A) "\/"_os U1 = GenOSAlg B reconsider u1m = the Sorts of U1, am = the Sorts of (GenOSAlg A) as MSSubset of U0 by MSUALG_2:def_9; A2: ( the Sorts of U1 is OrderSortedSet of S1 & the Sorts of (GenOSAlg A) is OrderSortedSet of S1 ) by OSALG_1:17; then reconsider u1 = u1m, a = am as OSSubset of U0 by Def2; ( a c= the Sorts of U0 & u1 c= the Sorts of U0 ) by PBOOLE:def_18; then a \/ u1 c= the Sorts of U0 by PBOOLE:16; then reconsider b = a \/ u1 as MSSubset of U0 by PBOOLE:def_18; A3: a \/ u1 is OrderSortedSet of S1 by A2, Th2; then reconsider b = b as OSSubset of U0 by Def2; A4: (GenOSAlg A) "\/"_os U1 = GenOSAlg b by Def13; then a \/ u1 is OSSubset of (GenOSAlg A) "\/"_os U1 by Def12; then A5: a \/ u1 c= the Sorts of ((GenOSAlg A) "\/"_os U1) by PBOOLE:def_18; A is OSSubset of GenOSAlg A by Def12; then A6: A c= the Sorts of (GenOSAlg A) by PBOOLE:def_18; then A \/ u1 c= a \/ u1 by PBOOLE:20; then B c= the Sorts of ((GenOSAlg A) "\/"_os U1) by A1, A5, PBOOLE:13; then A7: B is MSSubset of ((GenOSAlg A) "\/"_os U1) by PBOOLE:def_18; A8: A is OrderSortedSet of S1 by Def2; A9: the Sorts of ((GenOSAlg A) /\ (GenOSAlg B)) = the Sorts of (GenOSAlg A) /\ the Sorts of (GenOSAlg B) by MSUALG_2:def_16; B is OSSubset of GenOSAlg B by Def12; then A10: B c= the Sorts of (GenOSAlg B) by PBOOLE:def_18; A c= B by A1, PBOOLE:14; then A c= the Sorts of (GenOSAlg B) by A10, PBOOLE:13; then A c= the Sorts of (GenOSAlg A) /\ the Sorts of (GenOSAlg B) by A6, PBOOLE:17; then A is MSSubset of ((GenOSAlg A) /\ (GenOSAlg B)) by A9, PBOOLE:def_18; then A is OSSubset of (GenOSAlg A) /\ (GenOSAlg B) by A8, Def2; then GenOSAlg A is OSSubAlgebra of (GenOSAlg A) /\ (GenOSAlg B) by Def12; then a is MSSubset of ((GenOSAlg A) /\ (GenOSAlg B)) by MSUALG_2:def_9; then A11: a c= the Sorts of (GenOSAlg A) /\ the Sorts of (GenOSAlg B) by A9, PBOOLE:def_18; the Sorts of (GenOSAlg A) /\ the Sorts of (GenOSAlg B) c= a by PBOOLE:15; then a = the Sorts of (GenOSAlg A) /\ the Sorts of (GenOSAlg B) by A11, PBOOLE:146; then A12: a c= the Sorts of (GenOSAlg B) by PBOOLE:15; u1 c= B by A1, PBOOLE:14; then u1 c= the Sorts of (GenOSAlg B) by A10, PBOOLE:13; then b c= the Sorts of (GenOSAlg B) by A12, PBOOLE:16; then b is MSSubset of (GenOSAlg B) by PBOOLE:def_18; then b is OSSubset of GenOSAlg B by A3, Def2; then A13: GenOSAlg b is strict OSSubAlgebra of GenOSAlg B by Def12; B is OrderSortedSet of S1 by Def2; then B is OSSubset of (GenOSAlg A) "\/"_os U1 by A7, Def2; then GenOSAlg B is strict OSSubAlgebra of (GenOSAlg A) "\/"_os U1 by Def12; hence (GenOSAlg A) "\/"_os U1 = GenOSAlg B by A4, A13, MSUALG_2:7; ::_thesis: verum end; theorem Th38: :: OSALG_2:38 for S1 being OrderSortedSign for U0 being non-empty OSAlgebra of S1 for U1 being OSSubAlgebra of U0 for B being OSSubset of U0 st B = the Sorts of U0 holds (GenOSAlg B) "\/"_os U1 = GenOSAlg B proof let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1 for U1 being OSSubAlgebra of U0 for B being OSSubset of U0 st B = the Sorts of U0 holds (GenOSAlg B) "\/"_os U1 = GenOSAlg B let U0 be non-empty OSAlgebra of S1; ::_thesis: for U1 being OSSubAlgebra of U0 for B being OSSubset of U0 st B = the Sorts of U0 holds (GenOSAlg B) "\/"_os U1 = GenOSAlg B let U1 be OSSubAlgebra of U0; ::_thesis: for B being OSSubset of U0 st B = the Sorts of U0 holds (GenOSAlg B) "\/"_os U1 = GenOSAlg B let B be OSSubset of U0; ::_thesis: ( B = the Sorts of U0 implies (GenOSAlg B) "\/"_os U1 = GenOSAlg B ) A1: the Sorts of U1 is MSSubset of U0 by MSUALG_2:def_9; assume B = the Sorts of U0 ; ::_thesis: (GenOSAlg B) "\/"_os U1 = GenOSAlg B then the Sorts of U1 c= B by A1, PBOOLE:def_18; then B \/ the Sorts of U1 = B by PBOOLE:22; hence (GenOSAlg B) "\/"_os U1 = GenOSAlg B by Th37; ::_thesis: verum end; theorem Th39: :: OSALG_2:39 for S1 being OrderSortedSign for U0 being non-empty OSAlgebra of S1 for U1, U2 being OSSubAlgebra of U0 holds U1 "\/"_os U2 = U2 "\/"_os U1 proof let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1 for U1, U2 being OSSubAlgebra of U0 holds U1 "\/"_os U2 = U2 "\/"_os U1 let U0 be non-empty OSAlgebra of S1; ::_thesis: for U1, U2 being OSSubAlgebra of U0 holds U1 "\/"_os U2 = U2 "\/"_os U1 let U1, U2 be OSSubAlgebra of U0; ::_thesis: U1 "\/"_os U2 = U2 "\/"_os U1 reconsider u1 = the Sorts of U1, u2 = the Sorts of U2 as MSSubset of U0 by MSUALG_2:def_9; ( u1 c= the Sorts of U0 & u2 c= the Sorts of U0 ) by PBOOLE:def_18; then u1 \/ u2 c= the Sorts of U0 by PBOOLE:16; then reconsider A1 = u1 \/ u2 as MSSubset of U0 by PBOOLE:def_18; ( u1 is OrderSortedSet of S1 & u2 is OrderSortedSet of S1 ) by OSALG_1:17; then A1 is OrderSortedSet of S1 by Th2; then reconsider A = A1 as OSSubset of U0 by Def2; U1 "\/"_os U2 = GenOSAlg A by Def13; hence U1 "\/"_os U2 = U2 "\/"_os U1 by Def13; ::_thesis: verum end; theorem Th40: :: OSALG_2:40 for S1 being OrderSortedSign for U0 being non-empty OSAlgebra of S1 for U1, U2 being strict OSSubAlgebra of U0 holds U1 /\ (U1 "\/"_os U2) = U1 proof let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1 for U1, U2 being strict OSSubAlgebra of U0 holds U1 /\ (U1 "\/"_os U2) = U1 let U0 be non-empty OSAlgebra of S1; ::_thesis: for U1, U2 being strict OSSubAlgebra of U0 holds U1 /\ (U1 "\/"_os U2) = U1 let U1, U2 be strict OSSubAlgebra of U0; ::_thesis: U1 /\ (U1 "\/"_os U2) = U1 reconsider u1 = the Sorts of U1, u2 = the Sorts of U2 as MSSubset of U0 by MSUALG_2:def_9; reconsider u112 = the Sorts of (U1 /\ (U1 "\/"_os U2)) as MSSubset of U0 by MSUALG_2:def_9; A1: the Charact of (U1 /\ (U1 "\/"_os U2)) = Opers (U0,u112) by MSUALG_2:def_16; ( u1 c= the Sorts of U0 & u2 c= the Sorts of U0 ) by PBOOLE:def_18; then u1 \/ u2 c= the Sorts of U0 by PBOOLE:16; then reconsider A = u1 \/ u2 as MSSubset of U0 by PBOOLE:def_18; ( u1 is OrderSortedSet of S1 & u2 is OrderSortedSet of S1 ) by OSALG_1:17; then A is OrderSortedSet of S1 by Th2; then reconsider A = A as OSSubset of U0 by Def2; A2: the Sorts of (U1 /\ (U1 "\/"_os U2)) = the Sorts of U1 /\ the Sorts of (U1 "\/"_os U2) by MSUALG_2:def_16; U1 "\/"_os U2 = GenOSAlg A by Def13; then A is OSSubset of U1 "\/"_os U2 by Def12; then A3: A c= the Sorts of (U1 "\/"_os U2) by PBOOLE:def_18; the Sorts of U1 c= A by PBOOLE:14; then the Sorts of U1 c= the Sorts of (U1 "\/"_os U2) by A3, PBOOLE:13; then A4: the Sorts of U1 c= the Sorts of (U1 /\ (U1 "\/"_os U2)) by A2, PBOOLE:17; the Sorts of (U1 /\ (U1 "\/"_os U2)) c= the Sorts of U1 by A2, PBOOLE:15; then the Sorts of (U1 /\ (U1 "\/"_os U2)) = the Sorts of U1 by A4, PBOOLE:146; hence U1 /\ (U1 "\/"_os U2) = U1 by A1, MSUALG_2:def_9; ::_thesis: verum end; theorem Th41: :: OSALG_2:41 for S1 being OrderSortedSign for U0 being non-empty OSAlgebra of S1 for U1, U2 being strict OSSubAlgebra of U0 holds (U1 /\ U2) "\/"_os U2 = U2 proof let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1 for U1, U2 being strict OSSubAlgebra of U0 holds (U1 /\ U2) "\/"_os U2 = U2 let U0 be non-empty OSAlgebra of S1; ::_thesis: for U1, U2 being strict OSSubAlgebra of U0 holds (U1 /\ U2) "\/"_os U2 = U2 let U1, U2 be strict OSSubAlgebra of U0; ::_thesis: (U1 /\ U2) "\/"_os U2 = U2 reconsider u12 = the Sorts of (U1 /\ U2), u2 = the Sorts of U2 as MSSubset of U0 by MSUALG_2:def_9; A1: ( u12 is OrderSortedSet of S1 & u2 is OrderSortedSet of S1 ) by OSALG_1:17; then reconsider u12 = u12, u2 = u2 as OSSubset of U0 by Def2; ( u12 c= the Sorts of U0 & u2 c= the Sorts of U0 ) by PBOOLE:def_18; then u12 \/ u2 c= the Sorts of U0 by PBOOLE:16; then reconsider A = u12 \/ u2 as MSSubset of U0 by PBOOLE:def_18; A is OrderSortedSet of S1 by A1, Th2; then reconsider A = u12 \/ u2 as OSSubset of U0 by Def2; u12 = the Sorts of U1 /\ the Sorts of U2 by MSUALG_2:def_16; then u12 c= u2 by PBOOLE:15; then A2: A = u2 by PBOOLE:22; (U1 /\ U2) "\/"_os U2 = GenOSAlg A by Def13; hence (U1 /\ U2) "\/"_os U2 = U2 by A2, Th35; ::_thesis: verum end; begin definition let S1 be OrderSortedSign; let OU0 be OSAlgebra of S1; func OSSub OU0 -> set means :Def14: :: OSALG_2:def 14 for x being set holds ( x in it iff x is strict OSSubAlgebra of OU0 ); existence ex b1 being set st for x being set holds ( x in b1 iff x is strict OSSubAlgebra of OU0 ) proof set X = { (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum } ; take { (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum } ; ::_thesis: for x being set holds ( x in { (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum } iff x is strict OSSubAlgebra of OU0 ) let x be set ; ::_thesis: ( x in { (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum } iff x is strict OSSubAlgebra of OU0 ) thus ( x in { (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum } implies x is strict OSSubAlgebra of OU0 ) ::_thesis: ( x is strict OSSubAlgebra of OU0 implies x in { (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum } ) proof assume x in { (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum } ; ::_thesis: x is strict OSSubAlgebra of OU0 then ex A being Element of OSSubSort OU0 st x = GenOSAlg (@ A) ; hence x is strict OSSubAlgebra of OU0 ; ::_thesis: verum end; assume x is strict OSSubAlgebra of OU0 ; ::_thesis: x in { (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum } then reconsider a = x as strict OSSubAlgebra of OU0 ; reconsider A = the Sorts of a as OSSubset of OU0 by Th5; A is opers_closed by Th5; then reconsider h = A as Element of OSSubSort OU0 by Th20; a = GenOSAlg (@ h) by Th35; hence x in { (GenOSAlg (@ A)) where A is Element of OSSubSort OU0 : verum } ; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff x is strict OSSubAlgebra of OU0 ) ) & ( for x being set holds ( x in b2 iff x is strict OSSubAlgebra of OU0 ) ) holds b1 = b2 proof defpred S1[ set ] means \$1 is strict OSSubAlgebra of OU0; thus for X1, X2 being set st ( for x being set holds ( x in X1 iff S1[x] ) ) & ( for x being set holds ( x in X2 iff S1[x] ) ) holds X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum end; end; :: deftheorem Def14 defines OSSub OSALG_2:def_14_:_ for S1 being OrderSortedSign for OU0 being OSAlgebra of S1 for b3 being set holds ( b3 = OSSub OU0 iff for x being set holds ( x in b3 iff x is strict OSSubAlgebra of OU0 ) ); theorem Th42: :: OSALG_2:42 for S1 being OrderSortedSign for OU0 being OSAlgebra of S1 holds OSSub OU0 c= MSSub OU0 proof let S1 be OrderSortedSign; ::_thesis: for OU0 being OSAlgebra of S1 holds OSSub OU0 c= MSSub OU0 let OU0 be OSAlgebra of S1; ::_thesis: OSSub OU0 c= MSSub OU0 let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in OSSub OU0 or x in MSSub OU0 ) assume x in OSSub OU0 ; ::_thesis: x in MSSub OU0 then x is strict MSSubAlgebra of OU0 by Def14; hence x in MSSub OU0 by MSUALG_2:def_19; ::_thesis: verum end; registration let S be OrderSortedSign; let U0 be OSAlgebra of S; cluster OSSub U0 -> non empty ; coherence not OSSub U0 is empty proof set x = the strict OSSubAlgebra of U0; the strict OSSubAlgebra of U0 in OSSub U0 by Def14; hence not OSSub U0 is empty ; ::_thesis: verum end; end; definition let S1 be OrderSortedSign; let OU0 be OSAlgebra of S1; :: original: OSSub redefine func OSSub OU0 -> Subset of (MSSub OU0); coherence OSSub OU0 is Subset of (MSSub OU0) by Th42; end; definition let S1 be OrderSortedSign; let U0 be non-empty OSAlgebra of S1; func OSAlg_join U0 -> BinOp of (OSSub U0) means :Def15: :: OSALG_2:def 15 for x, y being Element of OSSub U0 for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds it . (x,y) = U1 "\/"_os U2; existence ex b1 being BinOp of (OSSub U0) st for x, y being Element of OSSub U0 for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds b1 . (x,y) = U1 "\/"_os U2 proof defpred S1[ Element of OSSub U0, Element of OSSub U0, set ] means for U1, U2 being strict OSSubAlgebra of U0 st \$1 = U1 & \$2 = U2 holds \$3 = U1 "\/"_os U2; A1: for x, y being Element of OSSub U0 ex z being Element of OSSub U0 st S1[x,y,z] proof let x, y be Element of OSSub U0; ::_thesis: ex z being Element of OSSub U0 st S1[x,y,z] reconsider U1 = x, U2 = y as strict OSSubAlgebra of U0 by Def14; reconsider z = U1 "\/"_os U2 as Element of OSSub U0 by Def14; take z ; ::_thesis: S1[x,y,z] thus S1[x,y,z] ; ::_thesis: verum end; consider o being BinOp of (OSSub U0) such that A2: for a, b being Element of OSSub U0 holds S1[a,b,o . (a,b)] from BINOP_1:sch_3(A1); take o ; ::_thesis: for x, y being Element of OSSub U0 for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds o . (x,y) = U1 "\/"_os U2 thus for x, y being Element of OSSub U0 for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds o . (x,y) = U1 "\/"_os U2 by A2; ::_thesis: verum end; uniqueness for b1, b2 being BinOp of (OSSub U0) st ( for x, y being Element of OSSub U0 for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds b1 . (x,y) = U1 "\/"_os U2 ) & ( for x, y being Element of OSSub U0 for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds b2 . (x,y) = U1 "\/"_os U2 ) holds b1 = b2 proof let o1, o2 be BinOp of (OSSub U0); ::_thesis: ( ( for x, y being Element of OSSub U0 for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds o1 . (x,y) = U1 "\/"_os U2 ) & ( for x, y being Element of OSSub U0 for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds o2 . (x,y) = U1 "\/"_os U2 ) implies o1 = o2 ) assume that A3: for x, y being Element of OSSub U0 for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds o1 . (x,y) = U1 "\/"_os U2 and A4: for x, y being Element of OSSub U0 for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds o2 . (x,y) = U1 "\/"_os U2 ; ::_thesis: o1 = o2 for x, y being Element of OSSub U0 holds o1 . (x,y) = o2 . (x,y) proof let x, y be Element of OSSub U0; ::_thesis: o1 . (x,y) = o2 . (x,y) reconsider U1 = x, U2 = y as strict OSSubAlgebra of U0 by Def14; o1 . (x,y) = U1 "\/"_os U2 by A3; hence o1 . (x,y) = o2 . (x,y) by A4; ::_thesis: verum end; hence o1 = o2 by BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def15 defines OSAlg_join OSALG_2:def_15_:_ for S1 being OrderSortedSign for U0 being non-empty OSAlgebra of S1 for b3 being BinOp of (OSSub U0) holds ( b3 = OSAlg_join U0 iff for x, y being Element of OSSub U0 for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds b3 . (x,y) = U1 "\/"_os U2 ); definition let S1 be OrderSortedSign; let U0 be non-empty OSAlgebra of S1; func OSAlg_meet U0 -> BinOp of (OSSub U0) means :Def16: :: OSALG_2:def 16 for x, y being Element of OSSub U0 for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds it . (x,y) = U1 /\ U2; existence ex b1 being BinOp of (OSSub U0) st for x, y being Element of OSSub U0 for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds b1 . (x,y) = U1 /\ U2 proof defpred S1[ Element of OSSub U0, Element of OSSub U0, set ] means for U1, U2 being strict OSSubAlgebra of U0 st \$1 = U1 & \$2 = U2 holds \$3 = U1 /\ U2; A1: for x, y being Element of OSSub U0 ex z being Element of OSSub U0 st S1[x,y,z] proof let x, y be Element of OSSub U0; ::_thesis: ex z being Element of OSSub U0 st S1[x,y,z] reconsider U1 = x, U2 = y as strict OSSubAlgebra of U0 by Def14; reconsider z = U1 /\ U2 as Element of OSSub U0 by Def14; take z ; ::_thesis: S1[x,y,z] thus S1[x,y,z] ; ::_thesis: verum end; consider o being BinOp of (OSSub U0) such that A2: for a, b being Element of OSSub U0 holds S1[a,b,o . (a,b)] from BINOP_1:sch_3(A1); take o ; ::_thesis: for x, y being Element of OSSub U0 for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds o . (x,y) = U1 /\ U2 thus for x, y being Element of OSSub U0 for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds o . (x,y) = U1 /\ U2 by A2; ::_thesis: verum end; uniqueness for b1, b2 being BinOp of (OSSub U0) st ( for x, y being Element of OSSub U0 for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds b1 . (x,y) = U1 /\ U2 ) & ( for x, y being Element of OSSub U0 for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds b2 . (x,y) = U1 /\ U2 ) holds b1 = b2 proof let o1, o2 be BinOp of (OSSub U0); ::_thesis: ( ( for x, y being Element of OSSub U0 for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds o1 . (x,y) = U1 /\ U2 ) & ( for x, y being Element of OSSub U0 for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds o2 . (x,y) = U1 /\ U2 ) implies o1 = o2 ) assume that A3: for x, y being Element of OSSub U0 for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds o1 . (x,y) = U1 /\ U2 and A4: for x, y being Element of OSSub U0 for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds o2 . (x,y) = U1 /\ U2 ; ::_thesis: o1 = o2 for x, y being Element of OSSub U0 holds o1 . (x,y) = o2 . (x,y) proof let x, y be Element of OSSub U0; ::_thesis: o1 . (x,y) = o2 . (x,y) reconsider U1 = x, U2 = y as strict OSSubAlgebra of U0 by Def14; o1 . (x,y) = U1 /\ U2 by A3; hence o1 . (x,y) = o2 . (x,y) by A4; ::_thesis: verum end; hence o1 = o2 by BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def16 defines OSAlg_meet OSALG_2:def_16_:_ for S1 being OrderSortedSign for U0 being non-empty OSAlgebra of S1 for b3 being BinOp of (OSSub U0) holds ( b3 = OSAlg_meet U0 iff for x, y being Element of OSSub U0 for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds b3 . (x,y) = U1 /\ U2 ); theorem Th43: :: OSALG_2:43 for S1 being OrderSortedSign for U0 being non-empty OSAlgebra of S1 for x, y being Element of OSSub U0 holds (OSAlg_meet U0) . (x,y) = (MSAlg_meet U0) . (x,y) proof let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1 for x, y being Element of OSSub U0 holds (OSAlg_meet U0) . (x,y) = (MSAlg_meet U0) . (x,y) let U0 be non-empty OSAlgebra of S1; ::_thesis: for x, y being Element of OSSub U0 holds (OSAlg_meet U0) . (x,y) = (MSAlg_meet U0) . (x,y) let x, y be Element of OSSub U0; ::_thesis: (OSAlg_meet U0) . (x,y) = (MSAlg_meet U0) . (x,y) ( x is strict OSSubAlgebra of U0 & y is strict OSSubAlgebra of U0 ) by Def14; then consider U1, U2 being strict OSSubAlgebra of U0 such that A1: ( x = U1 & y = U2 ) ; (OSAlg_meet U0) . (x,y) = U1 /\ U2 by A1, Def16 .= (MSAlg_meet U0) . (x,y) by A1, MSUALG_2:def_21 ; hence (OSAlg_meet U0) . (x,y) = (MSAlg_meet U0) . (x,y) ; ::_thesis: verum end; theorem Th44: :: OSALG_2:44 for S1 being OrderSortedSign for U0 being non-empty OSAlgebra of S1 holds OSAlg_join U0 is commutative proof let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1 holds OSAlg_join U0 is commutative let U0 be non-empty OSAlgebra of S1; ::_thesis: OSAlg_join U0 is commutative set o = OSAlg_join U0; for x, y being Element of OSSub U0 holds (OSAlg_join U0) . (x,y) = (OSAlg_join U0) . (y,x) proof let x, y be Element of OSSub U0; ::_thesis: (OSAlg_join U0) . (x,y) = (OSAlg_join U0) . (y,x) reconsider U1 = x, U2 = y as strict OSSubAlgebra of U0 by Def14; set B = the Sorts of U1 \/ the Sorts of U2; the Sorts of U2 is MSSubset of U0 by MSUALG_2:def_9; then A1: the Sorts of U2 c= the Sorts of U0 by PBOOLE:def_18; the Sorts of U1 is MSSubset of U0 by MSUALG_2:def_9; then the Sorts of U1 c= the Sorts of U0 by PBOOLE:def_18; then the Sorts of U1 \/ the Sorts of U2 c= the Sorts of U0 by A1, PBOOLE:16; then A2: the Sorts of U1 \/ the Sorts of U2 is MSSubset of U0 by PBOOLE:def_18; ( the Sorts of U1 is OrderSortedSet of S1 & the Sorts of U2 is OrderSortedSet of S1 ) by OSALG_1:17; then the Sorts of U1 \/ the Sorts of U2 is OrderSortedSet of S1 by Th2; then reconsider B = the Sorts of U1 \/ the Sorts of U2 as OSSubset of U0 by A2, Def2; A3: U1 "\/"_os U2 = GenOSAlg B by Def13; ( (OSAlg_join U0) . (x,y) = U1 "\/"_os U2 & (OSAlg_join U0) . (y,x) = U2 "\/"_os U1 ) by Def15; hence (OSAlg_join U0) . (x,y) = (OSAlg_join U0) . (y,x) by A3, Def13; ::_thesis: verum end; hence OSAlg_join U0 is commutative by BINOP_1:def_2; ::_thesis: verum end; theorem Th45: :: OSALG_2:45 for S1 being OrderSortedSign for U0 being non-empty OSAlgebra of S1 holds OSAlg_join U0 is associative proof let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1 holds OSAlg_join U0 is associative let U0 be non-empty OSAlgebra of S1; ::_thesis: OSAlg_join U0 is associative set o = OSAlg_join U0; for x, y, z being Element of OSSub U0 holds (OSAlg_join U0) . (x,((OSAlg_join U0) . (y,z))) = (OSAlg_join U0) . (((OSAlg_join U0) . (x,y)),z) proof let x, y, z be Element of OSSub U0; ::_thesis: (OSAlg_join U0) . (x,((OSAlg_join U0) . (y,z))) = (OSAlg_join U0) . (((OSAlg_join U0) . (x,y)),z) reconsider U1 = x, U2 = y, U3 = z as strict OSSubAlgebra of U0 by Def14; set B = the Sorts of U1 \/ ( the Sorts of U2 \/ the Sorts of U3); A1: the Sorts of U2 is OrderSortedSet of S1 by OSALG_1:17; the Sorts of U2 is MSSubset of U0 by MSUALG_2:def_9; then A2: the Sorts of U2 c= the Sorts of U0 by PBOOLE:def_18; the Sorts of U3 is MSSubset of U0 by MSUALG_2:def_9; then the Sorts of U3 c= the Sorts of U0 by PBOOLE:def_18; then A3: the Sorts of U2 \/ the Sorts of U3 c= the Sorts of U0 by A2, PBOOLE:16; then reconsider C1 = the Sorts of U2 \/ the Sorts of U3 as MSSubset of U0 by PBOOLE:def_18; the Sorts of U3 is OrderSortedSet of S1 by OSALG_1:17; then A4: the Sorts of U2 \/ the Sorts of U3 is OrderSortedSet of S1 by A1, Th2; then reconsider C = C1 as OSSubset of U0 by Def2; A5: the Sorts of U1 is OrderSortedSet of S1 by OSALG_1:17; then A6: the Sorts of U1 \/ ( the Sorts of U2 \/ the Sorts of U3) is OrderSortedSet of S1 by A4, Th2; the Sorts of U1 is MSSubset of U0 by MSUALG_2:def_9; then A7: the Sorts of U1 c= the Sorts of U0 by PBOOLE:def_18; then the Sorts of U1 \/ the Sorts of U2 c= the Sorts of U0 by A2, PBOOLE:16; then reconsider D1 = the Sorts of U1 \/ the Sorts of U2 as MSSubset of U0 by PBOOLE:def_18; (OSAlg_join U0) . (y,z) = U2 "\/"_os U3 by Def15; then A8: (OSAlg_join U0) . (x,((OSAlg_join U0) . (y,z))) = U1 "\/"_os (U2 "\/"_os U3) by Def15; the Sorts of U1 \/ the Sorts of U2 is OrderSortedSet of S1 by A5, A1, Th2; then reconsider D = D1 as OSSubset of U0 by Def2; A9: (OSAlg_join U0) . (x,y) = U1 "\/"_os U2 by Def15; the Sorts of U1 \/ ( the Sorts of U2 \/ the Sorts of U3) c= the Sorts of U0 by A7, A3, PBOOLE:16; then the Sorts of U1 \/ ( the Sorts of U2 \/ the Sorts of U3) is MSSubset of U0 by PBOOLE:def_18; then reconsider B = the Sorts of U1 \/ ( the Sorts of U2 \/ the Sorts of U3) as OSSubset of U0 by A6, Def2; A10: B = D \/ the Sorts of U3 by PBOOLE:28; A11: (U1 "\/"_os U2) "\/"_os U3 = (GenOSAlg D) "\/"_os U3 by Def13 .= GenOSAlg B by A10, Th37 ; U1 "\/"_os (U2 "\/"_os U3) = U1 "\/"_os (GenOSAlg C) by Def13 .= (GenOSAlg C) "\/"_os U1 by Th39 .= GenOSAlg B by Th37 ; hence (OSAlg_join U0) . (x,((OSAlg_join U0) . (y,z))) = (OSAlg_join U0) . (((OSAlg_join U0) . (x,y)),z) by A9, A8, A11, Def15; ::_thesis: verum end; hence OSAlg_join U0 is associative by BINOP_1:def_3; ::_thesis: verum end; theorem Th46: :: OSALG_2:46 for S1 being OrderSortedSign for U0 being non-empty OSAlgebra of S1 holds OSAlg_meet U0 is commutative proof let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1 holds OSAlg_meet U0 is commutative let U0 be non-empty OSAlgebra of S1; ::_thesis: OSAlg_meet U0 is commutative set o = OSAlg_meet U0; set m = MSAlg_meet U0; A1: MSAlg_meet U0 is commutative by MSUALG_2:31; for x, y being Element of OSSub U0 holds (OSAlg_meet U0) . (x,y) = (OSAlg_meet U0) . (y,x) proof let x, y be Element of OSSub U0; ::_thesis: (OSAlg_meet U0) . (x,y) = (OSAlg_meet U0) . (y,x) (OSAlg_meet U0) . (x,y) = (MSAlg_meet U0) . (x,y) by Th43 .= (MSAlg_meet U0) . (y,x) by A1, BINOP_1:def_2 .= (OSAlg_meet U0) . (y,x) by Th43 ; hence (OSAlg_meet U0) . (x,y) = (OSAlg_meet U0) . (y,x) ; ::_thesis: verum end; hence OSAlg_meet U0 is commutative by BINOP_1:def_2; ::_thesis: verum end; theorem Th47: :: OSALG_2:47 for S1 being OrderSortedSign for U0 being non-empty OSAlgebra of S1 holds OSAlg_meet U0 is associative proof let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1 holds OSAlg_meet U0 is associative let U0 be non-empty OSAlgebra of S1; ::_thesis: OSAlg_meet U0 is associative set o = OSAlg_meet U0; set m = MSAlg_meet U0; A1: MSAlg_meet U0 is associative by MSUALG_2:32; for x, y, z being Element of OSSub U0 holds (OSAlg_meet U0) . (x,((OSAlg_meet U0) . (y,z))) = (OSAlg_meet U0) . (((OSAlg_meet U0) . (x,y)),z) proof let x, y, z be Element of OSSub U0; ::_thesis: (OSAlg_meet U0) . (x,((OSAlg_meet U0) . (y,z))) = (OSAlg_meet U0) . (((OSAlg_meet U0) . (x,y)),z) A2: (OSAlg_meet U0) . (x,y) = (MSAlg_meet U0) . (x,y) by Th43; (OSAlg_meet U0) . (y,z) = (MSAlg_meet U0) . (y,z) by Th43; then (OSAlg_meet U0) . (x,((OSAlg_meet U0) . (y,z))) = (MSAlg_meet U0) . (x,((MSAlg_meet U0) . (y,z))) by Th43 .= (MSAlg_meet U0) . (((MSAlg_meet U0) . (x,y)),z) by A1, BINOP_1:def_3 .= (OSAlg_meet U0) . (((OSAlg_meet U0) . (x,y)),z) by A2, Th43 ; hence (OSAlg_meet U0) . (x,((OSAlg_meet U0) . (y,z))) = (OSAlg_meet U0) . (((OSAlg_meet U0) . (x,y)),z) ; ::_thesis: verum end; hence OSAlg_meet U0 is associative by BINOP_1:def_3; ::_thesis: verum end; definition let S1 be OrderSortedSign; let U0 be non-empty OSAlgebra of S1; func OSSubAlLattice U0 -> strict Lattice equals :: OSALG_2:def 17 LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #); coherence LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is strict Lattice proof set L = LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #); A1: for a, b, c being Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) holds a "\/" (b "\/" c) = (a "\/" b) "\/" c proof let a, b, c be Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #); ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c OSAlg_join U0 is associative by Th45; hence a "\/" (b "\/" c) = (a "\/" b) "\/" c by BINOP_1:def_3; ::_thesis: verum end; A2: for a, b being Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) holds a "/\" b = b "/\" a proof let a, b be Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #); ::_thesis: a "/\" b = b "/\" a OSAlg_meet U0 is commutative by Th46; hence a "/\" b = b "/\" a by BINOP_1:def_2; ::_thesis: verum end; A3: for a, b being Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) holds a "/\" (a "\/" b) = a proof let a, b be Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #); ::_thesis: a "/\" (a "\/" b) = a reconsider x = a, y = b as Element of OSSub U0 ; (OSAlg_meet U0) . (x,((OSAlg_join U0) . (x,y))) = x proof reconsider U1 = x, U2 = y as strict OSSubAlgebra of U0 by Def14; (OSAlg_join U0) . (x,y) = U1 "\/"_os U2 by Def15; hence (OSAlg_meet U0) . (x,((OSAlg_join U0) . (x,y))) = U1 /\ (U1 "\/"_os U2) by Def16 .= x by Th40 ; ::_thesis: verum end; hence a "/\" (a "\/" b) = a ; ::_thesis: verum end; A4: for a, b being Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) holds (a "/\" b) "\/" b = b proof let a, b be Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #); ::_thesis: (a "/\" b) "\/" b = b reconsider x = a, y = b as Element of OSSub U0 ; (OSAlg_join U0) . (((OSAlg_meet U0) . (x,y)),y) = y proof reconsider U1 = x, U2 = y as strict OSSubAlgebra of U0 by Def14; (OSAlg_meet U0) . (x,y) = U1 /\ U2 by Def16; hence (OSAlg_join U0) . (((OSAlg_meet U0) . (x,y)),y) = (U1 /\ U2) "\/"_os U2 by Def15 .= y by Th41 ; ::_thesis: verum end; hence (a "/\" b) "\/" b = b ; ::_thesis: verum end; A5: for a, b, c being Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) holds a "/\" (b "/\" c) = (a "/\" b) "/\" c proof let a, b, c be Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #); ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c OSAlg_meet U0 is associative by Th47; hence a "/\" (b "/\" c) = (a "/\" b) "/\" c by BINOP_1:def_3; ::_thesis: verum end; for a, b being Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) holds a "\/" b = b "\/" a proof let a, b be Element of LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #); ::_thesis: a "\/" b = b "\/" a OSAlg_join U0 is commutative by Th44; hence a "\/" b = b "\/" a by BINOP_1:def_2; ::_thesis: verum end; then ( LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is strict & LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is join-commutative & LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is join-associative & LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is meet-absorbing & LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is meet-commutative & LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is meet-associative & LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is join-absorbing ) by A1, A4, A2, A5, A3, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9; hence LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #) is strict Lattice ; ::_thesis: verum end; end; :: deftheorem defines OSSubAlLattice OSALG_2:def_17_:_ for S1 being OrderSortedSign for U0 being non-empty OSAlgebra of S1 holds OSSubAlLattice U0 = LattStr(# (OSSub U0),(OSAlg_join U0),(OSAlg_meet U0) #); theorem Th48: :: OSALG_2:48 for S1 being OrderSortedSign for U0 being non-empty OSAlgebra of S1 holds OSSubAlLattice U0 is bounded proof let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1 holds OSSubAlLattice U0 is bounded let U0 be non-empty OSAlgebra of S1; ::_thesis: OSSubAlLattice U0 is bounded set L = OSSubAlLattice U0; thus OSSubAlLattice U0 is lower-bounded :: according to LATTICES:def_15 ::_thesis: OSSubAlLattice U0 is upper-bounded proof set C = OSConstants U0; reconsider G = GenOSAlg (OSConstants U0) as Element of OSSub U0 by Def14; reconsider G1 = G as Element of (OSSubAlLattice U0) ; take G1 ; :: according to LATTICES:def_13 ::_thesis: for b1 being Element of the carrier of (OSSubAlLattice U0) holds ( G1 "/\" b1 = G1 & b1 "/\" G1 = G1 ) let a be Element of (OSSubAlLattice U0); ::_thesis: ( G1 "/\" a = G1 & a "/\" G1 = G1 ) reconsider a1 = a as Element of OSSub U0 ; reconsider a2 = a1 as strict OSSubAlgebra of U0 by Def14; thus G1 "/\" a = (GenOSAlg (OSConstants U0)) /\ a2 by Def16 .= G1 by Th36 ; ::_thesis: a "/\" G1 = G1 hence a "/\" G1 = G1 ; ::_thesis: verum end; thus OSSubAlLattice U0 is upper-bounded ::_thesis: verum proof reconsider B = the Sorts of U0 as MSSubset of U0 by PBOOLE:def_18; the Sorts of U0 is OrderSortedSet of S1 by OSALG_1:17; then reconsider B = B as OSSubset of U0 by Def2; reconsider G = GenOSAlg B as Element of OSSub U0 by Def14; reconsider G1 = G as Element of (OSSubAlLattice U0) ; take G1 ; :: according to LATTICES:def_14 ::_thesis: for b1 being Element of the carrier of (OSSubAlLattice U0) holds ( G1 "\/" b1 = G1 & b1 "\/" G1 = G1 ) let a be Element of (OSSubAlLattice U0); ::_thesis: ( G1 "\/" a = G1 & a "\/" G1 = G1 ) reconsider a1 = a as Element of OSSub U0 ; reconsider a2 = a1 as strict OSSubAlgebra of U0 by Def14; thus G1 "\/" a = (GenOSAlg B) "\/"_os a2 by Def15 .= G1 by Th38 ; ::_thesis: a "\/" G1 = G1 hence a "\/" G1 = G1 ; ::_thesis: verum end; end; registration let S1 be OrderSortedSign; let U0 be non-empty OSAlgebra of S1; cluster OSSubAlLattice U0 -> strict bounded ; coherence OSSubAlLattice U0 is bounded by Th48; end; theorem :: OSALG_2:49 for S1 being OrderSortedSign for U0 being non-empty OSAlgebra of S1 holds Bottom (OSSubAlLattice U0) = GenOSAlg (OSConstants U0) proof let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1 holds Bottom (OSSubAlLattice U0) = GenOSAlg (OSConstants U0) let U0 be non-empty OSAlgebra of S1; ::_thesis: Bottom (OSSubAlLattice U0) = GenOSAlg (OSConstants U0) set C = OSConstants U0; reconsider G = GenOSAlg (OSConstants U0) as Element of OSSub U0 by Def14; set L = OSSubAlLattice U0; reconsider G1 = G as Element of (OSSubAlLattice U0) ; now__::_thesis:_for_a_being_Element_of_(OSSubAlLattice_U0)_holds_ (_G1_"/\"_a_=_G1_&_a_"/\"_G1_=_G1_) let a be Element of (OSSubAlLattice U0); ::_thesis: ( G1 "/\" a = G1 & a "/\" G1 = G1 ) reconsider a1 = a as Element of OSSub U0 ; reconsider a2 = a1 as strict OSSubAlgebra of U0 by Def14; thus G1 "/\" a = (GenOSAlg (OSConstants U0)) /\ a2 by Def16 .= G1 by Th36 ; ::_thesis: a "/\" G1 = G1 hence a "/\" G1 = G1 ; ::_thesis: verum end; hence Bottom (OSSubAlLattice U0) = GenOSAlg (OSConstants U0) by LATTICES:def_16; ::_thesis: verum end; theorem Th50: :: OSALG_2:50 for S1 being OrderSortedSign for U0 being non-empty OSAlgebra of S1 for B being OSSubset of U0 st B = the Sorts of U0 holds Top (OSSubAlLattice U0) = GenOSAlg B proof let S1 be OrderSortedSign; ::_thesis: for U0 being non-empty OSAlgebra of S1 for B being OSSubset of U0 st B = the Sorts of U0 holds Top (OSSubAlLattice U0) = GenOSAlg B let U0 be non-empty OSAlgebra of S1; ::_thesis: for B being OSSubset of U0 st B = the Sorts of U0 holds Top (OSSubAlLattice U0) = GenOSAlg B let B be OSSubset of U0; ::_thesis: ( B = the Sorts of U0 implies Top (OSSubAlLattice U0) = GenOSAlg B ) reconsider G = GenOSAlg B as Element of OSSub U0 by Def14; set L = OSSubAlLattice U0; reconsider G1 = G as Element of (OSSubAlLattice U0) ; assume A1: B = the Sorts of U0 ; ::_thesis: Top (OSSubAlLattice U0) = GenOSAlg B now__::_thesis:_for_a_being_Element_of_(OSSubAlLattice_U0)_holds_ (_G1_"\/"_a_=_G1_&_a_"\/"_G1_=_G1_) let a be Element of (OSSubAlLattice U0); ::_thesis: ( G1 "\/" a = G1 & a "\/" G1 = G1 ) reconsider a1 = a as Element of OSSub U0 ; reconsider a2 = a1 as strict OSSubAlgebra of U0 by Def14; thus G1 "\/" a = (GenOSAlg B) "\/"_os a2 by Def15 .= G1 by A1, Th38 ; ::_thesis: a "\/" G1 = G1 hence a "\/" G1 = G1 ; ::_thesis: verum end; hence Top (OSSubAlLattice U0) = GenOSAlg B by LATTICES:def_17; ::_thesis: verum end; theorem :: OSALG_2:51 for S1 being OrderSortedSign for U0 being strict non-empty OSAlgebra of S1 holds Top (OSSubAlLattice U0) = U0 proof let S1 be OrderSortedSign; ::_thesis: for U0 being strict non-empty OSAlgebra of S1 holds Top (OSSubAlLattice U0) = U0 let U0 be strict non-empty OSAlgebra of S1; ::_thesis: Top (OSSubAlLattice U0) = U0 reconsider B = the Sorts of U0 as MSSubset of U0 by PBOOLE:def_18; B is OrderSortedSet of S1 by OSALG_1:17; then reconsider B = the Sorts of U0 as OSSubset of U0 by Def2; thus Top (OSSubAlLattice U0) = GenOSAlg B by Th50 .= U0 by Th34 ; ::_thesis: verum end;