:: ROBBINS3 semantic presentation begin definition let L be non empty \/-SemiLattStr ; attrL is join-Associative means :Def1: :: ROBBINS3:def 1 for x, y, z being Element of L holds x "\/" (y "\/" z) = y "\/" (x "\/" z); end; :: deftheorem Def1 defines join-Associative ROBBINS3:def_1_:_ for L being non empty \/-SemiLattStr holds ( L is join-Associative iff for x, y, z being Element of L holds x "\/" (y "\/" z) = y "\/" (x "\/" z) ); definition let L be non empty /\-SemiLattStr ; attrL is meet-Associative means :Def2: :: ROBBINS3:def 2 for x, y, z being Element of L holds x "/\" (y "/\" z) = y "/\" (x "/\" z); end; :: deftheorem Def2 defines meet-Associative ROBBINS3:def_2_:_ for L being non empty /\-SemiLattStr holds ( L is meet-Associative iff for x, y, z being Element of L holds x "/\" (y "/\" z) = y "/\" (x "/\" z) ); definition let L be non empty LattStr ; attrL is meet-Absorbing means :Def3: :: ROBBINS3:def 3 for x, y being Element of L holds x "\/" (x "/\" y) = x; end; :: deftheorem Def3 defines meet-Absorbing ROBBINS3:def_3_:_ for L being non empty LattStr holds ( L is meet-Absorbing iff for x, y being Element of L holds x "\/" (x "/\" y) = x ); theorem Th1: :: ROBBINS3:1 for L being non empty LattStr st L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing holds ( L is meet-idempotent & L is join-idempotent ) proof let L be non empty LattStr ; ::_thesis: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing implies ( L is meet-idempotent & L is join-idempotent ) ) assume A1: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) ; ::_thesis: ( L is meet-idempotent & L is join-idempotent ) A2: for x being Element of L holds x "\/" x = x proof let a be Element of L; ::_thesis: a "\/" a = a a = a "\/" (a "/\" a) by A1, Def3; hence a "\/" a = a by A1, LATTICES:def_9; ::_thesis: verum end; for x being Element of L holds x "/\" x = x proof let a be Element of L; ::_thesis: a "/\" a = a a = a "/\" (a "\/" a) by A1, LATTICES:def_9; hence a "/\" a = a by A1, Def3; ::_thesis: verum end; hence ( L is meet-idempotent & L is join-idempotent ) by A2, ROBBINS1:def_7, SHEFFER1:def_9; ::_thesis: verum end; theorem Th2: :: ROBBINS3:2 for L being non empty LattStr st L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing holds ( L is meet-commutative & L is join-commutative ) proof let L be non empty LattStr ; ::_thesis: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing implies ( L is meet-commutative & L is join-commutative ) ) assume A1: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) ; ::_thesis: ( L is meet-commutative & L is join-commutative ) then A2: ( L is join-idempotent & L is meet-idempotent ) by Th1; A3: for x, y being Element of L holds x "/\" y = y "/\" x proof let a, b be Element of L; ::_thesis: a "/\" b = b "/\" a a "/\" b = a "/\" (b "/\" (b "\/" a)) by A1, LATTICES:def_9 .= b "/\" (a "/\" (b "\/" a)) by A1, Def2 .= b "/\" (a "/\" (b "\/" (a "\/" a))) by A2, ROBBINS1:def_7 .= b "/\" (a "/\" (a "\/" (b "\/" a))) by A1, Def1 .= b "/\" a by A1, LATTICES:def_9 ; hence a "/\" b = b "/\" a ; ::_thesis: verum end; for x, y being Element of L holds x "\/" y = y "\/" x proof let a, b be Element of L; ::_thesis: a "\/" b = b "\/" a a "\/" b = a "\/" (b "\/" (b "/\" a)) by A1, Def3 .= b "\/" (a "\/" (b "/\" a)) by A1, Def1 .= b "\/" (a "\/" (b "/\" (a "/\" a))) by A2, SHEFFER1:def_9 .= b "\/" (a "\/" (a "/\" (b "/\" a))) by A1, Def2 .= b "\/" a by A1, Def3 ; hence a "\/" b = b "\/" a ; ::_thesis: verum end; hence ( L is meet-commutative & L is join-commutative ) by A3, LATTICES:def_4, LATTICES:def_6; ::_thesis: verum end; theorem Th3: :: ROBBINS3:3 for L being non empty LattStr st L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing holds L is meet-absorbing proof let L be non empty LattStr ; ::_thesis: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing implies L is meet-absorbing ) assume A1: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) ; ::_thesis: L is meet-absorbing then A2: ( L is meet-commutative & L is join-commutative ) by Th2; for x, y being Element of L holds (x "/\" y) "\/" y = y proof let a, b be Element of L; ::_thesis: (a "/\" b) "\/" b = b b = b "\/" (b "/\" a) by A1, Def3 .= b "\/" (a "/\" b) by A2, LATTICES:def_6 .= (a "/\" b) "\/" b by A2, LATTICES:def_4 ; hence (a "/\" b) "\/" b = b ; ::_thesis: verum end; hence L is meet-absorbing by LATTICES:def_8; ::_thesis: verum end; theorem Th4: :: ROBBINS3:4 for L being non empty LattStr st L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing holds ( L is meet-associative & L is join-associative ) proof let L be non empty LattStr ; ::_thesis: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing implies ( L is meet-associative & L is join-associative ) ) assume A1: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) ; ::_thesis: ( L is meet-associative & L is join-associative ) then A2: ( L is meet-commutative & L is join-commutative ) by Th2; A3: for x, y, z being Element of L holds x "\/" (y "\/" z) = (x "\/" y) "\/" z proof let a, b, c be Element of L; ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c a "\/" (b "\/" c) = a "\/" (c "\/" b) by A2, LATTICES:def_4 .= c "\/" (a "\/" b) by A1, Def1 .= (a "\/" b) "\/" c by A2, LATTICES:def_4 ; hence a "\/" (b "\/" c) = (a "\/" b) "\/" c ; ::_thesis: verum end; for x, y, z being Element of L holds x "/\" (y "/\" z) = (x "/\" y) "/\" z proof let a, b, c be Element of L; ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c a "/\" (b "/\" c) = a "/\" (c "/\" b) by A2, LATTICES:def_6 .= c "/\" (a "/\" b) by A1, Def2 .= (a "/\" b) "/\" c by A2, LATTICES:def_6 ; hence a "/\" (b "/\" c) = (a "/\" b) "/\" c ; ::_thesis: verum end; hence ( L is meet-associative & L is join-associative ) by A3, LATTICES:def_5, LATTICES:def_7; ::_thesis: verum end; theorem Th5: :: ROBBINS3:5 for L being non empty LattStr holds ( L is Lattice-like iff ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) ) proof let L be non empty LattStr ; ::_thesis: ( L is Lattice-like iff ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) ) A1: ( L is Lattice-like implies ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) ) proof assume A2: L is Lattice-like ; ::_thesis: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) A3: for x, y, z being Element of L holds x "/\" (y "/\" z) = y "/\" (x "/\" z) proof let a, b, c be Element of L; ::_thesis: a "/\" (b "/\" c) = b "/\" (a "/\" c) a "/\" (b "/\" c) = (a "/\" b) "/\" c by A2, LATTICES:def_7 .= (b "/\" a) "/\" c by A2, LATTICES:def_6 .= b "/\" (a "/\" c) by A2, LATTICES:def_7 ; hence a "/\" (b "/\" c) = b "/\" (a "/\" c) ; ::_thesis: verum end; A4: for x, y being Element of L holds x "\/" (x "/\" y) = x proof let a, b be Element of L; ::_thesis: a "\/" (a "/\" b) = a a = (b "/\" a) "\/" a by A2, LATTICES:def_8 .= (a "/\" b) "\/" a by A2, LATTICES:def_6 .= a "\/" (a "/\" b) by A2, LATTICES:def_4 ; hence a "\/" (a "/\" b) = a ; ::_thesis: verum end; for x, y, z being Element of L holds x "\/" (y "\/" z) = y "\/" (x "\/" z) proof let a, b, c be Element of L; ::_thesis: a "\/" (b "\/" c) = b "\/" (a "\/" c) a "\/" (b "\/" c) = (a "\/" b) "\/" c by A2, LATTICES:def_5 .= (b "\/" a) "\/" c by A2, LATTICES:def_4 .= b "\/" (a "\/" c) by A2, LATTICES:def_5 ; hence a "\/" (b "\/" c) = b "\/" (a "\/" c) ; ::_thesis: verum end; hence ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) by A2, A3, A4, Def1, Def2, Def3; ::_thesis: verum end; ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing implies L is Lattice-like ) proof assume A5: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) ; ::_thesis: L is Lattice-like then A6: L is meet-absorbing by Th3; ( L is meet-commutative & L is join-commutative & L is meet-associative & L is join-associative ) by A5, Th2, Th4; hence L is Lattice-like by A5, A6; ::_thesis: verum end; hence ( L is Lattice-like iff ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) ) by A1; ::_thesis: verum end; registration cluster non empty Lattice-like -> non empty join-Associative meet-Associative meet-Absorbing for LattStr ; coherence for b1 being non empty LattStr st b1 is Lattice-like holds ( b1 is meet-Associative & b1 is join-Associative & b1 is meet-Absorbing ) by Th5; cluster non empty join-absorbing join-Associative meet-Associative meet-Absorbing -> non empty Lattice-like for LattStr ; coherence for b1 being non empty LattStr st b1 is meet-Associative & b1 is join-Associative & b1 is meet-Absorbing & b1 is join-absorbing holds b1 is Lattice-like by Th5; end; begin registration cluster non empty PartialOrdered OrderInvolutive -> non empty Dneg PartialOrdered for OrthoRelStr ; coherence for b1 being non empty PartialOrdered OrthoRelStr st b1 is OrderInvolutive holds b1 is Dneg proof let L be non empty PartialOrdered OrthoRelStr ; ::_thesis: ( L is OrderInvolutive implies L is Dneg ) assume L is OrderInvolutive ; ::_thesis: L is Dneg then consider f being Function of L,L such that A1: f = the Compl of L and A2: f is Orderinvolutive by OPOSET_1:def_18; ( f is V296() & f is antitone ) by A2, OPOSET_1:def_17; hence L is Dneg by A1, OPOSET_1:def_3; ::_thesis: verum end; end; theorem Th6: :: ROBBINS3:6 for L being non empty Dneg OrthoRelStr for x being Element of L holds (x `) ` = x proof let L be non empty Dneg OrthoRelStr ; ::_thesis: for x being Element of L holds (x `) ` = x let x be Element of L; ::_thesis: (x `) ` = x consider f being Function of L,L such that A1: f = the Compl of L and A2: f is V296() by OPOSET_1:def_3; ( f . x = x ` & f . (f . x) = x ) by A1, A2, PARTIT_2:def_3, ROBBINS1:def_3; hence (x `) ` = x by A1, ROBBINS1:def_3; ::_thesis: verum end; theorem Th7: :: ROBBINS3:7 for O being non empty PartialOrdered OrderInvolutive OrthoRelStr for x, y being Element of O st x <= y holds y ` <= x ` proof let O be non empty PartialOrdered OrderInvolutive OrthoRelStr ; ::_thesis: for x, y being Element of O st x <= y holds y ` <= x ` let x, y be Element of O; ::_thesis: ( x <= y implies y ` <= x ` ) assume A1: x <= y ; ::_thesis: y ` <= x ` consider f being Function of O,O such that A2: f = the Compl of O and A3: f is Orderinvolutive by OPOSET_1:def_18; ( f is V296() & f is antitone ) by A3, OPOSET_1:def_17; then f . x >= f . y by A1, WAYBEL_9:def_1; then x ` >= f . y by A2, ROBBINS1:def_3; hence y ` <= x ` by A2, ROBBINS1:def_3; ::_thesis: verum end; registration cluster non empty reflexive transitive antisymmetric with_suprema with_infima strict Dneg PartialOrdered Pure OrderInvolutive for OrthoRelStr ; existence ex b1 being PreOrthoPoset st ( b1 is with_infima & b1 is with_suprema & b1 is strict ) proof take TrivOrthoRelStr ; ::_thesis: ( TrivOrthoRelStr is with_infima & TrivOrthoRelStr is with_suprema & TrivOrthoRelStr is strict ) thus ( TrivOrthoRelStr is with_infima & TrivOrthoRelStr is with_suprema & TrivOrthoRelStr is strict ) ; ::_thesis: verum end; end; notation let L be non empty \/-SemiLattStr ; let x, y be Element of L; synonym x |_| y for x "\/" y; end; notation let L be non empty /\-SemiLattStr ; let x, y be Element of L; synonym x |^| y for x "/\" y; end; notation let L be non empty RelStr ; let x, y be Element of L; synonym x "|^|" y for x "/\" y; synonym x "|_|" y for x "\/" y; end; begin definition attrc1 is strict ; struct \/-SemiLattRelStr -> \/-SemiLattStr , RelStr ; aggr\/-SemiLattRelStr(# carrier, L_join, InternalRel #) -> \/-SemiLattRelStr ; end; definition attrc1 is strict ; struct /\-SemiLattRelStr -> /\-SemiLattStr , RelStr ; aggr/\-SemiLattRelStr(# carrier, L_meet, InternalRel #) -> /\-SemiLattRelStr ; end; definition attrc1 is strict ; struct LattRelStr -> /\-SemiLattRelStr , \/-SemiLattRelStr , LattStr ; aggrLattRelStr(# carrier, L_join, L_meet, InternalRel #) -> LattRelStr ; end; definition func TrivLattRelStr -> LattRelStr equals :: ROBBINS3:def 4 LattRelStr(# 1,op2,op2,(id 1) #); coherence LattRelStr(# 1,op2,op2,(id 1) #) is LattRelStr ; end; :: deftheorem defines TrivLattRelStr ROBBINS3:def_4_:_ TrivLattRelStr = LattRelStr(# 1,op2,op2,(id 1) #); registration cluster TrivLattRelStr -> 1 -element ; coherence TrivLattRelStr is 1 -element proof the carrier of TrivLattRelStr = {0} by CARD_1:49; hence the carrier of TrivLattRelStr is 1 -element ; :: according to STRUCT_0:def_19 ::_thesis: verum end; end; registration cluster non empty for \/-SemiLattRelStr ; existence not for b1 being \/-SemiLattRelStr holds b1 is empty proof take TrivLattRelStr ; ::_thesis: not TrivLattRelStr is empty thus not TrivLattRelStr is empty ; ::_thesis: verum end; cluster non empty for /\-SemiLattRelStr ; existence not for b1 being /\-SemiLattRelStr holds b1 is empty proof take TrivLattRelStr ; ::_thesis: not TrivLattRelStr is empty thus not TrivLattRelStr is empty ; ::_thesis: verum end; cluster non empty for LattRelStr ; existence not for b1 being LattRelStr holds b1 is empty proof take TrivLattRelStr ; ::_thesis: not TrivLattRelStr is empty thus not TrivLattRelStr is empty ; ::_thesis: verum end; end; theorem :: ROBBINS3:8 for R being non empty RelStr st the InternalRel of R is_reflexive_in the carrier of R & the InternalRel of R is antisymmetric & the InternalRel of R is transitive holds ( R is reflexive & R is antisymmetric & R is transitive ) proof let r be non empty RelStr ; ::_thesis: ( the InternalRel of r is_reflexive_in the carrier of r & the InternalRel of r is antisymmetric & the InternalRel of r is transitive implies ( r is reflexive & r is antisymmetric & r is transitive ) ) set i = the InternalRel of r; set c = the carrier of r; assume that A1: the InternalRel of r is_reflexive_in the carrier of r and A2: ( the InternalRel of r is antisymmetric & the InternalRel of r is transitive ) ; ::_thesis: ( r is reflexive & r is antisymmetric & r is transitive ) A3: the InternalRel of r is_transitive_in field the InternalRel of r by A2, RELAT_2:def_16; A4: field the InternalRel of r = the carrier of r by A1, PARTIT_2:21; then the InternalRel of r is_antisymmetric_in the carrier of r by A2, RELAT_2:def_12; hence ( r is reflexive & r is antisymmetric & r is transitive ) by A1, A4, A3, ORDERS_2:def_2, ORDERS_2:def_3, ORDERS_2:def_4; ::_thesis: verum end; registration cluster TrivLattRelStr -> reflexive ; coherence TrivLattRelStr is reflexive proof set T = TrivLattRelStr ; set C = the carrier of TrivLattRelStr; set I = the InternalRel of TrivLattRelStr; field the InternalRel of TrivLattRelStr = the carrier of TrivLattRelStr by PARTIT_2:18; then the InternalRel of TrivLattRelStr is_reflexive_in the carrier of TrivLattRelStr by RELAT_2:def_9; hence TrivLattRelStr is reflexive by ORDERS_2:def_2; ::_thesis: verum end; end; registration cluster reflexive transitive antisymmetric with_suprema with_infima for LattRelStr ; existence ex b1 being LattRelStr st ( b1 is antisymmetric & b1 is reflexive & b1 is transitive & b1 is with_suprema & b1 is with_infima ) proof take TrivLattRelStr ; ::_thesis: ( TrivLattRelStr is antisymmetric & TrivLattRelStr is reflexive & TrivLattRelStr is transitive & TrivLattRelStr is with_suprema & TrivLattRelStr is with_infima ) thus ( TrivLattRelStr is antisymmetric & TrivLattRelStr is reflexive & TrivLattRelStr is transitive & TrivLattRelStr is with_suprema & TrivLattRelStr is with_infima ) ; ::_thesis: verum end; end; registration cluster TrivLattRelStr -> meet-Absorbing ; coherence TrivLattRelStr is meet-Absorbing ; end; Lm1: TrivLattRelStr is Lattice-like ; registration cluster non empty Lattice-like for LattRelStr ; existence ex b1 being non empty LattRelStr st b1 is Lattice-like by Lm1; end; definition let L be Lattice; :: original: LattRel redefine func LattRel L -> Order of the carrier of L; coherence LattRel L is Order of the carrier of L proof A1: LattRel L = { [p,q] where p, q is Element of L : p [= q } by FILTER_1:def_8; LattRel L c= [: the carrier of L, the carrier of L:] proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LattRel L or x in [: the carrier of L, the carrier of L:] ) assume x in LattRel L ; ::_thesis: x in [: the carrier of L, the carrier of L:] then ex p, q being Element of L st ( x = [p,q] & p [= q ) by A1; hence x in [: the carrier of L, the carrier of L:] by ZFMISC_1:87; ::_thesis: verum end; then reconsider R = LattRel L as Relation of the carrier of L ; A2: R is_antisymmetric_in the carrier of L proof let x, y be set ; :: according to RELAT_2:def_4 ::_thesis: ( not x in the carrier of L or not y in the carrier of L or not [x,y] in R or not [y,x] in R or x = y ) assume ( x in the carrier of L & y in the carrier of L ) ; ::_thesis: ( not [x,y] in R or not [y,x] in R or x = y ) then reconsider x9 = x, y9 = y as Element of L ; assume ( [x,y] in R & [y,x] in R ) ; ::_thesis: x = y then ( x9 [= y9 & y9 [= x9 ) by FILTER_1:31; hence x = y by LATTICES:8; ::_thesis: verum end; A3: R is_transitive_in the carrier of L proof let x, y, z be set ; :: according to RELAT_2:def_8 ::_thesis: ( not x in the carrier of L or not y in the carrier of L or not z in the carrier of L or not [x,y] in R or not [y,z] in R or [x,z] in R ) assume ( x in the carrier of L & y in the carrier of L & z in the carrier of L ) ; ::_thesis: ( not [x,y] in R or not [y,z] in R or [x,z] in R ) then reconsider x9 = x, y9 = y, z9 = z as Element of L ; assume ( [x,y] in R & [y,z] in R ) ; ::_thesis: [x,z] in R then ( x9 [= y9 & y9 [= z9 ) by FILTER_1:31; then x9 [= z9 by LATTICES:7; hence [x,z] in R by FILTER_1:31; ::_thesis: verum end; A4: R is_reflexive_in the carrier of L proof let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in the carrier of L or [x,x] in R ) assume x in the carrier of L ; ::_thesis: [x,x] in R then reconsider x = x as Element of L ; x [= x ; hence [x,x] in R by FILTER_1:31; ::_thesis: verum end; then ( dom R = the carrier of L & field R = the carrier of L ) by ORDERS_1:13; hence LattRel L is Order of the carrier of L by A4, A2, A3, PARTFUN1:def_2, RELAT_2:def_9, RELAT_2:def_12, RELAT_2:def_16; ::_thesis: verum end; end; begin definition attrc1 is strict ; struct OrthoLattRelStr -> LattRelStr , OrthoLattStr , OrthoRelStr ; aggrOrthoLattRelStr(# carrier, L_join, L_meet, InternalRel, Compl #) -> OrthoLattRelStr ; end; definition func TrivCLRelStr -> OrthoLattRelStr equals :: ROBBINS3:def 5 OrthoLattRelStr(# 1,op2,op2,(id 1),op1 #); coherence OrthoLattRelStr(# 1,op2,op2,(id 1),op1 #) is OrthoLattRelStr ; end; :: deftheorem defines TrivCLRelStr ROBBINS3:def_5_:_ TrivCLRelStr = OrthoLattRelStr(# 1,op2,op2,(id 1),op1 #); definition let L be non empty ComplStr ; attrL is involutive means :Def6: :: ROBBINS3:def 6 for x being Element of L holds (x `) ` = x; end; :: deftheorem Def6 defines involutive ROBBINS3:def_6_:_ for L being non empty ComplStr holds ( L is involutive iff for x being Element of L holds (x `) ` = x ); definition let L be non empty ComplLLattStr ; attrL is with_Top means :Def7: :: ROBBINS3:def 7 for x, y being Element of L holds x |_| (x `) = y |_| (y `); end; :: deftheorem Def7 defines with_Top ROBBINS3:def_7_:_ for L being non empty ComplLLattStr holds ( L is with_Top iff for x, y being Element of L holds x |_| (x `) = y |_| (y `) ); registration cluster TrivOrtLat -> involutive with_Top ; coherence ( TrivOrtLat is involutive & TrivOrtLat is with_Top ) proof thus TrivOrtLat is involutive ::_thesis: TrivOrtLat is with_Top proof let x be Element of TrivOrtLat; :: according to ROBBINS3:def_6 ::_thesis: (x `) ` = x thus (x `) ` = x by STRUCT_0:def_10; ::_thesis: verum end; thus TrivOrtLat is with_Top ::_thesis: verum proof let x, y be Element of TrivOrtLat; :: according to ROBBINS3:def_7 ::_thesis: x |_| (x `) = y |_| (y `) thus x |_| (x `) = y |_| (y `) by STRUCT_0:def_10; ::_thesis: verum end; end; end; registration cluster TrivCLRelStr -> 1 -element ; coherence TrivCLRelStr is 1 -element proof the carrier of TrivCLRelStr = {0} by CARD_1:49; hence the carrier of TrivCLRelStr is 1 -element ; :: according to STRUCT_0:def_19 ::_thesis: verum end; end; registration cluster TrivCLRelStr -> reflexive ; coherence TrivCLRelStr is reflexive proof for x being Element of TrivCLRelStr holds x <= x proof let x be Element of TrivCLRelStr; ::_thesis: x <= x [x,x] in id {{}} by CARD_1:49, RELAT_1:def_10; hence x <= x by CARD_1:49, ORDERS_2:def_5; ::_thesis: verum end; hence TrivCLRelStr is reflexive by YELLOW_0:def_1; ::_thesis: verum end; end; registration cluster TrivCLRelStr -> involutive with_Top ; coherence ( TrivCLRelStr is involutive & TrivCLRelStr is with_Top ) proof set L = TrivCLRelStr ; thus TrivCLRelStr is involutive ::_thesis: TrivCLRelStr is with_Top proof let x be Element of TrivCLRelStr; :: according to ROBBINS3:def_6 ::_thesis: (x `) ` = x thus (x `) ` = x by STRUCT_0:def_10; ::_thesis: verum end; thus TrivCLRelStr is with_Top ::_thesis: verum proof let x, y be Element of TrivCLRelStr; :: according to ROBBINS3:def_7 ::_thesis: x |_| (x `) = y |_| (y `) thus x |_| (x `) = y |_| (y `) by STRUCT_0:def_10; ::_thesis: verum end; end; end; registration cluster non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean de_Morgan upper-bounded' lower-bounded' distributive' complemented' join-Associative meet-Associative meet-Absorbing involutive with_Top for OrthoLattStr ; existence ex b1 being 1 -element OrthoLattStr st ( b1 is involutive & b1 is with_Top & b1 is de_Morgan & b1 is Lattice-like ) proof take TrivOrtLat ; ::_thesis: ( TrivOrtLat is involutive & TrivOrtLat is with_Top & TrivOrtLat is de_Morgan & TrivOrtLat is Lattice-like ) thus ( TrivOrtLat is involutive & TrivOrtLat is with_Top & TrivOrtLat is de_Morgan & TrivOrtLat is Lattice-like ) ; ::_thesis: verum end; end; definition mode Ortholattice is non empty Lattice-like de_Morgan involutive with_Top OrthoLattStr ; end; begin theorem Th9: :: ROBBINS3:9 for K, L being non empty LattStr st LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is join-commutative holds L is join-commutative proof let K, L be non empty LattStr ; ::_thesis: ( LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is join-commutative implies L is join-commutative ) assume that A1: LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) and A2: K is join-commutative ; ::_thesis: L is join-commutative L is join-commutative proof let x, y be Element of L; :: according to LATTICES:def_4 ::_thesis: x |_| y = y |_| x reconsider x9 = x, y9 = y as Element of K by A1; x9 |_| y9 = y9 |_| x9 by A2, LATTICES:def_4; hence x |_| y = y |_| x by A1; ::_thesis: verum end; hence L is join-commutative ; ::_thesis: verum end; theorem Th10: :: ROBBINS3:10 for K, L being non empty LattStr st LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is meet-commutative holds L is meet-commutative proof let K, L be non empty LattStr ; ::_thesis: ( LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is meet-commutative implies L is meet-commutative ) assume that A1: LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) and A2: K is meet-commutative ; ::_thesis: L is meet-commutative L is meet-commutative proof let x, y be Element of L; :: according to LATTICES:def_6 ::_thesis: x |^| y = y |^| x reconsider x9 = x, y9 = y as Element of K by A1; x9 "/\" y9 = y9 "/\" x9 by A2, LATTICES:def_6; hence x |^| y = y |^| x by A1; ::_thesis: verum end; hence L is meet-commutative ; ::_thesis: verum end; theorem Th11: :: ROBBINS3:11 for K, L being non empty LattStr st LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is join-associative holds L is join-associative proof let K, L be non empty LattStr ; ::_thesis: ( LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is join-associative implies L is join-associative ) assume that A1: LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) and A2: K is join-associative ; ::_thesis: L is join-associative L is join-associative proof let x, y, z be Element of L; :: according to LATTICES:def_5 ::_thesis: x |_| (y |_| z) = (x |_| y) |_| z reconsider x9 = x, y9 = y, z9 = z as Element of K by A1; (x9 |_| y9) |_| z9 = x9 |_| (y9 |_| z9) by A2, LATTICES:def_5; hence x |_| (y |_| z) = (x |_| y) |_| z by A1; ::_thesis: verum end; hence L is join-associative ; ::_thesis: verum end; theorem Th12: :: ROBBINS3:12 for K, L being non empty LattStr st LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is meet-associative holds L is meet-associative proof let K, L be non empty LattStr ; ::_thesis: ( LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is meet-associative implies L is meet-associative ) assume that A1: LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) and A2: K is meet-associative ; ::_thesis: L is meet-associative L is meet-associative proof let x, y, z be Element of L; :: according to LATTICES:def_7 ::_thesis: x |^| (y |^| z) = (x |^| y) |^| z reconsider x9 = x, y9 = y, z9 = z as Element of K by A1; (x9 "/\" y9) "/\" z9 = x9 "/\" (y9 "/\" z9) by A2, LATTICES:def_7; hence x |^| (y |^| z) = (x |^| y) |^| z by A1; ::_thesis: verum end; hence L is meet-associative ; ::_thesis: verum end; theorem Th13: :: ROBBINS3:13 for K, L being non empty LattStr st LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is join-absorbing holds L is join-absorbing proof let K, L be non empty LattStr ; ::_thesis: ( LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is join-absorbing implies L is join-absorbing ) assume that A1: LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) and A2: K is join-absorbing ; ::_thesis: L is join-absorbing L is join-absorbing proof let x, y be Element of L; :: according to LATTICES:def_9 ::_thesis: x |^| (x |_| y) = x reconsider x9 = x, y9 = y as Element of K by A1; x9 "/\" (x9 "\/" y9) = x9 by A2, LATTICES:def_9; hence x |^| (x |_| y) = x by A1; ::_thesis: verum end; hence L is join-absorbing ; ::_thesis: verum end; theorem Th14: :: ROBBINS3:14 for K, L being non empty LattStr st LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is meet-absorbing holds L is meet-absorbing proof let K, L be non empty LattStr ; ::_thesis: ( LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is meet-absorbing implies L is meet-absorbing ) assume that A1: LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) and A2: K is meet-absorbing ; ::_thesis: L is meet-absorbing L is meet-absorbing proof let x, y be Element of L; :: according to LATTICES:def_8 ::_thesis: (x |^| y) |_| y = y reconsider x9 = x, y9 = y as Element of K by A1; (x9 "/\" y9) "\/" y9 = y9 by A2, LATTICES:def_8; hence (x |^| y) |_| y = y by A1; ::_thesis: verum end; hence L is meet-absorbing ; ::_thesis: verum end; theorem :: ROBBINS3:15 for K, L being non empty LattStr st LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is Lattice-like holds L is Lattice-like proof let K, L be non empty LattStr ; ::_thesis: ( LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is Lattice-like implies L is Lattice-like ) assume ( LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is Lattice-like ) ; ::_thesis: L is Lattice-like then ( L is join-commutative & L is join-associative & L is meet-absorbing & L is meet-commutative & L is meet-associative & L is join-absorbing ) by Th9, Th10, Th11, Th12, Th13, Th14; hence L is Lattice-like ; ::_thesis: verum end; theorem :: ROBBINS3:16 for L1, L2 being non empty \/-SemiLattStr st \/-SemiLattStr(# the carrier of L1, the L_join of L1 #) = \/-SemiLattStr(# the carrier of L2, the L_join of L2 #) holds for a1, b1 being Element of L1 for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 holds a1 "\/" b1 = a2 "\/" b2 ; theorem :: ROBBINS3:17 for L1, L2 being non empty /\-SemiLattStr st /\-SemiLattStr(# the carrier of L1, the L_meet of L1 #) = /\-SemiLattStr(# the carrier of L2, the L_meet of L2 #) holds for a1, b1 being Element of L1 for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 holds a1 "/\" b1 = a2 "/\" b2 ; theorem Th18: :: ROBBINS3:18 for K, L being non empty ComplStr for x being Element of K for y being Element of L st the Compl of K = the Compl of L & x = y holds x ` = y ` proof let K, L be non empty ComplStr ; ::_thesis: for x being Element of K for y being Element of L st the Compl of K = the Compl of L & x = y holds x ` = y ` let x be Element of K; ::_thesis: for y being Element of L st the Compl of K = the Compl of L & x = y holds x ` = y ` let y be Element of L; ::_thesis: ( the Compl of K = the Compl of L & x = y implies x ` = y ` ) assume ( the Compl of K = the Compl of L & x = y ) ; ::_thesis: x ` = y ` then x ` = the Compl of L . y by ROBBINS1:def_3 .= y ` by ROBBINS1:def_3 ; hence x ` = y ` ; ::_thesis: verum end; theorem Th19: :: ROBBINS3:19 for K, L being non empty ComplLLattStr st ComplLLattStr(# the carrier of K, the L_join of K, the Compl of K #) = ComplLLattStr(# the carrier of L, the L_join of L, the Compl of L #) & K is with_Top holds L is with_Top proof let K, L be non empty ComplLLattStr ; ::_thesis: ( ComplLLattStr(# the carrier of K, the L_join of K, the Compl of K #) = ComplLLattStr(# the carrier of L, the L_join of L, the Compl of L #) & K is with_Top implies L is with_Top ) assume that A1: ComplLLattStr(# the carrier of K, the L_join of K, the Compl of K #) = ComplLLattStr(# the carrier of L, the L_join of L, the Compl of L #) and A2: K is with_Top ; ::_thesis: L is with_Top for x, y being Element of L holds x |_| (x `) = y |_| (y `) proof let x, y be Element of L; ::_thesis: x |_| (x `) = y |_| (y `) reconsider x9 = x, y9 = y as Element of K by A1; x |_| (x `) = x9 |_| (x9 `) by A1, Th18 .= y9 |_| (y9 `) by A2, Def7 .= y |_| (y `) by A1, Th18 ; hence x |_| (x `) = y |_| (y `) ; ::_thesis: verum end; hence L is with_Top by Def7; ::_thesis: verum end; theorem Th20: :: ROBBINS3:20 for K, L being non empty OrthoLattStr st OrthoLattStr(# the carrier of K, the L_join of K, the L_meet of K, the Compl of K #) = OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) & K is de_Morgan holds L is de_Morgan proof let K, L be non empty OrthoLattStr ; ::_thesis: ( OrthoLattStr(# the carrier of K, the L_join of K, the L_meet of K, the Compl of K #) = OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) & K is de_Morgan implies L is de_Morgan ) assume that A1: OrthoLattStr(# the carrier of K, the L_join of K, the L_meet of K, the Compl of K #) = OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) and A2: K is de_Morgan ; ::_thesis: L is de_Morgan for x, y being Element of L holds x "/\" y = ((x `) "\/" (y `)) ` proof let x, y be Element of L; ::_thesis: x "/\" y = ((x `) "\/" (y `)) ` reconsider x9 = x, y9 = y as Element of K by A1; A3: ( x ` = x9 ` & y ` = y9 ` ) by A1, Th18; x "/\" y = x9 "/\" y9 by A1 .= ((x9 `) "\/" (y9 `)) ` by A2, ROBBINS1:def_23 .= ((x `) "\/" (y `)) ` by A1, A3, Th18 ; hence x "/\" y = ((x `) "\/" (y `)) ` ; ::_thesis: verum end; hence L is de_Morgan by ROBBINS1:def_23; ::_thesis: verum end; theorem Th21: :: ROBBINS3:21 for K, L being non empty OrthoLattStr st OrthoLattStr(# the carrier of K, the L_join of K, the L_meet of K, the Compl of K #) = OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) & K is involutive holds L is involutive proof let K, L be non empty OrthoLattStr ; ::_thesis: ( OrthoLattStr(# the carrier of K, the L_join of K, the L_meet of K, the Compl of K #) = OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) & K is involutive implies L is involutive ) assume that A1: OrthoLattStr(# the carrier of K, the L_join of K, the L_meet of K, the Compl of K #) = OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) and A2: K is involutive ; ::_thesis: L is involutive for x being Element of L holds (x `) ` = x proof let x be Element of L; ::_thesis: (x `) ` = x reconsider x9 = x as Element of K by A1; x ` = x9 ` by A1, Th18; then (x `) ` = (x9 `) ` by A1, Th18 .= x by A2, Def6 ; hence (x `) ` = x ; ::_thesis: verum end; hence L is involutive by Def6; ::_thesis: verum end; begin definition let R be RelStr ; mode RelAugmentation of R -> LattRelStr means :: ROBBINS3:def 8 RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of R, the InternalRel of R #); existence ex b1 being LattRelStr st RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of R, the InternalRel of R #) proof set A = the BinOp of the carrier of R; set L = LattRelStr(# the carrier of R, the BinOp of the carrier of R, the BinOp of the carrier of R, the InternalRel of R #); take LattRelStr(# the carrier of R, the BinOp of the carrier of R, the BinOp of the carrier of R, the InternalRel of R #) ; ::_thesis: RelStr(# the carrier of LattRelStr(# the carrier of R, the BinOp of the carrier of R, the BinOp of the carrier of R, the InternalRel of R #), the InternalRel of LattRelStr(# the carrier of R, the BinOp of the carrier of R, the BinOp of the carrier of R, the InternalRel of R #) #) = RelStr(# the carrier of R, the InternalRel of R #) thus RelStr(# the carrier of LattRelStr(# the carrier of R, the BinOp of the carrier of R, the BinOp of the carrier of R, the InternalRel of R #), the InternalRel of LattRelStr(# the carrier of R, the BinOp of the carrier of R, the BinOp of the carrier of R, the InternalRel of R #) #) = RelStr(# the carrier of R, the InternalRel of R #) ; ::_thesis: verum end; end; :: deftheorem defines RelAugmentation ROBBINS3:def_8_:_ for R being RelStr for b2 being LattRelStr holds ( b2 is RelAugmentation of R iff RelStr(# the carrier of b2, the InternalRel of b2 #) = RelStr(# the carrier of R, the InternalRel of R #) ); definition let R be LattStr ; mode LatAugmentation of R -> LattRelStr means :Def9: :: ROBBINS3:def 9 LattStr(# the carrier of it, the L_join of it, the L_meet of it #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #); existence ex b1 being LattRelStr st LattStr(# the carrier of b1, the L_join of b1, the L_meet of b1 #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) proof set IR = the Relation of the carrier of R; set L = LattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R #); take LattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R #) ; ::_thesis: LattStr(# the carrier of LattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R #), the L_join of LattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R #), the L_meet of LattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R #) #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) thus LattStr(# the carrier of LattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R #), the L_join of LattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R #), the L_meet of LattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R #) #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) ; ::_thesis: verum end; end; :: deftheorem Def9 defines LatAugmentation ROBBINS3:def_9_:_ for R being LattStr for b2 being LattRelStr holds ( b2 is LatAugmentation of R iff LattStr(# the carrier of b2, the L_join of b2, the L_meet of b2 #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) ); registration let L be non empty LattStr ; cluster -> non empty for LatAugmentation of L; coherence for b1 being LatAugmentation of L holds not b1 is empty proof let R be LatAugmentation of L; ::_thesis: not R is empty LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) by Def9; hence not R is empty ; ::_thesis: verum end; end; registration let L be non empty meet-associative LattStr ; cluster -> meet-associative for LatAugmentation of L; coherence for b1 being LatAugmentation of L holds b1 is meet-associative proof let R be LatAugmentation of L; ::_thesis: R is meet-associative LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) by Def9; hence R is meet-associative by Th12; ::_thesis: verum end; end; registration let L be non empty join-associative LattStr ; cluster -> join-associative for LatAugmentation of L; coherence for b1 being LatAugmentation of L holds b1 is join-associative proof let R be LatAugmentation of L; ::_thesis: R is join-associative LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) by Def9; hence R is join-associative by Th11; ::_thesis: verum end; end; registration let L be non empty meet-commutative LattStr ; cluster -> meet-commutative for LatAugmentation of L; coherence for b1 being LatAugmentation of L holds b1 is meet-commutative proof let R be LatAugmentation of L; ::_thesis: R is meet-commutative LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) by Def9; hence R is meet-commutative by Th10; ::_thesis: verum end; end; registration let L be non empty join-commutative LattStr ; cluster -> join-commutative for LatAugmentation of L; coherence for b1 being LatAugmentation of L holds b1 is join-commutative proof let R be LatAugmentation of L; ::_thesis: R is join-commutative LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) by Def9; hence R is join-commutative by Th9; ::_thesis: verum end; end; registration let L be non empty join-absorbing LattStr ; cluster -> join-absorbing for LatAugmentation of L; coherence for b1 being LatAugmentation of L holds b1 is join-absorbing proof let R be LatAugmentation of L; ::_thesis: R is join-absorbing LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) by Def9; hence R is join-absorbing by Th13; ::_thesis: verum end; end; registration let L be non empty meet-absorbing LattStr ; cluster -> meet-absorbing for LatAugmentation of L; coherence for b1 being LatAugmentation of L holds b1 is meet-absorbing proof let R be LatAugmentation of L; ::_thesis: R is meet-absorbing LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) by Def9; hence R is meet-absorbing by Th14; ::_thesis: verum end; end; definition let L be non empty \/-SemiLattRelStr ; attrL is naturally_sup-generated means :Def10: :: ROBBINS3:def 10 for x, y being Element of L holds ( x <= y iff x |_| y = y ); end; :: deftheorem Def10 defines naturally_sup-generated ROBBINS3:def_10_:_ for L being non empty \/-SemiLattRelStr holds ( L is naturally_sup-generated iff for x, y being Element of L holds ( x <= y iff x |_| y = y ) ); definition let L be non empty /\-SemiLattRelStr ; attrL is naturally_inf-generated means :Def11: :: ROBBINS3:def 11 for x, y being Element of L holds ( x <= y iff x |^| y = x ); end; :: deftheorem Def11 defines naturally_inf-generated ROBBINS3:def_11_:_ for L being non empty /\-SemiLattRelStr holds ( L is naturally_inf-generated iff for x, y being Element of L holds ( x <= y iff x |^| y = x ) ); registration let L be Lattice; cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like join-Associative meet-Associative meet-Absorbing naturally_sup-generated naturally_inf-generated for LatAugmentation of L; existence ex b1 being LatAugmentation of L st ( b1 is naturally_sup-generated & b1 is naturally_inf-generated & b1 is Lattice-like ) proof set R = LattRel L; set S = LattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L) #); LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of LattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L) #), the L_join of LattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L) #), the L_meet of LattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L) #) #) ; then reconsider S = LattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L) #) as LatAugmentation of L by Def9; for x, y being Element of S holds ( x <= y iff x |^| y = x ) proof let x, y be Element of S; ::_thesis: ( x <= y iff x |^| y = x ) reconsider x9 = x, y9 = y as Element of L ; hereby ::_thesis: ( x |^| y = x implies x <= y ) assume x <= y ; ::_thesis: x |^| y = x then [x,y] in the InternalRel of S by ORDERS_2:def_5; then x9 [= y9 by FILTER_1:31; then x9 |^| y9 = x9 by LATTICES:4; hence x |^| y = x ; ::_thesis: verum end; A1: x9 |^| y9 = x |^| y ; assume x |^| y = x ; ::_thesis: x <= y then x9 [= y9 by A1, LATTICES:4; then [x9,y9] in LattRel L by FILTER_1:31; hence x <= y by ORDERS_2:def_5; ::_thesis: verum end; then A2: S is naturally_inf-generated by Def11; for x, y being Element of S holds ( x <= y iff x |_| y = y ) proof let x, y be Element of S; ::_thesis: ( x <= y iff x |_| y = y ) reconsider x9 = x, y9 = y as Element of L ; hereby ::_thesis: ( x |_| y = y implies x <= y ) assume x <= y ; ::_thesis: x |_| y = y then [x,y] in the InternalRel of S by ORDERS_2:def_5; then x9 [= y9 by FILTER_1:31; then x9 |_| y9 = y9 by LATTICES:def_3; hence x |_| y = y ; ::_thesis: verum end; A3: x9 |_| y9 = x |_| y ; assume x |_| y = y ; ::_thesis: x <= y then x9 [= y9 by A3, LATTICES:def_3; then [x9,y9] in LattRel L by FILTER_1:31; hence x <= y by ORDERS_2:def_5; ::_thesis: verum end; then S is naturally_sup-generated by Def10; hence ex b1 being LatAugmentation of L st ( b1 is naturally_sup-generated & b1 is naturally_inf-generated & b1 is Lattice-like ) by A2; ::_thesis: verum end; end; registration cluster1 -element reflexive for LattRelStr ; existence ex b1 being LattRelStr st ( b1 is 1 -element & b1 is reflexive ) proof take TrivLattRelStr ; ::_thesis: ( TrivLattRelStr is 1 -element & TrivLattRelStr is reflexive ) thus ( TrivLattRelStr is 1 -element & TrivLattRelStr is reflexive ) ; ::_thesis: verum end; end; registration cluster1 -element reflexive for OrthoLattRelStr ; existence ex b1 being OrthoLattRelStr st ( b1 is 1 -element & b1 is reflexive ) proof take TrivCLRelStr ; ::_thesis: ( TrivCLRelStr is 1 -element & TrivCLRelStr is reflexive ) thus ( TrivCLRelStr is 1 -element & TrivCLRelStr is reflexive ) ; ::_thesis: verum end; end; registration cluster1 -element reflexive for OrthoRelStr ; existence ex b1 being OrthoRelStr st ( b1 is 1 -element & b1 is reflexive ) proof take TrivOrthoRelStr ; ::_thesis: ( TrivOrthoRelStr is 1 -element & TrivOrthoRelStr is reflexive ) thus ( TrivOrthoRelStr is 1 -element & TrivOrthoRelStr is reflexive ) ; ::_thesis: verum end; end; registration cluster1 -element -> 1 -element well-complemented de_Morgan involutive with_Top for OrthoLattStr ; coherence for b1 being 1 -element OrthoLattStr holds ( b1 is involutive & b1 is with_Top & b1 is de_Morgan & b1 is well-complemented ) proof let L be 1 -element OrthoLattStr ; ::_thesis: ( L is involutive & L is with_Top & L is de_Morgan & L is well-complemented ) reconsider L9 = L as 1 -element OrthoLattStr ; A1: for x being Element of L9 holds (x `) ` = x by STRUCT_0:def_10; A2: for x being Element of L9 holds x ` is_a_complement_of x proof let x be Element of L9; ::_thesis: x ` is_a_complement_of x A3: ( (x `) |_| x = Top L9 & (x `) |^| x = Bottom L9 ) by STRUCT_0:def_10; ( x |_| (x `) = Top L9 & x |^| (x `) = Bottom L9 ) by STRUCT_0:def_10; hence x ` is_a_complement_of x by A3, LATTICES:def_18; ::_thesis: verum end; ( ( for x, y being Element of L9 holds x |_| (x `) = y |_| (y `) ) & ( for x, y being Element of L9 holds x |^| y = ((x `) |_| (y `)) ` ) ) by STRUCT_0:def_10; hence ( L is involutive & L is with_Top & L is de_Morgan & L is well-complemented ) by A1, A2, Def6, Def7, ROBBINS1:def_10, ROBBINS1:def_23; ::_thesis: verum end; end; registration cluster1 -element reflexive -> 1 -element reflexive PartialOrdered Pure OrderInvolutive for OrthoRelStr ; coherence for b1 being 1 -element reflexive OrthoRelStr holds ( b1 is OrderInvolutive & b1 is Pure & b1 is PartialOrdered ) proof let L be 1 -element reflexive OrthoRelStr ; ::_thesis: ( L is OrderInvolutive & L is Pure & L is PartialOrdered ) reconsider L9 = L as 1 -element reflexive OrthoRelStr ; reconsider f = the Compl of L9 as Function of L9,L9 ; consider x being set such that A1: the carrier of L9 = {x} by ZFMISC_1:131; f = id {x} by A1, FUNCT_2:51; then A2: f is V296() ; then A3: L9 is Dneg by OPOSET_1:def_3; for z, y being Element of L9 st z <= y holds f . z >= f . y proof let z, y be Element of L9; ::_thesis: ( z <= y implies f . z >= f . y ) assume z <= y ; ::_thesis: f . z >= f . y ( f . z = x & f . y = x ) by A1, FUNCT_2:50; hence f . z >= f . y by YELLOW_0:def_1; ::_thesis: verum end; then f is antitone by WAYBEL_9:def_1; then f is Orderinvolutive by A2, OPOSET_1:def_17; hence ( L is OrderInvolutive & L is Pure & L is PartialOrdered ) by A3, OPOSET_1:def_15, OPOSET_1:def_18; ::_thesis: verum end; end; registration cluster1 -element reflexive -> 1 -element reflexive naturally_sup-generated naturally_inf-generated for LattRelStr ; coherence for b1 being 1 -element reflexive LattRelStr holds ( b1 is naturally_sup-generated & b1 is naturally_inf-generated ) proof let L be 1 -element reflexive LattRelStr ; ::_thesis: ( L is naturally_sup-generated & L is naturally_inf-generated ) reconsider L9 = L as 1 -element reflexive LattRelStr ; ( ( for x, y being Element of L9 holds ( x <= y iff x |_| y = y ) ) & ( for x, y being Element of L9 holds ( x <= y iff x |^| y = x ) ) ) by STRUCT_0:def_10; hence ( L is naturally_sup-generated & L is naturally_inf-generated ) by Def10, Def11; ::_thesis: verum end; end; registration cluster non empty Lattice-like with_suprema with_infima de_Morgan PartialOrdered Pure OrderInvolutive naturally_sup-generated naturally_inf-generated for OrthoLattRelStr ; existence ex b1 being non empty OrthoLattRelStr st ( b1 is with_infima & b1 is with_suprema & b1 is naturally_sup-generated & b1 is naturally_inf-generated & b1 is de_Morgan & b1 is Lattice-like & b1 is OrderInvolutive & b1 is Pure & b1 is PartialOrdered ) proof take TrivCLRelStr ; ::_thesis: ( TrivCLRelStr is with_infima & TrivCLRelStr is with_suprema & TrivCLRelStr is naturally_sup-generated & TrivCLRelStr is naturally_inf-generated & TrivCLRelStr is de_Morgan & TrivCLRelStr is Lattice-like & TrivCLRelStr is OrderInvolutive & TrivCLRelStr is Pure & TrivCLRelStr is PartialOrdered ) thus ( TrivCLRelStr is with_infima & TrivCLRelStr is with_suprema & TrivCLRelStr is naturally_sup-generated & TrivCLRelStr is naturally_inf-generated & TrivCLRelStr is de_Morgan & TrivCLRelStr is Lattice-like & TrivCLRelStr is OrderInvolutive & TrivCLRelStr is Pure & TrivCLRelStr is PartialOrdered ) ; ::_thesis: verum end; end; registration cluster non empty Lattice-like with_suprema with_infima naturally_sup-generated naturally_inf-generated for LattRelStr ; existence ex b1 being non empty LattRelStr st ( b1 is with_infima & b1 is with_suprema & b1 is naturally_sup-generated & b1 is naturally_inf-generated & b1 is Lattice-like ) proof take TrivLattRelStr ; ::_thesis: ( TrivLattRelStr is with_infima & TrivLattRelStr is with_suprema & TrivLattRelStr is naturally_sup-generated & TrivLattRelStr is naturally_inf-generated & TrivLattRelStr is Lattice-like ) thus ( TrivLattRelStr is with_infima & TrivLattRelStr is with_suprema & TrivLattRelStr is naturally_sup-generated & TrivLattRelStr is naturally_inf-generated & TrivLattRelStr is Lattice-like ) ; ::_thesis: verum end; end; theorem Th22: :: ROBBINS3:22 for L being non empty naturally_sup-generated LattRelStr for x, y being Element of L holds ( x <= y iff x [= y ) proof let L be non empty naturally_sup-generated LattRelStr ; ::_thesis: for x, y being Element of L holds ( x <= y iff x [= y ) let x, y be Element of L; ::_thesis: ( x <= y iff x [= y ) hereby ::_thesis: ( x [= y implies x <= y ) assume x <= y ; ::_thesis: x [= y then x |_| y = y by Def10; hence x [= y by LATTICES:def_3; ::_thesis: verum end; assume x [= y ; ::_thesis: x <= y then x |_| y = y by LATTICES:def_3; hence x <= y by Def10; ::_thesis: verum end; theorem Th23: :: ROBBINS3:23 for L being non empty Lattice-like naturally_sup-generated LattRelStr holds RelStr(# the carrier of L, the InternalRel of L #) = LattPOSet L proof let L be non empty Lattice-like naturally_sup-generated LattRelStr ; ::_thesis: RelStr(# the carrier of L, the InternalRel of L #) = LattPOSet L A1: for x, y being set holds ( [x,y] in the InternalRel of L iff [x,y] in LattRel L ) proof let x, y be set ; ::_thesis: ( [x,y] in the InternalRel of L iff [x,y] in LattRel L ) hereby ::_thesis: ( [x,y] in LattRel L implies [x,y] in the InternalRel of L ) assume A2: [x,y] in the InternalRel of L ; ::_thesis: [x,y] in LattRel L then reconsider x9 = x, y9 = y as Element of L by ZFMISC_1:87; x9 <= y9 by A2, ORDERS_2:def_5; then x9 [= y9 by Th22; hence [x,y] in LattRel L by FILTER_1:31; ::_thesis: verum end; assume A3: [x,y] in LattRel L ; ::_thesis: [x,y] in the InternalRel of L then reconsider x9 = x, y9 = y as Element of L by ZFMISC_1:87; x9 [= y9 by A3, FILTER_1:31; then x9 <= y9 by Th22; hence [x,y] in the InternalRel of L by ORDERS_2:def_5; ::_thesis: verum end; LattPOSet L = RelStr(# the carrier of L,(LattRel L) #) by LATTICE3:def_2; hence RelStr(# the carrier of L, the InternalRel of L #) = LattPOSet L by A1, RELAT_1:def_2; ::_thesis: verum end; registration cluster non empty Lattice-like naturally_sup-generated -> non empty with_suprema with_infima for LattRelStr ; coherence for b1 being non empty LattRelStr st b1 is naturally_sup-generated & b1 is Lattice-like holds ( b1 is with_infima & b1 is with_suprema ) proof let L be non empty LattRelStr ; ::_thesis: ( L is naturally_sup-generated & L is Lattice-like implies ( L is with_infima & L is with_suprema ) ) assume ( L is naturally_sup-generated & L is Lattice-like ) ; ::_thesis: ( L is with_infima & L is with_suprema ) then reconsider L9 = L as non empty Lattice-like naturally_sup-generated LattRelStr ; ( LattPOSet L9 is with_suprema & LattPOSet L9 is with_infima ) ; then ( RelStr(# the carrier of L9, the InternalRel of L9 #) is with_suprema & RelStr(# the carrier of L9, the InternalRel of L9 #) is with_infima ) by Th23; hence ( L is with_infima & L is with_suprema ) by YELLOW_7:14, YELLOW_7:15; ::_thesis: verum end; end; begin definition let R be OrthoLattStr ; mode CLatAugmentation of R -> OrthoLattRelStr means :Def12: :: ROBBINS3:def 12 OrthoLattStr(# the carrier of it, the L_join of it, the L_meet of it, the Compl of it #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #); existence ex b1 being OrthoLattRelStr st OrthoLattStr(# the carrier of b1, the L_join of b1, the L_meet of b1, the Compl of b1 #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) proof set IR = the Relation of the carrier of R; set L = OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #); take OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #) ; ::_thesis: OrthoLattStr(# the carrier of OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #), the L_join of OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #), the L_meet of OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #), the Compl of OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #) #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) thus OrthoLattStr(# the carrier of OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #), the L_join of OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #), the L_meet of OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #), the Compl of OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #) #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) ; ::_thesis: verum end; end; :: deftheorem Def12 defines CLatAugmentation ROBBINS3:def_12_:_ for R being OrthoLattStr for b2 being OrthoLattRelStr holds ( b2 is CLatAugmentation of R iff OrthoLattStr(# the carrier of b2, the L_join of b2, the L_meet of b2, the Compl of b2 #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) ); registration let L be non empty OrthoLattStr ; cluster -> non empty for CLatAugmentation of L; coherence for b1 being CLatAugmentation of L holds not b1 is empty proof let R be CLatAugmentation of L; ::_thesis: not R is empty OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) by Def12; hence not R is empty ; ::_thesis: verum end; end; registration let L be non empty meet-associative OrthoLattStr ; cluster -> meet-associative for CLatAugmentation of L; coherence for b1 being CLatAugmentation of L holds b1 is meet-associative proof let R be CLatAugmentation of L; ::_thesis: R is meet-associative OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) by Def12; then LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) ; hence R is meet-associative by Th12; ::_thesis: verum end; end; registration let L be non empty join-associative OrthoLattStr ; cluster -> join-associative for CLatAugmentation of L; coherence for b1 being CLatAugmentation of L holds b1 is join-associative proof let R be CLatAugmentation of L; ::_thesis: R is join-associative OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) by Def12; then LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) ; hence R is join-associative by Th11; ::_thesis: verum end; end; registration let L be non empty meet-commutative OrthoLattStr ; cluster -> meet-commutative for CLatAugmentation of L; coherence for b1 being CLatAugmentation of L holds b1 is meet-commutative proof let R be CLatAugmentation of L; ::_thesis: R is meet-commutative OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) by Def12; then LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) ; hence R is meet-commutative by Th10; ::_thesis: verum end; end; registration let L be non empty join-commutative OrthoLattStr ; cluster -> join-commutative for CLatAugmentation of L; coherence for b1 being CLatAugmentation of L holds b1 is join-commutative proof let R be CLatAugmentation of L; ::_thesis: R is join-commutative OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) by Def12; then LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) ; hence R is join-commutative by Th9; ::_thesis: verum end; end; registration let L be non empty meet-absorbing OrthoLattStr ; cluster -> meet-absorbing for CLatAugmentation of L; coherence for b1 being CLatAugmentation of L holds b1 is meet-absorbing proof let R be CLatAugmentation of L; ::_thesis: R is meet-absorbing OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) by Def12; then LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) ; hence R is meet-absorbing by Th14; ::_thesis: verum end; end; registration let L be non empty join-absorbing OrthoLattStr ; cluster -> join-absorbing for CLatAugmentation of L; coherence for b1 being CLatAugmentation of L holds b1 is join-absorbing proof let R be CLatAugmentation of L; ::_thesis: R is join-absorbing OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) by Def12; then LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) ; hence R is join-absorbing by Th13; ::_thesis: verum end; end; registration let L be non empty with_Top OrthoLattStr ; cluster -> with_Top for CLatAugmentation of L; coherence for b1 being CLatAugmentation of L holds b1 is with_Top proof let R be CLatAugmentation of L; ::_thesis: R is with_Top OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) by Def12; then ComplLLattStr(# the carrier of L, the L_join of L, the Compl of L #) = ComplLLattStr(# the carrier of R, the L_join of R, the Compl of R #) ; hence R is with_Top by Th19; ::_thesis: verum end; end; registration let L be Ortholattice; cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like join-Associative meet-Associative meet-Absorbing with_Top naturally_sup-generated naturally_inf-generated for CLatAugmentation of L; existence ex b1 being CLatAugmentation of L st ( b1 is naturally_sup-generated & b1 is naturally_inf-generated & b1 is Lattice-like ) proof set R = LattRel L; set S = OrthoLattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L), the Compl of L #); OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of OrthoLattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L), the Compl of L #), the L_join of OrthoLattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L), the Compl of L #), the L_meet of OrthoLattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L), the Compl of L #), the Compl of OrthoLattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L), the Compl of L #) #) ; then reconsider S = OrthoLattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L), the Compl of L #) as CLatAugmentation of L by Def12; for x, y being Element of S holds ( x <= y iff x |^| y = x ) proof let x, y be Element of S; ::_thesis: ( x <= y iff x |^| y = x ) reconsider x9 = x, y9 = y as Element of L ; hereby ::_thesis: ( x |^| y = x implies x <= y ) assume x <= y ; ::_thesis: x |^| y = x then [x9,y9] in the InternalRel of S by ORDERS_2:def_5; then x9 [= y9 by FILTER_1:31; then x9 |^| y9 = x9 by LATTICES:4; hence x |^| y = x ; ::_thesis: verum end; A1: x9 |^| y9 = x |^| y ; assume x |^| y = x ; ::_thesis: x <= y then x9 [= y9 by A1, LATTICES:4; then [x9,y9] in LattRel L by FILTER_1:31; hence x <= y by ORDERS_2:def_5; ::_thesis: verum end; then A2: S is naturally_inf-generated by Def11; for x, y being Element of S holds ( x <= y iff x |_| y = y ) proof let x, y be Element of S; ::_thesis: ( x <= y iff x |_| y = y ) reconsider x9 = x, y9 = y as Element of L ; hereby ::_thesis: ( x |_| y = y implies x <= y ) assume x <= y ; ::_thesis: x |_| y = y then [x,y] in the InternalRel of S by ORDERS_2:def_5; then x9 [= y9 by FILTER_1:31; then x9 |_| y9 = y9 by LATTICES:def_3; hence x |_| y = y ; ::_thesis: verum end; A3: x9 |_| y9 = x |_| y ; assume x |_| y = y ; ::_thesis: x <= y then x9 [= y9 by A3, LATTICES:def_3; then [x9,y9] in LattRel L by FILTER_1:31; hence x <= y by ORDERS_2:def_5; ::_thesis: verum end; then S is naturally_sup-generated by Def10; hence ex b1 being CLatAugmentation of L st ( b1 is naturally_sup-generated & b1 is naturally_inf-generated & b1 is Lattice-like ) by A2; ::_thesis: verum end; end; registration cluster non empty Lattice-like well-complemented de_Morgan involutive with_Top naturally_sup-generated for OrthoLattRelStr ; existence ex b1 being non empty OrthoLattRelStr st ( b1 is involutive & b1 is with_Top & b1 is de_Morgan & b1 is Lattice-like & b1 is naturally_sup-generated & b1 is well-complemented ) proof take TrivCLRelStr ; ::_thesis: ( TrivCLRelStr is involutive & TrivCLRelStr is with_Top & TrivCLRelStr is de_Morgan & TrivCLRelStr is Lattice-like & TrivCLRelStr is naturally_sup-generated & TrivCLRelStr is well-complemented ) thus ( TrivCLRelStr is involutive & TrivCLRelStr is with_Top & TrivCLRelStr is de_Morgan & TrivCLRelStr is Lattice-like & TrivCLRelStr is naturally_sup-generated & TrivCLRelStr is well-complemented ) ; ::_thesis: verum end; end; theorem Th24: :: ROBBINS3:24 for L being non empty with_suprema with_infima PartialOrdered OrthoRelStr for x, y being Element of L st x <= y holds ( y = x "|_|" y & x = x "|^|" y ) proof let L be non empty with_suprema with_infima PartialOrdered OrthoRelStr ; ::_thesis: for x, y being Element of L st x <= y holds ( y = x "|_|" y & x = x "|^|" y ) let a, b be Element of L; ::_thesis: ( a <= b implies ( b = a "|_|" b & a = a "|^|" b ) ) assume A1: a <= b ; ::_thesis: ( b = a "|_|" b & a = a "|^|" b ) then b = b "|_|" a by YELLOW_0:24; hence ( b = a "|_|" b & a = a "|^|" b ) by A1, LATTICE3:13, YELLOW_0:25; ::_thesis: verum end; definition let L be non empty meet-commutative /\-SemiLattStr ; let a, b be Element of L; :: original: |^| redefine funca |^| b -> M2( the carrier of L); commutativity for a, b being Element of L holds a |^| b = b |^| a by LATTICES:def_6; end; definition let L be non empty join-commutative \/-SemiLattStr ; let a, b be Element of L; :: original: |_| redefine funca |_| b -> M2( the carrier of L); commutativity for a, b being Element of L holds a |_| b = b |_| a by LATTICES:def_4; end; registration cluster non empty meet-commutative meet-absorbing join-absorbing naturally_sup-generated -> non empty reflexive for LattRelStr ; coherence for b1 being non empty LattRelStr st b1 is meet-absorbing & b1 is join-absorbing & b1 is meet-commutative & b1 is naturally_sup-generated holds b1 is reflexive proof let L be non empty LattRelStr ; ::_thesis: ( L is meet-absorbing & L is join-absorbing & L is meet-commutative & L is naturally_sup-generated implies L is reflexive ) assume ( L is meet-absorbing & L is join-absorbing & L is meet-commutative & L is naturally_sup-generated ) ; ::_thesis: L is reflexive then reconsider L9 = L as non empty meet-commutative meet-absorbing join-absorbing naturally_sup-generated LattRelStr ; for x being Element of L9 holds x <= x proof let x be Element of L9; ::_thesis: x <= x x [= x ; hence x <= x by Th22; ::_thesis: verum end; hence L is reflexive by YELLOW_0:def_1; ::_thesis: verum end; end; registration cluster non empty join-associative naturally_sup-generated -> non empty transitive for LattRelStr ; coherence for b1 being non empty LattRelStr st b1 is join-associative & b1 is naturally_sup-generated holds b1 is transitive proof let L be non empty LattRelStr ; ::_thesis: ( L is join-associative & L is naturally_sup-generated implies L is transitive ) assume ( L is join-associative & L is naturally_sup-generated ) ; ::_thesis: L is transitive then reconsider L9 = L as non empty join-associative naturally_sup-generated LattRelStr ; for x, y, z being Element of L9 st x <= y & y <= z holds x <= z proof let x, y, z be Element of L9; ::_thesis: ( x <= y & y <= z implies x <= z ) assume ( x <= y & y <= z ) ; ::_thesis: x <= z then ( x [= y & y [= z ) by Th22; then x [= z by LATTICES:7; hence x <= z by Th22; ::_thesis: verum end; hence L is transitive by YELLOW_0:def_2; ::_thesis: verum end; end; registration cluster non empty join-commutative naturally_sup-generated -> non empty antisymmetric for LattRelStr ; coherence for b1 being non empty LattRelStr st b1 is join-commutative & b1 is naturally_sup-generated holds b1 is antisymmetric proof let L be non empty LattRelStr ; ::_thesis: ( L is join-commutative & L is naturally_sup-generated implies L is antisymmetric ) assume ( L is join-commutative & L is naturally_sup-generated ) ; ::_thesis: L is antisymmetric then reconsider L9 = L as non empty join-commutative naturally_sup-generated LattRelStr ; for x, y being Element of L9 st x <= y & y <= x holds x = y proof let x, y be Element of L9; ::_thesis: ( x <= y & y <= x implies x = y ) assume ( x <= y & y <= x ) ; ::_thesis: x = y then ( x [= y & y [= x ) by Th22; hence x = y by LATTICES:8; ::_thesis: verum end; hence L is antisymmetric by YELLOW_0:def_3; ::_thesis: verum end; end; theorem Th25: :: ROBBINS3:25 for L being non empty Lattice-like with_suprema with_infima naturally_sup-generated OrthoLattRelStr for x, y being Element of L holds x "|_|" y = x |_| y proof let L be non empty Lattice-like with_suprema with_infima naturally_sup-generated OrthoLattRelStr ; ::_thesis: for x, y being Element of L holds x "|_|" y = x |_| y let x, y be Element of L; ::_thesis: x "|_|" y = x |_| y x <= x "|_|" y by YELLOW_0:22; then A1: x [= x "|_|" y by Th22; y <= x "|_|" y by YELLOW_0:22; then A2: y [= x "|_|" y by Th22; x [= x |_| y by LATTICES:5; then A3: x <= x |_| y by Th22; y [= x |_| y by LATTICES:5; then A4: y <= x |_| y by Th22; (x |_| y) "|_|" (x "|_|" y) = ((x |_| y) "|_|" x) "|_|" y by LATTICE3:14 .= (x |_| y) "|_|" y by A3, YELLOW_0:24 .= x |_| y by A4, YELLOW_0:24 ; then x "|_|" y <= x |_| y by YELLOW_0:24; then A5: x "|_|" y [= x |_| y by Th22; (x "|_|" y) |_| (x |_| y) = ((x "|_|" y) |_| x) |_| y by LATTICES:def_5 .= (x "|_|" y) |_| y by A1, LATTICES:def_3 .= x "|_|" y by A2, LATTICES:def_3 ; hence x "|_|" y = x |_| y by A5, LATTICES:def_3; ::_thesis: verum end; theorem Th26: :: ROBBINS3:26 for L being non empty Lattice-like with_suprema with_infima naturally_sup-generated OrthoLattRelStr for x, y being Element of L holds x "|^|" y = x |^| y proof let L be non empty Lattice-like with_suprema with_infima naturally_sup-generated OrthoLattRelStr ; ::_thesis: for x, y being Element of L holds x "|^|" y = x |^| y let x, y be Element of L; ::_thesis: x "|^|" y = x |^| y x "|^|" y <= x by YELLOW_0:23; then A1: x "|^|" y [= x by Th22; x "|^|" y <= y by YELLOW_0:23; then A2: x "|^|" y [= y by Th22; x |^| y [= x by LATTICES:6; then A3: x |^| y <= x by Th22; x |^| y [= y by LATTICES:6; then A4: x |^| y <= y by Th22; (x |^| y) "|^|" (x "|^|" y) = ((x |^| y) "|^|" x) "|^|" y by LATTICE3:16 .= (x |^| y) "|^|" y by A3, YELLOW_0:25 .= x |^| y by A4, YELLOW_0:25 ; then x |^| y <= x "|^|" y by YELLOW_0:25; then A5: x |^| y [= x "|^|" y by Th22; (x "|^|" y) |^| (x |^| y) = ((x "|^|" y) |^| x) |^| y by LATTICES:def_7 .= (x "|^|" y) |^| y by A1, LATTICES:4 .= x "|^|" y by A2, LATTICES:4 ; hence x "|^|" y = x |^| y by A5, LATTICES:4; ::_thesis: verum end; theorem :: ROBBINS3:27 for L being non empty Lattice-like with_suprema with_infima PartialOrdered OrderInvolutive naturally_sup-generated naturally_inf-generated OrthoLattRelStr holds L is de_Morgan proof let L be non empty Lattice-like with_suprema with_infima PartialOrdered OrderInvolutive naturally_sup-generated naturally_inf-generated OrthoLattRelStr ; ::_thesis: L is de_Morgan A1: for x, y being Element of L holds (x `) "|_|" (y `) <= (x "|^|" y) ` proof let a, b be Element of L; ::_thesis: (a `) "|_|" (b `) <= (a "|^|" b) ` set i = a "|^|" b; set s = (a `) "|_|" (b `); a "|^|" b <= a by YELLOW_0:23; then a ` <= (a "|^|" b) ` by Th7; then A2: (a `) "|_|" (b `) <= ((a "|^|" b) `) "|_|" (b `) by WAYBEL_1:2; a "|^|" b <= b by YELLOW_0:23; then b ` <= (a "|^|" b) ` by Th7; then (a "|^|" b) ` = (b `) "|_|" ((a "|^|" b) `) by Th24; hence (a `) "|_|" (b `) <= (a "|^|" b) ` by A2, LATTICE3:13; ::_thesis: verum end; A3: for x, y being Element of L holds (x "|_|" y) ` <= (x `) "|^|" (y `) proof let a, b be Element of L; ::_thesis: (a "|_|" b) ` <= (a `) "|^|" (b `) set i = (a `) "|^|" (b `); set s = a "|_|" b; a <= a "|_|" b by YELLOW_0:22; then (a "|_|" b) ` <= a ` by Th7; then A4: ((a "|_|" b) `) "|^|" (b `) <= (a `) "|^|" (b `) by WAYBEL_1:1; b <= a "|_|" b by YELLOW_0:22; then (a "|_|" b) ` <= b ` by Th7; hence (a "|_|" b) ` <= (a `) "|^|" (b `) by A4, Th24; ::_thesis: verum end; for x, y being Element of L holds ((x `) |_| (y `)) ` = x |^| y proof let a, b be Element of L; ::_thesis: ((a `) |_| (b `)) ` = a |^| b set s = (a `) "|_|" (b `); set i = a "|^|" b; ( (a `) ` = a & (b `) ` = b ) by Th6; then A5: ((a `) "|_|" (b `)) ` <= a "|^|" b by A3; ((a "|^|" b) `) ` <= ((a `) "|_|" (b `)) ` by A1, Th7; then A6: a "|^|" b <= ((a `) "|_|" (b `)) ` by Th6; ( a "|^|" b = a |^| b & (a `) "|_|" (b `) = (a `) |_| (b `) ) by Th25, Th26; hence ((a `) |_| (b `)) ` = a |^| b by A5, A6, ORDERS_2:2; ::_thesis: verum end; hence L is de_Morgan by ROBBINS1:def_23; ::_thesis: verum end; registration let L be Ortholattice; cluster -> involutive for CLatAugmentation of L; coherence for b1 being CLatAugmentation of L holds b1 is involutive proof let R be CLatAugmentation of L; ::_thesis: R is involutive OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) by Def12; hence R is involutive by Th21; ::_thesis: verum end; end; registration let L be Ortholattice; cluster -> de_Morgan for CLatAugmentation of L; coherence for b1 being CLatAugmentation of L holds b1 is de_Morgan proof let R be CLatAugmentation of L; ::_thesis: R is de_Morgan OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) by Def12; hence R is de_Morgan by Th20; ::_thesis: verum end; end; theorem Th28: :: ROBBINS3:28 for L being non empty OrthoLattRelStr st L is involutive & L is with_Top & L is de_Morgan & L is Lattice-like & L is naturally_sup-generated holds ( L is Orthocomplemented & L is PartialOrdered ) proof let L be non empty OrthoLattRelStr ; ::_thesis: ( L is involutive & L is with_Top & L is de_Morgan & L is Lattice-like & L is naturally_sup-generated implies ( L is Orthocomplemented & L is PartialOrdered ) ) assume ( L is involutive & L is with_Top & L is de_Morgan & L is Lattice-like & L is naturally_sup-generated ) ; ::_thesis: ( L is Orthocomplemented & L is PartialOrdered ) then reconsider L9 = L as non empty Lattice-like de_Morgan involutive with_Top naturally_sup-generated OrthoLattRelStr ; reconsider f = the Compl of L9 as Function of L9,L9 ; for x, y being Element of L9 st x <= y holds f . x >= f . y proof let x, y be Element of L9; ::_thesis: ( x <= y implies f . x >= f . y ) assume x <= y ; ::_thesis: f . x >= f . y then x [= y by Th22; then A1: x ` = (x |^| y) ` by LATTICES:4 .= (((x `) |_| (y `)) `) ` by ROBBINS1:def_23 .= (x `) |_| (y `) by Def6 ; ( f . x = x ` & f . y = y ` ) by ROBBINS1:def_3; hence f . x >= f . y by A1, Def10; ::_thesis: verum end; then A2: f is antitone by WAYBEL_9:def_1; A3: for y being Element of L9 holds ( ex_sup_of {y,(f . y)},L9 & ex_inf_of {y,(f . y)},L9 & "\/" ({y,(f . y)},L9) is_maximum_of the carrier of L9 & "/\" ({y,(f . y)},L9) is_minimum_of the carrier of L9 ) proof set xx = "\/" ( the carrier of L9,L9); let y be Element of L9; ::_thesis: ( ex_sup_of {y,(f . y)},L9 & ex_inf_of {y,(f . y)},L9 & "\/" ({y,(f . y)},L9) is_maximum_of the carrier of L9 & "/\" ({y,(f . y)},L9) is_minimum_of the carrier of L9 ) thus ex_sup_of {y,(f . y)},L9 by YELLOW_0:20; ::_thesis: ( ex_inf_of {y,(f . y)},L9 & "\/" ({y,(f . y)},L9) is_maximum_of the carrier of L9 & "/\" ({y,(f . y)},L9) is_minimum_of the carrier of L9 ) thus ex_inf_of {y,(f . y)},L9 by YELLOW_0:21; ::_thesis: ( "\/" ({y,(f . y)},L9) is_maximum_of the carrier of L9 & "/\" ({y,(f . y)},L9) is_minimum_of the carrier of L9 ) set t = y |_| (y `); for b being Element of L9 st b in the carrier of L9 holds b <= y |_| (y `) proof let b be Element of L9; ::_thesis: ( b in the carrier of L9 implies b <= y |_| (y `) ) assume b in the carrier of L9 ; ::_thesis: b <= y |_| (y `) b |_| (y |_| (y `)) = b |_| (b |_| (b `)) by Def7 .= (b |_| b) |_| (b `) by LATTICES:def_5 .= b |_| (b `) .= y |_| (y `) by Def7 ; then b [= y |_| (y `) by LATTICES:def_3; hence b <= y |_| (y `) by Th22; ::_thesis: verum end; then A4: y |_| (y `) is_>=_than the carrier of L9 by LATTICE3:def_9; then L9 is upper-bounded by YELLOW_0:def_5; then A5: ex_sup_of the carrier of L9,L9 by YELLOW_0:43; reconsider t = y |_| (y `) as Element of L9 ; A6: for a being Element of L9 st the carrier of L9 is_<=_than a holds t <= a by LATTICE3:def_9; "\/" ({y,(f . y)},L9) = "\/" ({y,(y `)},L9) by ROBBINS1:def_3 .= y "|_|" (y `) by YELLOW_0:41 .= y |_| (y `) by Th25 .= "\/" ( the carrier of L9,L9) by A4, A5, A6, YELLOW_0:def_9 ; hence "\/" ({y,(f . y)},L9) is_maximum_of the carrier of L9 by A5, WAYBEL_1:def_7; ::_thesis: "/\" ({y,(f . y)},L9) is_minimum_of the carrier of L9 set xx = "/\" ( the carrier of L9,L9); set t = y |^| (y `); A7: for a, b being Element of L9 holds a |^| (a `) = b |^| (b `) proof let a, b be Element of L9; ::_thesis: a |^| (a `) = b |^| (b `) a |^| (a `) = ((a `) |_| ((a `) `)) ` by ROBBINS1:def_23 .= ((b `) |_| ((b `) `)) ` by Def7 .= b |^| (b `) by ROBBINS1:def_23 ; hence a |^| (a `) = b |^| (b `) ; ::_thesis: verum end; for b being Element of L9 st b in the carrier of L9 holds b >= y |^| (y `) proof let b be Element of L9; ::_thesis: ( b in the carrier of L9 implies b >= y |^| (y `) ) assume b in the carrier of L9 ; ::_thesis: b >= y |^| (y `) b |^| (y |^| (y `)) = b |^| (b |^| (b `)) by A7 .= (b |^| b) |^| (b `) by LATTICES:def_7 .= b |^| (b `) .= y |^| (y `) by A7 ; then y |^| (y `) [= b by LATTICES:4; hence b >= y |^| (y `) by Th22; ::_thesis: verum end; then A8: y |^| (y `) is_<=_than the carrier of L9 by LATTICE3:def_8; then L9 is lower-bounded by YELLOW_0:def_4; then A9: ex_inf_of the carrier of L9,L9 by YELLOW_0:42; reconsider t = y |^| (y `) as Element of L9 ; A10: for a being Element of L9 st the carrier of L9 is_>=_than a holds t >= a by LATTICE3:def_8; "/\" ({y,(f . y)},L9) = "/\" ({y,(y `)},L9) by ROBBINS1:def_3 .= y "|^|" (y `) by YELLOW_0:40 .= y |^| (y `) by Th26 .= "/\" ( the carrier of L9,L9) by A8, A9, A10, YELLOW_0:def_10 ; hence "/\" ({y,(f . y)},L9) is_minimum_of the carrier of L9 by A9, WAYBEL_1:def_6; ::_thesis: verum end; for x being Element of L9 holds f . (f . x) = x proof let x be Element of L9; ::_thesis: f . (f . x) = x f . (f . x) = f . (x `) by ROBBINS1:def_3 .= (x `) ` by ROBBINS1:def_3 .= x by Def6 ; hence f . (f . x) = x ; ::_thesis: verum end; then f is V296() by PARTIT_2:def_3; then f is Orderinvolutive by A2, OPOSET_1:def_17; then f OrthoComplement_on L9 by A3, OPOSET_1:def_21; hence ( L is Orthocomplemented & L is PartialOrdered ) by OPOSET_1:def_22; ::_thesis: verum end; theorem :: ROBBINS3:29 for L being Ortholattice for E being naturally_sup-generated CLatAugmentation of L holds E is Orthocomplemented by Th28; registration let L be Ortholattice; cluster naturally_sup-generated -> Orthocomplemented naturally_sup-generated for CLatAugmentation of L; coherence for b1 being naturally_sup-generated CLatAugmentation of L holds b1 is Orthocomplemented by Th28; end; theorem Th30: :: ROBBINS3:30 for L being non empty OrthoLattStr st L is Boolean & L is well-complemented & L is Lattice-like holds L is Ortholattice proof let L be non empty OrthoLattStr ; ::_thesis: ( L is Boolean & L is well-complemented & L is Lattice-like implies L is Ortholattice ) assume ( L is Boolean & L is well-complemented & L is Lattice-like ) ; ::_thesis: L is Ortholattice then reconsider L9 = L as non empty Lattice-like Boolean well-complemented OrthoLattStr ; A1: for x, y being Element of L9 holds x "/\" y = ((x `) "\/" (y `)) ` by ROBBINS1:33; ( ( for x being Element of L9 holds (x `) ` = x ) & ( for x, y being Element of L9 holds x |_| (x `) = y |_| (y `) ) ) by ROBBINS1:3, ROBBINS1:4; hence L is Ortholattice by A1, Def6, Def7, ROBBINS1:def_23; ::_thesis: verum end; registration cluster non empty Lattice-like Boolean well-complemented -> non empty de_Morgan involutive with_Top for OrthoLattStr ; coherence for b1 being non empty OrthoLattStr st b1 is Boolean & b1 is well-complemented & b1 is Lattice-like holds ( b1 is involutive & b1 is with_Top & b1 is de_Morgan ) by Th30; end;