:: ROBBINS1 semantic presentation begin definition attrc1 is strict ; struct ComplStr -> 1-sorted ; aggrComplStr(# carrier, Compl #) -> ComplStr ; sel Compl c1 -> UnOp of the carrier of c1; end; definition attrc1 is strict ; struct ComplLLattStr -> \/-SemiLattStr , ComplStr ; aggrComplLLattStr(# carrier, L_join, Compl #) -> ComplLLattStr ; end; definition attrc1 is strict ; struct ComplULattStr -> /\-SemiLattStr , ComplStr ; aggrComplULattStr(# carrier, L_meet, Compl #) -> ComplULattStr ; end; definition attrc1 is strict ; struct OrthoLattStr -> ComplLLattStr , LattStr ; aggrOrthoLattStr(# carrier, L_join, L_meet, Compl #) -> OrthoLattStr ; end; definition func TrivComplLat -> strict ComplLLattStr equals :: ROBBINS1:def 1 ComplLLattStr(# 1,op2,op1 #); coherence ComplLLattStr(# 1,op2,op1 #) is strict ComplLLattStr ; end; :: deftheorem defines TrivComplLat ROBBINS1:def_1_:_ TrivComplLat = ComplLLattStr(# 1,op2,op1 #); definition func TrivOrtLat -> strict OrthoLattStr equals :: ROBBINS1:def 2 OrthoLattStr(# 1,op2,op2,op1 #); coherence OrthoLattStr(# 1,op2,op2,op1 #) is strict OrthoLattStr ; end; :: deftheorem defines TrivOrtLat ROBBINS1:def_2_:_ TrivOrtLat = OrthoLattStr(# 1,op2,op2,op1 #); registration cluster TrivComplLat -> 1 -element strict ; coherence TrivComplLat is 1 -element proof the carrier of TrivComplLat = {0} by CARD_1:49; hence the carrier of TrivComplLat is 1 -element ; :: according to STRUCT_0:def_19 ::_thesis: verum end; cluster TrivOrtLat -> 1 -element strict ; coherence TrivOrtLat is 1 -element proof the carrier of TrivOrtLat = {0} by CARD_1:49; hence the carrier of TrivOrtLat is 1 -element ; :: according to STRUCT_0:def_19 ::_thesis: verum end; end; registration cluster1 -element strict for OrthoLattStr ; existence ex b1 being OrthoLattStr st ( b1 is strict & b1 is 1 -element ) proof take TrivOrtLat ; ::_thesis: ( TrivOrtLat is strict & TrivOrtLat is 1 -element ) thus ( TrivOrtLat is strict & TrivOrtLat is 1 -element ) ; ::_thesis: verum end; cluster1 -element strict for ComplLLattStr ; existence ex b1 being ComplLLattStr st ( b1 is strict & b1 is 1 -element ) proof take TrivComplLat ; ::_thesis: ( TrivComplLat is strict & TrivComplLat is 1 -element ) thus ( TrivComplLat is strict & TrivComplLat is 1 -element ) ; ::_thesis: verum end; end; registration let L be 1 -element ComplLLattStr ; cluster ComplStr(# the carrier of L, the Compl of L #) -> 1 -element ; coherence ComplStr(# the carrier of L, the Compl of L #) is 1 -element proof thus the carrier of ComplStr(# the carrier of L, the Compl of L #) is 1 -element ; :: according to STRUCT_0:def_19 ::_thesis: verum end; end; registration cluster1 -element strict for ComplStr ; existence ex b1 being ComplStr st ( b1 is strict & b1 is 1 -element ) proof take ComplStr(# the carrier of TrivOrtLat, the Compl of TrivOrtLat #) ; ::_thesis: ( ComplStr(# the carrier of TrivOrtLat, the Compl of TrivOrtLat #) is strict & ComplStr(# the carrier of TrivOrtLat, the Compl of TrivOrtLat #) is 1 -element ) thus ( ComplStr(# the carrier of TrivOrtLat, the Compl of TrivOrtLat #) is strict & ComplStr(# the carrier of TrivOrtLat, the Compl of TrivOrtLat #) is 1 -element ) ; ::_thesis: verum end; end; definition let L be non empty ComplStr ; let x be Element of L; funcx ` -> Element of L equals :: ROBBINS1:def 3 the Compl of L . x; coherence the Compl of L . x is Element of L ; end; :: deftheorem defines ` ROBBINS1:def_3_:_ for L being non empty ComplStr for x being Element of L holds x ` = the Compl of L . x; notation let L be non empty ComplLLattStr ; let x, y be Element of L; synonym x + y for x "\/" y; end; definition let L be non empty ComplLLattStr ; let x, y be Element of L; funcx *' y -> Element of L equals :: ROBBINS1:def 4 ((x `) "\/" (y `)) ` ; coherence ((x `) "\/" (y `)) ` is Element of L ; end; :: deftheorem defines *' ROBBINS1:def_4_:_ for L being non empty ComplLLattStr for x, y being Element of L holds x *' y = ((x `) "\/" (y `)) ` ; definition let L be non empty ComplLLattStr ; attrL is Robbins means :Def5: :: ROBBINS1:def 5 for x, y being Element of L holds (((x + y) `) + ((x + (y `)) `)) ` = x; attrL is Huntington means :Def6: :: ROBBINS1:def 6 for x, y being Element of L holds (((x `) + (y `)) `) + (((x `) + y) `) = x; end; :: deftheorem Def5 defines Robbins ROBBINS1:def_5_:_ for L being non empty ComplLLattStr holds ( L is Robbins iff for x, y being Element of L holds (((x + y) `) + ((x + (y `)) `)) ` = x ); :: deftheorem Def6 defines Huntington ROBBINS1:def_6_:_ for L being non empty ComplLLattStr holds ( L is Huntington iff for x, y being Element of L holds (((x `) + (y `)) `) + (((x `) + y) `) = x ); definition let G be non empty \/-SemiLattStr ; attrG is join-idempotent means :Def7: :: ROBBINS1:def 7 for x being Element of G holds x "\/" x = x; end; :: deftheorem Def7 defines join-idempotent ROBBINS1:def_7_:_ for G being non empty \/-SemiLattStr holds ( G is join-idempotent iff for x being Element of G holds x "\/" x = x ); registration cluster TrivComplLat -> join-commutative join-associative strict Robbins Huntington join-idempotent ; coherence ( TrivComplLat is join-commutative & TrivComplLat is join-associative & TrivComplLat is Robbins & TrivComplLat is Huntington & TrivComplLat is join-idempotent ) proof set L = TrivComplLat ; thus for x, y being Element of TrivComplLat holds x + y = y + x by STRUCT_0:def_10; :: according to LATTICES:def_4 ::_thesis: ( TrivComplLat is join-associative & TrivComplLat is Robbins & TrivComplLat is Huntington & TrivComplLat is join-idempotent ) thus for x, y, z being Element of TrivComplLat holds (x + y) + z = x + (y + z) by STRUCT_0:def_10; :: according to LATTICES:def_5 ::_thesis: ( TrivComplLat is Robbins & TrivComplLat is Huntington & TrivComplLat is join-idempotent ) thus for x, y being Element of TrivComplLat holds (((x + y) `) + ((x + (y `)) `)) ` = x by STRUCT_0:def_10; :: according to ROBBINS1:def_5 ::_thesis: ( TrivComplLat is Huntington & TrivComplLat is join-idempotent ) thus for x, y being Element of TrivComplLat holds (((x `) + (y `)) `) + (((x `) + y) `) = x by STRUCT_0:def_10; :: according to ROBBINS1:def_6 ::_thesis: TrivComplLat is join-idempotent let x be Element of TrivComplLat; :: according to ROBBINS1:def_7 ::_thesis: x "\/" x = x thus x "\/" x = x by STRUCT_0:def_10; ::_thesis: verum end; cluster TrivOrtLat -> join-commutative join-associative strict Robbins Huntington ; coherence ( TrivOrtLat is join-commutative & TrivOrtLat is join-associative & TrivOrtLat is Huntington & TrivOrtLat is Robbins ) proof set L = TrivOrtLat ; thus for x, y being Element of TrivOrtLat holds x + y = y + x by STRUCT_0:def_10; :: according to LATTICES:def_4 ::_thesis: ( TrivOrtLat is join-associative & TrivOrtLat is Huntington & TrivOrtLat is Robbins ) thus for x, y, z being Element of TrivOrtLat holds (x + y) + z = x + (y + z) by STRUCT_0:def_10; :: according to LATTICES:def_5 ::_thesis: ( TrivOrtLat is Huntington & TrivOrtLat is Robbins ) thus for x, y being Element of TrivOrtLat holds (((x `) + (y `)) `) + (((x `) + y) `) = x by STRUCT_0:def_10; :: according to ROBBINS1:def_6 ::_thesis: TrivOrtLat is Robbins let x, y be Element of TrivOrtLat; :: according to ROBBINS1:def_5 ::_thesis: (((x + y) `) + ((x + (y `)) `)) ` = x thus (((x + y) `) + ((x + (y `)) `)) ` = x by STRUCT_0:def_10; ::_thesis: verum end; end; registration cluster TrivOrtLat -> meet-commutative meet-associative meet-absorbing join-absorbing strict ; coherence ( TrivOrtLat is meet-commutative & TrivOrtLat is meet-associative & TrivOrtLat is meet-absorbing & TrivOrtLat is join-absorbing ) proof set L = TrivOrtLat ; thus for x, y being Element of TrivOrtLat holds x "/\" y = y "/\" x by STRUCT_0:def_10; :: according to LATTICES:def_6 ::_thesis: ( TrivOrtLat is meet-associative & TrivOrtLat is meet-absorbing & TrivOrtLat is join-absorbing ) thus for x, y, z being Element of TrivOrtLat holds (x "/\" y) "/\" z = x "/\" (y "/\" z) by STRUCT_0:def_10; :: according to LATTICES:def_7 ::_thesis: ( TrivOrtLat is meet-absorbing & TrivOrtLat is join-absorbing ) thus for x, y being Element of TrivOrtLat holds (x "/\" y) "\/" y = y by STRUCT_0:def_10; :: according to LATTICES:def_8 ::_thesis: TrivOrtLat is join-absorbing let x, y be Element of TrivOrtLat; :: according to LATTICES:def_9 ::_thesis: x "/\" (x + y) = x thus x "/\" (x "\/" y) = x by STRUCT_0:def_10; ::_thesis: verum end; end; registration cluster non empty join-commutative join-associative strict Robbins Huntington join-idempotent for ComplLLattStr ; existence ex b1 being non empty ComplLLattStr st ( b1 is strict & b1 is join-associative & b1 is join-commutative & b1 is Robbins & b1 is join-idempotent & b1 is Huntington ) proof take TrivComplLat ; ::_thesis: ( TrivComplLat is strict & TrivComplLat is join-associative & TrivComplLat is join-commutative & TrivComplLat is Robbins & TrivComplLat is join-idempotent & TrivComplLat is Huntington ) thus ( TrivComplLat is strict & TrivComplLat is join-associative & TrivComplLat is join-commutative & TrivComplLat is Robbins & TrivComplLat is join-idempotent & TrivComplLat is Huntington ) ; ::_thesis: verum end; end; registration cluster non empty Lattice-like strict Robbins Huntington for OrthoLattStr ; existence ex b1 being non empty OrthoLattStr st ( b1 is strict & b1 is Lattice-like & b1 is Robbins & b1 is Huntington ) proof take TrivOrtLat ; ::_thesis: ( TrivOrtLat is strict & TrivOrtLat is Lattice-like & TrivOrtLat is Robbins & TrivOrtLat is Huntington ) thus ( TrivOrtLat is strict & TrivOrtLat is Lattice-like & TrivOrtLat is Robbins & TrivOrtLat is Huntington ) ; ::_thesis: verum end; end; definition let L be non empty join-commutative ComplLLattStr ; let x, y be Element of L; :: original: + redefine funcx + y -> M2( the carrier of L); commutativity for x, y being Element of L holds x + y = y + x by LATTICES:def_4; end; theorem Th1: :: ROBBINS1:1 for L being non empty join-commutative join-associative Huntington ComplLLattStr for a, b being Element of L holds (a *' b) + (a *' (b `)) = a by Def6; theorem Th2: :: ROBBINS1:2 for L being non empty join-commutative join-associative Huntington ComplLLattStr for a being Element of L holds a + (a `) = (a `) + ((a `) `) proof let L be non empty join-commutative join-associative Huntington ComplLLattStr ; ::_thesis: for a being Element of L holds a + (a `) = (a `) + ((a `) `) let a be Element of L; ::_thesis: a + (a `) = (a `) + ((a `) `) set y = a ` ; set z = ((a `) `) ` ; ( a = (((a `) + (((a `) `) `)) `) + (((a `) + ((a `) `)) `) & a ` = ((((a `) `) + (((a `) `) `)) `) + ((((a `) `) + ((a `) `)) `) ) by Def6; then a + (a `) = (((((a `) + (((a `) `) `)) `) + (((a `) + ((a `) `)) `)) + ((((a `) `) + ((a `) `)) `)) + ((((a `) `) + (((a `) `) `)) `) by LATTICES:def_5 .= ((((((a `) `) + ((a `) `)) `) + (((a `) + ((a `) `)) `)) + (((a `) + (((a `) `) `)) `)) + ((((a `) `) + (((a `) `) `)) `) by LATTICES:def_5 .= (((((a `) `) + (a `)) `) + ((((a `) `) + ((a `) `)) `)) + ((((a `) + (((a `) `) `)) `) + ((((a `) `) + (((a `) `) `)) `)) by LATTICES:def_5 .= (a `) + ((((a `) + (((a `) `) `)) `) + ((((a `) `) + (((a `) `) `)) `)) by Def6 .= (a `) + ((a `) `) by Def6 ; hence a + (a `) = (a `) + ((a `) `) ; ::_thesis: verum end; theorem Th3: :: ROBBINS1:3 for L being non empty join-commutative join-associative Huntington ComplLLattStr for x being Element of L holds (x `) ` = x proof let L be non empty join-commutative join-associative Huntington ComplLLattStr ; ::_thesis: for x being Element of L holds (x `) ` = x let x be Element of L; ::_thesis: (x `) ` = x set y = x ` ; ( (((((x `) `) `) + ((x `) `)) `) + (((((x `) `) `) + (x `)) `) = (x `) ` & (((x `) + (((x `) `) `)) `) + (((x `) + ((x `) `)) `) = x ) by Def6; hence (x `) ` = x by Th2; ::_thesis: verum end; theorem Th4: :: ROBBINS1:4 for L being non empty join-commutative join-associative Huntington ComplLLattStr for a, b being Element of L holds a + (a `) = b + (b `) proof let L be non empty join-commutative join-associative Huntington ComplLLattStr ; ::_thesis: for a, b being Element of L holds a + (a `) = b + (b `) let a, b be Element of L; ::_thesis: a + (a `) = b + (b `) thus a + (a `) = ((((a `) + ((b `) `)) `) + (((a `) + (b `)) `)) + (a `) by Def6 .= ((((a `) + ((b `) `)) `) + (((a `) + (b `)) `)) + (((((a `) `) + ((b `) `)) `) + ((((a `) `) + (b `)) `)) by Def6 .= ((((a `) `) + (b `)) `) + (((((a `) `) + ((b `) `)) `) + ((((a `) + ((b `) `)) `) + (((a `) + (b `)) `))) by LATTICES:def_5 .= ((((a `) `) + (b `)) `) + ((((a `) + (b `)) `) + ((((a `) + ((b `) `)) `) + ((((a `) `) + ((b `) `)) `))) by LATTICES:def_5 .= (((((a `) `) + (b `)) `) + (((a `) + (b `)) `)) + ((((a `) + ((b `) `)) `) + ((((a `) `) + ((b `) `)) `)) by LATTICES:def_5 .= b + (((((a `) `) + ((b `) `)) `) + (((a `) + ((b `) `)) `)) by Def6 .= b + (b `) by Def6 ; ::_thesis: verum end; theorem Th5: :: ROBBINS1:5 for L being non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr ex c being Element of L st for a being Element of L holds ( c + a = c & a + (a `) = c ) proof let L be non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr ; ::_thesis: ex c being Element of L st for a being Element of L holds ( c + a = c & a + (a `) = c ) set b = the Element of L; take c = ( the Element of L `) + the Element of L; ::_thesis: for a being Element of L holds ( c + a = c & a + (a `) = c ) let a be Element of L; ::_thesis: ( c + a = c & a + (a `) = c ) thus c + a = ((a `) + a) + a by Th4 .= (a `) + (a + a) by LATTICES:def_5 .= (a `) + a by Def7 .= c by Th4 ; ::_thesis: a + (a `) = c thus a + (a `) = c by Th4; ::_thesis: verum end; theorem Th6: :: ROBBINS1:6 for L being non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr holds L is upper-bounded proof let L be non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr ; ::_thesis: L is upper-bounded consider c being Element of L such that A1: for a being Element of L holds ( c + a = c & a + (a `) = c ) by Th5; for a being Element of L holds ( a + c = c & a + (a `) = c ) by A1; hence L is upper-bounded by A1, LATTICES:def_14; ::_thesis: verum end; registration cluster non empty join-commutative join-associative Huntington join-idempotent -> non empty upper-bounded for ComplLLattStr ; coherence for b1 being non empty ComplLLattStr st b1 is join-commutative & b1 is join-associative & b1 is join-idempotent & b1 is Huntington holds b1 is upper-bounded by Th6; end; definition let L be non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr ; redefine func Top L means :Def8: :: ROBBINS1:def 8 ex a being Element of L st it = a + (a `); compatibility for b1 being M2( the carrier of L) holds ( b1 = Top L iff ex a being Element of L st b1 = a + (a `) ) proof let IT be Element of L; ::_thesis: ( IT = Top L iff ex a being Element of L st IT = a + (a `) ) hereby ::_thesis: ( ex a being Element of L st IT = a + (a `) implies IT = Top L ) set a = the Element of L; assume A1: IT = Top L ; ::_thesis: ex a being Element of L st IT = a + (a `) take a = the Element of L; ::_thesis: IT = a + (a `) for b being Element of L holds ( (a + (a `)) + b = a + (a `) & b + (a + (a `)) = a + (a `) ) proof let b be Element of L; ::_thesis: ( (a + (a `)) + b = a + (a `) & b + (a + (a `)) = a + (a `) ) (a + (a `)) + b = (b + (b `)) + b by Th4 .= (b `) + (b + b) by LATTICES:def_5 .= (b `) + b by Def7 .= (a `) + a by Th4 ; hence ( (a + (a `)) + b = a + (a `) & b + (a + (a `)) = a + (a `) ) ; ::_thesis: verum end; hence IT = a + (a `) by A1, LATTICES:def_17; ::_thesis: verum end; given a being Element of L such that A2: IT = a + (a `) ; ::_thesis: IT = Top L A3: for b being Element of L holds (a + (a `)) + b = a + (a `) proof let b be Element of L; ::_thesis: (a + (a `)) + b = a + (a `) (a + (a `)) + b = (b + (b `)) + b by Th4 .= (b `) + (b + b) by LATTICES:def_5 .= (b `) + b by Def7 .= (a `) + a by Th4 ; hence (a + (a `)) + b = a + (a `) ; ::_thesis: verum end; then for b being Element of L holds b + (a + (a `)) = a + (a `) ; hence IT = Top L by A2, A3, LATTICES:def_17; ::_thesis: verum end; end; :: deftheorem Def8 defines Top ROBBINS1:def_8_:_ for L being non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr for b2 being M2( the carrier of b1) holds ( b2 = Top L iff ex a being Element of L st b2 = a + (a `) ); theorem Th7: :: ROBBINS1:7 for L being non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr ex c being Element of L st for a being Element of L holds ( c *' a = c & (a + (a `)) ` = c ) proof let L be non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr ; ::_thesis: ex c being Element of L st for a being Element of L holds ( c *' a = c & (a + (a `)) ` = c ) set b = the Element of L; take c = (( the Element of L `) + the Element of L) ` ; ::_thesis: for a being Element of L holds ( c *' a = c & (a + (a `)) ` = c ) let a be Element of L; ::_thesis: ( c *' a = c & (a + (a `)) ` = c ) thus c *' a = ((( the Element of L `) + the Element of L) + (a `)) ` by Th3 .= (((a `) + a) + (a `)) ` by Th4 .= (a + ((a `) + (a `))) ` by LATTICES:def_5 .= (a + (a `)) ` by Def7 .= c by Th4 ; ::_thesis: (a + (a `)) ` = c thus (a + (a `)) ` = c by Th4; ::_thesis: verum end; definition let L be non empty join-commutative join-associative ComplLLattStr ; let x, y be Element of L; :: original: *' redefine funcx *' y -> Element of L; commutativity 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 thus a *' b = ((a `) + (b `)) ` .= b *' a ; ::_thesis: verum end; end; definition let L be non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr ; func Bot L -> Element of L means :Def9: :: ROBBINS1:def 9 for a being Element of L holds it *' a = it; existence ex b1 being Element of L st for a being Element of L holds b1 *' a = b1 proof ex c being Element of L st for a being Element of L holds ( c *' a = c & (a + (a `)) ` = c ) by Th7; hence ex b1 being Element of L st for a being Element of L holds b1 *' a = b1 ; ::_thesis: verum end; uniqueness for b1, b2 being Element of L st ( for a being Element of L holds b1 *' a = b1 ) & ( for a being Element of L holds b2 *' a = b2 ) holds b1 = b2 proof let c1, c2 be Element of L; ::_thesis: ( ( for a being Element of L holds c1 *' a = c1 ) & ( for a being Element of L holds c2 *' a = c2 ) implies c1 = c2 ) assume that A1: for a being Element of L holds c1 *' a = c1 and A2: for a being Element of L holds c2 *' a = c2 ; ::_thesis: c1 = c2 thus c1 = c2 *' c1 by A1 .= c2 by A2 ; ::_thesis: verum end; end; :: deftheorem Def9 defines Bot ROBBINS1:def_9_:_ for L being non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr for b2 being Element of L holds ( b2 = Bot L iff for a being Element of L holds b2 *' a = b2 ); theorem Th8: :: ROBBINS1:8 for L being non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr for a being Element of L holds Bot L = (a + (a `)) ` proof let L be non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr ; ::_thesis: for a being Element of L holds Bot L = (a + (a `)) ` let a be Element of L; ::_thesis: Bot L = (a + (a `)) ` for b being Element of L holds ((a + (a `)) `) *' b = (a + (a `)) ` proof let b be Element of L; ::_thesis: ((a + (a `)) `) *' b = (a + (a `)) ` ((a + (a `)) `) *' b = ((((b + (b `)) `) `) + (b `)) ` by Th4 .= ((b + (b `)) + (b `)) ` by Th3 .= (b + ((b `) + (b `))) ` by LATTICES:def_5 .= (b + (b `)) ` by Def7 .= ((a `) + a) ` by Th4 ; hence ((a + (a `)) `) *' b = (a + (a `)) ` ; ::_thesis: verum end; hence Bot L = (a + (a `)) ` by Def9; ::_thesis: verum end; theorem Th9: :: ROBBINS1:9 for L being non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr holds ( (Top L) ` = Bot L & Top L = (Bot L) ` ) proof let L be non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr ; ::_thesis: ( (Top L) ` = Bot L & Top L = (Bot L) ` ) set a = the Element of L; thus (Top L) ` = ( the Element of L + ( the Element of L `)) ` by Def8 .= Bot L by Th8 ; ::_thesis: Top L = (Bot L) ` hence Top L = (Bot L) ` by Th3; ::_thesis: verum end; theorem Th10: :: ROBBINS1:10 for L being non empty join-commutative join-associative Huntington ComplLLattStr for a, b being Element of L st a ` = b ` holds a = b proof let L be non empty join-commutative join-associative Huntington ComplLLattStr ; ::_thesis: for a, b being Element of L st a ` = b ` holds a = b let a, b be Element of L; ::_thesis: ( a ` = b ` implies a = b ) assume A1: a ` = b ` ; ::_thesis: a = b thus a = (a `) ` by Th3 .= b by A1, Th3 ; ::_thesis: verum end; theorem Th11: :: ROBBINS1:11 for L being non empty join-commutative join-associative Huntington ComplLLattStr for a, b being Element of L holds a + ((b + (b `)) `) = a proof let L be non empty join-commutative join-associative Huntington ComplLLattStr ; ::_thesis: for a, b being Element of L holds a + ((b + (b `)) `) = a let a, b be Element of L; ::_thesis: a + ((b + (b `)) `) = a set O = b + (b `); A1: ((b + (b `)) `) ` = b + (b `) by Th3; A2: (b + (b `)) ` = (((((b + (b `)) `) `) + (((b + (b `)) `) `)) `) + (((((b + (b `)) `) `) + ((b + (b `)) `)) `) by Def6 .= (((b + (b `)) + (b + (b `))) `) + ((b + (b `)) `) by A1, Th4 ; A3: b + (b `) = (a `) + a by Th4; b + (b `) = (b + (b `)) + ((b + (b `)) `) by Th4 .= ((b + (b `)) + ((b + (b `)) `)) + (((b + (b `)) + (b + (b `))) `) by A2, LATTICES:def_5 .= (b + (b `)) + (((b + (b `)) + (b + (b `))) `) by Th4 ; then A4: (b + (b `)) + (b + (b `)) = ((b + (b `)) + (b + (b `))) + (((b + (b `)) + (b + (b `))) `) by LATTICES:def_5 .= b + (b `) by Th4 ; hence a + ((b + (b `)) `) = ((((a `) + (a `)) `) + (((a `) + a) `)) + ((((a `) + a) `) + (((a `) + a) `)) by A2, A3, Def6 .= (((a `) + (a `)) `) + ((((a `) + a) `) + (((a `) + a) `)) by A2, A4, A3, LATTICES:def_5 .= a by A2, A4, A3, Def6 ; ::_thesis: verum end; theorem Th12: :: ROBBINS1:12 for L being non empty join-commutative join-associative Huntington ComplLLattStr for a being Element of L holds a + a = a proof let L be non empty join-commutative join-associative Huntington ComplLLattStr ; ::_thesis: for a being Element of L holds a + a = a let a be Element of L; ::_thesis: a + a = a A1: (a + a) ` = ((((a `) `) + (a `)) `) + ((a + a) `) by Th11 .= ((((a `) `) + (a `)) `) + ((((a `) `) + a) `) by Th3 .= a ` by Def6 ; thus a + a = ((a + a) `) ` by Th3 .= a by A1, Th3 ; ::_thesis: verum end; registration cluster non empty join-commutative join-associative Huntington -> non empty join-idempotent for ComplLLattStr ; coherence for b1 being non empty ComplLLattStr st b1 is join-commutative & b1 is join-associative & b1 is Huntington holds b1 is join-idempotent proof let L be non empty ComplLLattStr ; ::_thesis: ( L is join-commutative & L is join-associative & L is Huntington implies L is join-idempotent ) assume ( L is join-commutative & L is join-associative & L is Huntington ) ; ::_thesis: L is join-idempotent then for a being Element of L holds a + a = a by Th12; hence L is join-idempotent by Def7; ::_thesis: verum end; end; theorem Th13: :: ROBBINS1:13 for L being non empty join-commutative join-associative Huntington ComplLLattStr for a being Element of L holds a + (Bot L) = a proof let L be non empty join-commutative join-associative Huntington ComplLLattStr ; ::_thesis: for a being Element of L holds a + (Bot L) = a let a be Element of L; ::_thesis: a + (Bot L) = a a = (((a `) + (a `)) `) + (((a `) + a) `) by Def6 .= ((a `) `) + (((a `) + a) `) by Def7 .= a + (((a `) + a) `) by Th3 ; hence a + (Bot L) = a by Th8; ::_thesis: verum end; theorem :: ROBBINS1:14 for L being non empty join-commutative join-associative Huntington ComplLLattStr for a being Element of L holds a *' (Top L) = a proof let L be non empty join-commutative join-associative Huntington ComplLLattStr ; ::_thesis: for a being Element of L holds a *' (Top L) = a let a be Element of L; ::_thesis: a *' (Top L) = a a *' (Top L) = ((a `) + (Bot L)) ` by Th9 .= (a `) ` by Th13 .= a by Th3 ; hence a *' (Top L) = a ; ::_thesis: verum end; theorem Th15: :: ROBBINS1:15 for L being non empty join-commutative join-associative Huntington ComplLLattStr for a being Element of L holds a *' (a `) = Bot L proof let L be non empty join-commutative join-associative Huntington ComplLLattStr ; ::_thesis: for a being Element of L holds a *' (a `) = Bot L let a be Element of L; ::_thesis: a *' (a `) = Bot L thus a *' (a `) = (Top L) ` by Def8 .= Bot L by Th9 ; ::_thesis: verum end; theorem Th16: :: ROBBINS1:16 for L being non empty join-commutative join-associative Huntington ComplLLattStr for a, b, c being Element of L holds a *' (b *' c) = (a *' b) *' c proof let L be non empty join-commutative join-associative Huntington ComplLLattStr ; ::_thesis: for a, b, c being Element of L holds a *' (b *' c) = (a *' b) *' c let a, b, c be Element of L; ::_thesis: a *' (b *' c) = (a *' b) *' c thus (a *' b) *' c = (((a `) + (b `)) + (c `)) ` by Th3 .= ((a `) + ((b `) + (c `))) ` by LATTICES:def_5 .= a *' (b *' c) by Th3 ; ::_thesis: verum end; theorem Th17: :: ROBBINS1:17 for L being non empty join-commutative join-associative Huntington ComplLLattStr for a, b being Element of L holds a + b = ((a `) *' (b `)) ` proof let L be non empty join-commutative join-associative Huntington ComplLLattStr ; ::_thesis: for a, b being Element of L holds a + b = ((a `) *' (b `)) ` let a, b be Element of L; ::_thesis: a + b = ((a `) *' (b `)) ` (a `) *' (b `) = (((a `) `) + b) ` by Th3 .= (a + b) ` by Th3 ; hence a + b = ((a `) *' (b `)) ` by Th3; ::_thesis: verum end; theorem :: ROBBINS1:18 for L being non empty join-commutative join-associative Huntington ComplLLattStr for a being Element of L holds a *' a = a proof let L be non empty join-commutative join-associative Huntington ComplLLattStr ; ::_thesis: for a being Element of L holds a *' a = a let a be Element of L; ::_thesis: a *' a = a thus a *' a = (a `) ` by Def7 .= a by Th3 ; ::_thesis: verum end; theorem :: ROBBINS1:19 for L being non empty join-commutative join-associative Huntington ComplLLattStr for a being Element of L holds a + (Top L) = Top L proof let L be non empty join-commutative join-associative Huntington ComplLLattStr ; ::_thesis: for a being Element of L holds a + (Top L) = Top L let a be Element of L; ::_thesis: a + (Top L) = Top L thus a + (Top L) = a + (a + (a `)) by Def8 .= (a + a) + (a `) by LATTICES:def_5 .= a + (a `) by Def7 .= Top L by Def8 ; ::_thesis: verum end; theorem Th20: :: ROBBINS1:20 for L being non empty join-commutative join-associative Huntington ComplLLattStr for a, b being Element of L holds a + (a *' b) = a proof let L be non empty join-commutative join-associative Huntington ComplLLattStr ; ::_thesis: for a, b being Element of L holds a + (a *' b) = a let a, b be Element of L; ::_thesis: a + (a *' b) = a thus a + (a *' b) = (a *' b) + ((a *' b) + (a *' (b `))) by Def6 .= ((a *' b) + (a *' b)) + (a *' (b `)) by LATTICES:def_5 .= (a *' b) + (a *' (b `)) by Def7 .= a by Def6 ; ::_thesis: verum end; theorem Th21: :: ROBBINS1:21 for L being non empty join-commutative join-associative Huntington ComplLLattStr for a, b being Element of L holds a *' (a + b) = a proof let L be non empty join-commutative join-associative Huntington ComplLLattStr ; ::_thesis: for a, b being Element of L holds a *' (a + b) = a let a, b be Element of L; ::_thesis: a *' (a + b) = a thus a *' (a + b) = ((a `) + ((((a `) *' (b `)) `) `)) ` by Th17 .= ((a `) + ((a `) *' (b `))) ` by Th3 .= (a `) ` by Th20 .= a by Th3 ; ::_thesis: verum end; theorem Th22: :: ROBBINS1:22 for L being non empty join-commutative join-associative Huntington ComplLLattStr for a, b being Element of L st (a `) + b = Top L & (b `) + a = Top L holds a = b proof let L be non empty join-commutative join-associative Huntington ComplLLattStr ; ::_thesis: for a, b being Element of L st (a `) + b = Top L & (b `) + a = Top L holds a = b let a, b be Element of L; ::_thesis: ( (a `) + b = Top L & (b `) + a = Top L implies a = b ) assume A1: ( (a `) + b = Top L & (b `) + a = Top L ) ; ::_thesis: a = b thus a = (((a `) + (b `)) `) + (((a `) + b) `) by Def6 .= b by A1, Def6 ; ::_thesis: verum end; theorem Th23: :: ROBBINS1:23 for L being non empty join-commutative join-associative Huntington ComplLLattStr for a, b being Element of L st a + b = Top L & a *' b = Bot L holds a ` = b proof let L be non empty join-commutative join-associative Huntington ComplLLattStr ; ::_thesis: for a, b being Element of L st a + b = Top L & a *' b = Bot L holds a ` = b let a, b be Element of L; ::_thesis: ( a + b = Top L & a *' b = Bot L implies a ` = b ) assume a + b = Top L ; ::_thesis: ( not a *' b = Bot L or a ` = b ) then A1: ((a `) `) + b = Top L by Th3; assume A2: a *' b = Bot L ; ::_thesis: a ` = b (b `) + (a `) = (((a `) + (b `)) `) ` by Th3 .= Top L by A2, Th9 ; hence a ` = b by A1, Th22; ::_thesis: verum end; theorem Th24: :: ROBBINS1:24 for L being non empty join-commutative join-associative Huntington ComplLLattStr for a, b, c being Element of L holds ((((((((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c)) + ((a *' (b `)) *' (c `))) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)) = Top L proof let L be non empty join-commutative join-associative Huntington ComplLLattStr ; ::_thesis: for a, b, c being Element of L holds ((((((((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c)) + ((a *' (b `)) *' (c `))) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)) = Top L let a, b, c be Element of L; ::_thesis: ((((((((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c)) + ((a *' (b `)) *' (c `))) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)) = Top L set A = (a *' b) *' c; set B = (a *' b) *' (c `); set C = (a *' (b `)) *' c; set D = (a *' (b `)) *' (c `); set E = ((a `) *' b) *' c; set F = ((a `) *' b) *' (c `); set G = ((a `) *' (b `)) *' c; set H = ((a `) *' (b `)) *' (c `); ((((((((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c)) + ((a *' (b `)) *' (c `))) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)) = ((((((a *' b) + ((a *' (b `)) *' c)) + ((a *' (b `)) *' (c `))) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)) by Def6 .= (((((a *' b) + (((a *' (b `)) *' c) + ((a *' (b `)) *' (c `)))) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)) by LATTICES:def_5 .= (((((a *' b) + (a *' (b `))) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)) by Def6 .= ((((a *' b) + (a *' (b `))) + ((((a `) *' b) *' c) + (((a `) *' b) *' (c `)))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)) by LATTICES:def_5 .= ((((a *' b) + (a *' (b `))) + ((a `) *' b)) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)) by Def6 .= (((a *' b) + (a *' (b `))) + ((a `) *' b)) + ((((a `) *' (b `)) *' c) + (((a `) *' (b `)) *' (c `))) by LATTICES:def_5 .= (((a *' b) + (a *' (b `))) + ((a `) *' b)) + ((a `) *' (b `)) by Def6 .= (a + ((a `) *' b)) + ((a `) *' (b `)) by Def6 .= a + (((a `) *' b) + ((a `) *' (b `))) by LATTICES:def_5 .= a + (a `) by Def6 ; hence ((((((((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c)) + ((a *' (b `)) *' (c `))) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)) = Top L by Def8; ::_thesis: verum end; theorem Th25: :: ROBBINS1:25 for L being non empty join-commutative join-associative Huntington ComplLLattStr for a, b, c being Element of L holds ( (a *' c) *' (b *' (c `)) = Bot L & ((a *' b) *' c) *' (((a `) *' b) *' c) = Bot L & ((a *' (b `)) *' c) *' (((a `) *' b) *' c) = Bot L & ((a *' b) *' c) *' (((a `) *' (b `)) *' c) = Bot L & ((a *' b) *' (c `)) *' (((a `) *' (b `)) *' (c `)) = Bot L ) proof let L be non empty join-commutative join-associative Huntington ComplLLattStr ; ::_thesis: for a, b, c being Element of L holds ( (a *' c) *' (b *' (c `)) = Bot L & ((a *' b) *' c) *' (((a `) *' b) *' c) = Bot L & ((a *' (b `)) *' c) *' (((a `) *' b) *' c) = Bot L & ((a *' b) *' c) *' (((a `) *' (b `)) *' c) = Bot L & ((a *' b) *' (c `)) *' (((a `) *' (b `)) *' (c `)) = Bot L ) let a, b, c be Element of L; ::_thesis: ( (a *' c) *' (b *' (c `)) = Bot L & ((a *' b) *' c) *' (((a `) *' b) *' c) = Bot L & ((a *' (b `)) *' c) *' (((a `) *' b) *' c) = Bot L & ((a *' b) *' c) *' (((a `) *' (b `)) *' c) = Bot L & ((a *' b) *' (c `)) *' (((a `) *' (b `)) *' (c `)) = Bot L ) A1: for a, b, c being Element of L holds (a *' c) *' (b *' (c `)) = Bot L proof let a, b, c be Element of L; ::_thesis: (a *' c) *' (b *' (c `)) = Bot L thus (a *' c) *' (b *' (c `)) = ((a *' c) *' (c `)) *' b by Th16 .= (a *' (c *' (c `))) *' b by Th16 .= (a *' (Bot L)) *' b by Th15 .= (Bot L) *' b by Def9 .= Bot L by Def9 ; ::_thesis: verum end; hence (a *' c) *' (b *' (c `)) = Bot L ; ::_thesis: ( ((a *' b) *' c) *' (((a `) *' b) *' c) = Bot L & ((a *' (b `)) *' c) *' (((a `) *' b) *' c) = Bot L & ((a *' b) *' c) *' (((a `) *' (b `)) *' c) = Bot L & ((a *' b) *' (c `)) *' (((a `) *' (b `)) *' (c `)) = Bot L ) thus ((a *' b) *' c) *' (((a `) *' b) *' c) = (a *' (b *' c)) *' (((a `) *' b) *' c) by Th16 .= (((b *' c) *' a) *' ((a `) *' b)) *' c by Th16 .= ((((b *' c) *' a) *' (a `)) *' b) *' c by Th16 .= (((b *' c) *' (a *' (a `))) *' b) *' c by Th16 .= ((b *' c) *' (a *' (a `))) *' (b *' c) by Th16 .= ((b *' c) *' (Bot L)) *' (b *' c) by Th15 .= (Bot L) *' (b *' c) by Def9 .= Bot L by Def9 ; ::_thesis: ( ((a *' (b `)) *' c) *' (((a `) *' b) *' c) = Bot L & ((a *' b) *' c) *' (((a `) *' (b `)) *' c) = Bot L & ((a *' b) *' (c `)) *' (((a `) *' (b `)) *' (c `)) = Bot L ) thus ((a *' (b `)) *' c) *' (((a `) *' b) *' c) = (a *' ((b `) *' c)) *' (((a `) *' b) *' c) by Th16 .= (((b `) *' c) *' a) *' ((a `) *' (b *' c)) by Th16 .= ((((b `) *' c) *' a) *' (a `)) *' (b *' c) by Th16 .= (((b `) *' c) *' (a *' (a `))) *' (b *' c) by Th16 .= (((b `) *' c) *' (Bot L)) *' (b *' c) by Th15 .= (Bot L) *' (b *' c) by Def9 .= Bot L by Def9 ; ::_thesis: ( ((a *' b) *' c) *' (((a `) *' (b `)) *' c) = Bot L & ((a *' b) *' (c `)) *' (((a `) *' (b `)) *' (c `)) = Bot L ) thus ((a *' b) *' c) *' (((a `) *' (b `)) *' c) = (a *' (b *' c)) *' (((a `) *' (b `)) *' c) by Th16 .= (a *' (b *' c)) *' ((a `) *' ((b `) *' c)) by Th16 .= Bot L by A1 ; ::_thesis: ((a *' b) *' (c `)) *' (((a `) *' (b `)) *' (c `)) = Bot L thus ((a *' b) *' (c `)) *' (((a `) *' (b `)) *' (c `)) = (a *' (b *' (c `))) *' (((a `) *' (b `)) *' (c `)) by Th16 .= (a *' (b *' (c `))) *' ((a `) *' ((b `) *' (c `))) by Th16 .= Bot L by A1 ; ::_thesis: verum end; theorem Th26: :: ROBBINS1:26 for L being non empty join-commutative join-associative Huntington ComplLLattStr for a, b, c being Element of L holds (a *' b) + (a *' c) = (((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c) proof let L be non empty join-commutative join-associative Huntington ComplLLattStr ; ::_thesis: for a, b, c being Element of L holds (a *' b) + (a *' c) = (((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c) let a, b, c be Element of L; ::_thesis: (a *' b) + (a *' c) = (((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c) set A = (a *' b) *' c; a *' c = ((a *' c) *' b) + ((a *' c) *' (b `)) by Def6 .= ((a *' b) *' c) + ((a *' c) *' (b `)) by Th16 .= ((a *' b) *' c) + ((a *' (b `)) *' c) by Th16 ; hence (a *' b) + (a *' c) = (((a *' b) *' c) + ((a *' b) *' (c `))) + (((a *' b) *' c) + ((a *' (b `)) *' c)) by Def6 .= (((a *' b) *' c) + (((a *' b) *' (c `)) + ((a *' b) *' c))) + ((a *' (b `)) *' c) by LATTICES:def_5 .= ((((a *' b) *' c) + ((a *' b) *' c)) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c) by LATTICES:def_5 .= (((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c) by Def7 ; ::_thesis: verum end; theorem Th27: :: ROBBINS1:27 for L being non empty join-commutative join-associative Huntington ComplLLattStr for a, b, c being Element of L holds (a *' (b + c)) ` = (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)) proof let L be non empty join-commutative join-associative Huntington ComplLLattStr ; ::_thesis: for a, b, c being Element of L holds (a *' (b + c)) ` = (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)) let a, b, c be Element of L; ::_thesis: (a *' (b + c)) ` = (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)) set D = (a *' (b `)) *' (c `); set E = ((a `) *' b) *' c; set F = ((a `) *' b) *' (c `); set G = ((a `) *' (b `)) *' c; set H = ((a `) *' (b `)) *' (c `); A1: a ` = ((a `) *' b) + ((a `) *' (b `)) by Def6 .= ((((a `) *' b) *' c) + (((a `) *' b) *' (c `))) + ((a `) *' (b `)) by Def6 .= ((((a `) *' b) *' c) + (((a `) *' b) *' (c `))) + ((((a `) *' (b `)) *' c) + (((a `) *' (b `)) *' (c `))) by Def6 ; A2: (b `) *' (c `) = (a *' ((b `) *' (c `))) + ((a `) *' ((b `) *' (c `))) by Th1 .= ((a *' (b `)) *' (c `)) + ((a `) *' ((b `) *' (c `))) by Th16 .= ((a *' (b `)) *' (c `)) + (((a `) *' (b `)) *' (c `)) by Th16 ; (a *' (b + c)) ` = (a `) + ((b + c) `) by Th3 .= (a `) + ((((b `) *' (c `)) `) `) by Th17 .= (a `) + ((b `) *' (c `)) by Th3 ; hence (a *' (b + c)) ` = ((((((a `) *' b) *' c) + (((a `) *' b) *' (c `))) + ((((a `) *' (b `)) *' c) + (((a `) *' (b `)) *' (c `)))) + (((a `) *' (b `)) *' (c `))) + ((a *' (b `)) *' (c `)) by A1, A2, LATTICES:def_5 .= (((((((a `) *' b) *' c) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `))) + (((a `) *' (b `)) *' (c `))) + ((a *' (b `)) *' (c `)) by LATTICES:def_5 .= ((((((a `) *' b) *' c) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + ((((a `) *' (b `)) *' (c `)) + (((a `) *' (b `)) *' (c `)))) + ((a *' (b `)) *' (c `)) by LATTICES:def_5 .= ((((((a `) *' b) *' c) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `))) + ((a *' (b `)) *' (c `)) by Def7 .= ((a *' (b `)) *' (c `)) + (((((a `) *' b) *' c) + (((a `) *' b) *' (c `))) + ((((a `) *' (b `)) *' c) + (((a `) *' (b `)) *' (c `)))) by LATTICES:def_5 .= (((a *' (b `)) *' (c `)) + ((((a `) *' b) *' c) + (((a `) *' b) *' (c `)))) + ((((a `) *' (b `)) *' c) + (((a `) *' (b `)) *' (c `))) by LATTICES:def_5 .= ((((a *' (b `)) *' (c `)) + ((((a `) *' b) *' c) + (((a `) *' b) *' (c `)))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)) by LATTICES:def_5 .= (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)) by LATTICES:def_5 ; ::_thesis: verum end; theorem Th28: :: ROBBINS1:28 for L being non empty join-commutative join-associative Huntington ComplLLattStr for a, b, c being Element of L holds ((a *' b) + (a *' c)) + ((a *' (b + c)) `) = Top L proof let L be non empty join-commutative join-associative Huntington ComplLLattStr ; ::_thesis: for a, b, c being Element of L holds ((a *' b) + (a *' c)) + ((a *' (b + c)) `) = Top L let a, b, c be Element of L; ::_thesis: ((a *' b) + (a *' c)) + ((a *' (b + c)) `) = Top L set A = (a *' b) *' c; set B = (a *' b) *' (c `); set C = (a *' (b `)) *' c; set D = (a *' (b `)) *' (c `); set E = ((a `) *' b) *' c; set F = ((a `) *' b) *' (c `); set G = ((a `) *' (b `)) *' c; set H = ((a `) *' (b `)) *' (c `); set ABC = (((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c); set GH = (((a `) *' (b `)) *' c) + (((a `) *' (b `)) *' (c `)); ( (a *' (b + c)) ` = (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)) & (a *' b) + (a *' c) = (((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c) ) by Th26, Th27; then ((a *' b) + (a *' c)) + ((a *' (b + c)) `) = ((((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c)) + (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + ((((a `) *' (b `)) *' c) + (((a `) *' (b `)) *' (c `)))) by LATTICES:def_5 .= ((((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c)) + ((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + ((((a `) *' b) *' (c `)) + ((((a `) *' (b `)) *' c) + (((a `) *' (b `)) *' (c `))))) by LATTICES:def_5 .= (((((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c)) + (((a *' (b `)) *' (c `)) + (((a `) *' b) *' c))) + ((((a `) *' b) *' (c `)) + ((((a `) *' (b `)) *' c) + (((a `) *' (b `)) *' (c `)))) by LATTICES:def_5 .= ((((((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c)) + ((a *' (b `)) *' (c `))) + (((a `) *' b) *' c)) + ((((a `) *' b) *' (c `)) + ((((a `) *' (b `)) *' c) + (((a `) *' (b `)) *' (c `)))) by LATTICES:def_5 .= (((((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c)) + ((a *' (b `)) *' (c `))) + ((((a `) *' b) *' c) + ((((a `) *' b) *' (c `)) + ((((a `) *' (b `)) *' c) + (((a `) *' (b `)) *' (c `))))) by LATTICES:def_5 .= (((((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c)) + ((a *' (b `)) *' (c `))) + ((((a `) *' b) *' c) + (((((a `) *' b) *' (c `)) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) by LATTICES:def_5 .= ((((((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c)) + ((a *' (b `)) *' (c `))) + (((a `) *' b) *' c)) + (((((a `) *' b) *' (c `)) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `))) by LATTICES:def_5 .= ((((((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c)) + ((a *' (b `)) *' (c `))) + (((a `) *' b) *' c)) + ((((a `) *' b) *' (c `)) + ((((a `) *' (b `)) *' c) + (((a `) *' (b `)) *' (c `)))) by LATTICES:def_5 .= (((((((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c)) + ((a *' (b `)) *' (c `))) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + ((((a `) *' (b `)) *' c) + (((a `) *' (b `)) *' (c `))) by LATTICES:def_5 .= ((((((((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c)) + ((a *' (b `)) *' (c `))) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)) by LATTICES:def_5 .= Top L by Th24 ; hence ((a *' b) + (a *' c)) + ((a *' (b + c)) `) = Top L ; ::_thesis: verum end; theorem Th29: :: ROBBINS1:29 for L being non empty join-commutative join-associative Huntington ComplLLattStr for a, b, c being Element of L holds ((a *' b) + (a *' c)) *' ((a *' (b + c)) `) = Bot L proof let L be non empty join-commutative join-associative Huntington ComplLLattStr ; ::_thesis: for a, b, c being Element of L holds ((a *' b) + (a *' c)) *' ((a *' (b + c)) `) = Bot L let a, b, c be Element of L; ::_thesis: ((a *' b) + (a *' c)) *' ((a *' (b + c)) `) = Bot L set A = (a *' b) *' c; set B = (a *' b) *' (c `); set C = (a *' (b `)) *' c; set D = (a *' (b `)) *' (c `); set E = ((a `) *' b) *' c; set F = ((a `) *' b) *' (c `); set G = ((a `) *' (b `)) *' c; set H = ((a `) *' (b `)) *' (c `); set DEFG = ((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c); (((a *' b) *' c) *' ((a *' (b `)) *' (c `))) + (((a *' b) *' c) *' (((a `) *' b) *' c)) = (Bot L) + (((a *' b) *' c) *' (((a `) *' b) *' c)) by Th25 .= (Bot L) + (Bot L) by Th25 .= Bot L by Def7 ; then Top L = (Bot L) + ((((a *' b) *' c) *' (((a *' (b `)) *' (c `)) + (((a `) *' b) *' c))) `) by Th28 .= (((a *' b) *' c) *' (((a *' (b `)) *' (c `)) + (((a `) *' b) *' c))) ` by Th13 ; then Bot L = ((((a *' b) *' c) *' (((a *' (b `)) *' (c `)) + (((a `) *' b) *' c))) `) ` by Th9 .= ((a *' b) *' c) *' (((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) by Th3 ; then (((a *' b) *' c) *' (((a *' (b `)) *' (c `)) + (((a `) *' b) *' c))) + (((a *' b) *' c) *' (((a `) *' b) *' (c `))) = (Bot L) + (Bot L) by Th25 .= Bot L by Def7 ; then Top L = (Bot L) + ((((a *' b) *' c) *' ((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `)))) `) by Th28 .= (((a *' b) *' c) *' ((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `)))) ` by Th13 ; then A1: Bot L = ((((a *' b) *' c) *' ((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `)))) `) ` by Th9 .= ((a *' b) *' c) *' ((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) by Th3 ; ((a *' b) *' c) *' (((a `) *' (b `)) *' c) = Bot L by Th25; then (((a *' b) *' c) *' ((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `)))) + (((a *' b) *' c) *' (((a `) *' (b `)) *' c)) = Bot L by A1, Def7; then Top L = (Bot L) + ((((a *' b) *' c) *' (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c))) `) by Th28 .= (((a *' b) *' c) *' (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c))) ` by Th13 ; then Bot L = ((((a *' b) *' c) *' (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c))) `) ` by Th9 .= ((a *' b) *' c) *' (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) by Th3 ; then (((a *' b) *' c) *' (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c))) + (((a *' b) *' c) *' (((a `) *' (b `)) *' (c `))) = (Bot L) + (Bot L) by Th25 .= Bot L by Def7 ; then A2: Top L = (Bot L) + ((((a *' b) *' c) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) `) by Th28 .= (((a *' b) *' c) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) ` by Th13 ; (((a *' b) *' (c `)) *' ((a *' (b `)) *' (c `))) + (((a *' b) *' (c `)) *' (((a `) *' b) *' c)) = (Bot L) + (((a *' b) *' (c `)) *' (((a `) *' b) *' c)) by Th25 .= (Bot L) + (Bot L) by Th25 .= Bot L by Def7 ; then Top L = (Bot L) + ((((a *' b) *' (c `)) *' (((a *' (b `)) *' (c `)) + (((a `) *' b) *' c))) `) by Th28 .= (((a *' b) *' (c `)) *' (((a *' (b `)) *' (c `)) + (((a `) *' b) *' c))) ` by Th13 ; then Bot L = ((((a *' b) *' (c `)) *' (((a *' (b `)) *' (c `)) + (((a `) *' b) *' c))) `) ` by Th9 .= ((a *' b) *' (c `)) *' (((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) by Th3 ; then (((a *' b) *' (c `)) *' (((a *' (b `)) *' (c `)) + (((a `) *' b) *' c))) + (((a *' b) *' (c `)) *' (((a `) *' b) *' (c `))) = (Bot L) + (Bot L) by Th25 .= Bot L by Def7 ; then Top L = (Bot L) + ((((a *' b) *' (c `)) *' ((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `)))) `) by Th28 .= (((a *' b) *' (c `)) *' ((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `)))) ` by Th13 ; then Bot L = ((((a *' b) *' (c `)) *' ((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `)))) `) ` by Th9 .= ((a *' b) *' (c `)) *' ((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) by Th3 ; then (((a *' b) *' (c `)) *' ((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `)))) + (((a *' b) *' (c `)) *' (((a `) *' (b `)) *' c)) = (Bot L) + (Bot L) by Th25 .= Bot L by Def7 ; then Top L = (Bot L) + ((((a *' b) *' (c `)) *' (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c))) `) by Th28 .= (((a *' b) *' (c `)) *' (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c))) ` by Th13 ; then A3: Bot L = ((((a *' b) *' (c `)) *' (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c))) `) ` by Th9 .= ((a *' b) *' (c `)) *' (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) by Th3 ; ((a *' (b `)) *' c) *' ((a *' (b `)) *' (c `)) = Bot L by Th25; then (((a *' (b `)) *' c) *' ((a *' (b `)) *' (c `))) + (((a *' (b `)) *' c) *' (((a `) *' b) *' c)) = (Bot L) + (Bot L) by Th25 .= Bot L by Def7 ; then Top L = (Bot L) + ((((a *' (b `)) *' c) *' (((a *' (b `)) *' (c `)) + (((a `) *' b) *' c))) `) by Th28 .= (((a *' (b `)) *' c) *' (((a *' (b `)) *' (c `)) + (((a `) *' b) *' c))) ` by Th13 ; then Bot L = ((((a *' (b `)) *' c) *' (((a *' (b `)) *' (c `)) + (((a `) *' b) *' c))) `) ` by Th9 .= ((a *' (b `)) *' c) *' (((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) by Th3 ; then (((a *' (b `)) *' c) *' (((a *' (b `)) *' (c `)) + (((a `) *' b) *' c))) + (((a *' (b `)) *' c) *' (((a `) *' b) *' (c `))) = (Bot L) + (Bot L) by Th25 .= Bot L by Def7 ; then Top L = (Bot L) + ((((a *' (b `)) *' c) *' ((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `)))) `) by Th28 .= (((a *' (b `)) *' c) *' ((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `)))) ` by Th13 ; then Bot L = ((((a *' (b `)) *' c) *' ((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `)))) `) ` by Th9 .= ((a *' (b `)) *' c) *' ((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) by Th3 ; then (((a *' (b `)) *' c) *' ((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `)))) + (((a *' (b `)) *' c) *' (((a `) *' (b `)) *' c)) = (Bot L) + (Bot L) by Th25 .= Bot L by Def7 ; then Top L = (Bot L) + ((((a *' (b `)) *' c) *' (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c))) `) by Th28 .= (((a *' (b `)) *' c) *' (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c))) ` by Th13 ; then Bot L = ((((a *' (b `)) *' c) *' (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c))) `) ` by Th9 .= ((a *' (b `)) *' c) *' (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) by Th3 ; then (((a *' (b `)) *' c) *' (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c))) + (((a *' (b `)) *' c) *' (((a `) *' (b `)) *' (c `))) = (Bot L) + (Bot L) by Th25 .= Bot L by Def7 ; then A4: Top L = (Bot L) + ((((a *' (b `)) *' c) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) `) by Th28 .= (((a *' (b `)) *' c) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) ` by Th13 ; ((a *' b) *' (c `)) *' (((a `) *' (b `)) *' (c `)) = Bot L by Th25; then (((a *' b) *' (c `)) *' (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c))) + (((a *' b) *' (c `)) *' (((a `) *' (b `)) *' (c `))) = Bot L by A3, Def7; then A5: Top L = (Bot L) + ((((a *' b) *' (c `)) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) `) by Th28 .= (((a *' b) *' (c `)) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) ` by Th13 ; A6: ((a *' b) *' (c `)) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `))) = ((((a *' b) *' (c `)) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) `) ` by Th3 .= Bot L by A5, Th9 ; ((a *' b) *' c) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `))) = ((((a *' b) *' c) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) `) ` by Th3 .= Bot L by A2, Th9 ; then (((a *' b) *' c) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) + (((a *' b) *' (c `)) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) = Bot L by A6, Def7; then Top L = (Bot L) + (((((a *' b) *' c) + ((a *' b) *' (c `))) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) `) by Th28 .= ((((a *' b) *' c) + ((a *' b) *' (c `))) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) ` by Th13 ; then A7: Bot L = (((((a *' b) *' c) + ((a *' b) *' (c `))) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) `) ` by Th9 .= (((a *' b) *' c) + ((a *' b) *' (c `))) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `))) by Th3 ; ((a *' (b `)) *' c) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `))) = ((((a *' (b `)) *' c) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) `) ` by Th3 .= Bot L by A4, Th9 ; then ((((a *' b) *' c) + ((a *' b) *' (c `))) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) + (((a *' (b `)) *' c) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) = Bot L by A7, Def7; then Top L = (Bot L) + ((((((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c)) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) `) by Th28 .= (((((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c)) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) ` by Th13 ; then A8: Bot L = ((((((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c)) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)))) `) ` by Th9 .= ((((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c)) *' ((((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `))) by Th3 ; (a *' (b + c)) ` = (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)) by Th27; hence ((a *' b) + (a *' c)) *' ((a *' (b + c)) `) = Bot L by A8, Th26; ::_thesis: verum end; theorem Th30: :: ROBBINS1:30 for L being non empty join-commutative join-associative Huntington ComplLLattStr for a, b, c being Element of L holds a *' (b + c) = (a *' b) + (a *' c) proof let L be non empty join-commutative join-associative Huntington ComplLLattStr ; ::_thesis: for a, b, c being Element of L holds a *' (b + c) = (a *' b) + (a *' c) let a, b, c be Element of L; ::_thesis: a *' (b + c) = (a *' b) + (a *' c) ( ((a *' b) + (a *' c)) + ((a *' (b + c)) `) = Top L & ((a *' b) + (a *' c)) *' ((a *' (b + c)) `) = Bot L ) by Th28, Th29; then ((a *' b) + (a *' c)) ` = (a *' (b + c)) ` by Th23; hence a *' (b + c) = (a *' b) + (a *' c) by Th10; ::_thesis: verum end; theorem :: ROBBINS1:31 for L being non empty join-commutative join-associative Huntington ComplLLattStr for a, b, c being Element of L holds a + (b *' c) = (a + b) *' (a + c) proof let L be non empty join-commutative join-associative Huntington ComplLLattStr ; ::_thesis: for a, b, c being Element of L holds a + (b *' c) = (a + b) *' (a + c) let a, b, c be Element of L; ::_thesis: a + (b *' c) = (a + b) *' (a + c) thus a + (b *' c) = ((a `) *' ((((b `) + (c `)) `) `)) ` by Th17 .= ((a `) *' ((b `) + (c `))) ` by Th3 .= (((a `) *' (b `)) + ((a `) *' (c `))) ` by Th30 .= (((((a `) *' (b `)) `) *' (((a `) *' (c `)) `)) `) ` by Th17 .= (((a `) *' (b `)) `) *' (((a `) *' (c `)) `) by Th3 .= (a + b) *' (((a `) *' (c `)) `) by Th17 .= (a + b) *' (a + c) by Th17 ; ::_thesis: verum end; begin definition let L be non empty OrthoLattStr ; attrL is well-complemented means :Def10: :: ROBBINS1:def 10 for a being Element of L holds a ` is_a_complement_of a; end; :: deftheorem Def10 defines well-complemented ROBBINS1:def_10_:_ for L being non empty OrthoLattStr holds ( L is well-complemented iff for a being Element of L holds a ` is_a_complement_of a ); registration cluster TrivOrtLat -> Boolean strict well-complemented ; coherence ( TrivOrtLat is Boolean & TrivOrtLat is well-complemented ) proof set L = TrivOrtLat ; thus TrivOrtLat is lower-bounded ; :: according to LATTICES:def_15,LATTICES:def_20 ::_thesis: ( TrivOrtLat is upper-bounded & TrivOrtLat is complemented & TrivOrtLat is distributive & TrivOrtLat is well-complemented ) thus TrivOrtLat is upper-bounded ; ::_thesis: ( TrivOrtLat is complemented & TrivOrtLat is distributive & TrivOrtLat is well-complemented ) thus TrivOrtLat is complemented ::_thesis: ( TrivOrtLat is distributive & TrivOrtLat is well-complemented ) proof let b be Element of TrivOrtLat; :: according to LATTICES:def_19 ::_thesis: ex b1 being M2( the carrier of TrivOrtLat) st b1 is_a_complement_of b take a = b; ::_thesis: a is_a_complement_of b ( a "\/" b = Top TrivOrtLat & a "/\" b = Bottom TrivOrtLat ) by STRUCT_0:def_10; hence a is_a_complement_of b by LATTICES:def_18; ::_thesis: verum end; thus TrivOrtLat is distributive ::_thesis: TrivOrtLat is well-complemented proof let x, y, z be Element of TrivOrtLat; :: according to LATTICES:def_11 ::_thesis: x "/\" (y + z) = (x "/\" y) + (x "/\" z) thus x "/\" (y + z) = (x "/\" y) + (x "/\" z) by STRUCT_0:def_10; ::_thesis: verum end; thus TrivOrtLat is well-complemented ::_thesis: verum proof let a be Element of TrivOrtLat; :: according to ROBBINS1:def_10 ::_thesis: a ` is_a_complement_of a ( (a `) "\/" a = Top TrivOrtLat & (a `) "/\" a = Bottom TrivOrtLat ) by STRUCT_0:def_10; hence a ` is_a_complement_of a by LATTICES:def_18; ::_thesis: verum end; end; end; definition mode preOrthoLattice is non empty Lattice-like OrthoLattStr ; end; registration cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like Boolean strict well-complemented for OrthoLattStr ; existence ex b1 being preOrthoLattice st ( b1 is strict & b1 is Boolean & b1 is well-complemented ) proof take TrivOrtLat ; ::_thesis: ( TrivOrtLat is strict & TrivOrtLat is Boolean & TrivOrtLat is well-complemented ) thus ( TrivOrtLat is strict & TrivOrtLat is Boolean & TrivOrtLat is well-complemented ) ; ::_thesis: verum end; end; theorem Th32: :: ROBBINS1:32 for L being distributive well-complemented preOrthoLattice for x being Element of L holds (x `) ` = x proof let L be distributive well-complemented preOrthoLattice; ::_thesis: for x being Element of L holds (x `) ` = x let x be Element of L; ::_thesis: (x `) ` = x (x `) ` is_a_complement_of x ` by Def10; then A1: ( ((x `) `) + (x `) = Top L & ((x `) `) "/\" (x `) = Bottom L ) by LATTICES:def_18; x ` is_a_complement_of x by Def10; then ( (x `) "\/" x = Top L & (x `) "/\" x = Bottom L ) by LATTICES:def_18; hence (x `) ` = x by A1, LATTICES:12; ::_thesis: verum end; theorem Th33: :: ROBBINS1:33 for L being distributive bounded well-complemented preOrthoLattice for x, y being Element of L holds x "/\" y = ((x `) "\/" (y `)) ` proof let L be distributive bounded well-complemented preOrthoLattice; ::_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 `)) ` A1: (x `) "\/" (Top L) = Top L ; A2: (y `) "\/" (Top L) = Top L ; A3: y ` is_a_complement_of y by Def10; then A4: (y `) "\/" y = Top L by LATTICES:def_18; (x "/\" y) ` is_a_complement_of x "/\" y by Def10; then A5: ( ((x "/\" y) `) "\/" (x "/\" y) = Top L & ((x "/\" y) `) "/\" (x "/\" y) = Bottom L ) by LATTICES:def_18; A6: x ` is_a_complement_of x by Def10; then A7: (x `) "\/" x = Top L by LATTICES:def_18; A8: (y `) "/\" y = Bottom L by A3, LATTICES:def_18; A9: (x `) "/\" x = Bottom L by A6, LATTICES:def_18; A10: ((x `) "\/" (y `)) "/\" (x "/\" y) = ((x "/\" y) "/\" (x `)) "\/" ((x "/\" y) "/\" (y `)) by LATTICES:def_11 .= (y "/\" (x "/\" (x `))) "\/" ((x "/\" y) "/\" (y `)) by LATTICES:def_7 .= (y "/\" (Bottom L)) "\/" (x "/\" (y "/\" (y `))) by A9, LATTICES:def_7 .= (Bottom L) "\/" (x "/\" (Bottom L)) by A8 .= (Bottom L) "\/" (Bottom L) .= Bottom L ; ((x `) "\/" (y `)) "\/" (x "/\" y) = (((x `) "\/" (y `)) "\/" x) "/\" (((x `) "\/" (y `)) "\/" y) by LATTICES:11 .= (((y `) "\/" (x `)) "\/" x) "/\" (Top L) by A4, A1, LATTICES:def_5 .= (Top L) "/\" (Top L) by A7, A2, LATTICES:def_5 .= Top L ; then (x "/\" y) ` = (x `) "\/" (y `) by A10, A5, LATTICES:12; hence x "/\" y = ((x `) "\/" (y `)) ` by Th32; ::_thesis: verum end; begin definition let L be non empty ComplLLattStr ; func CLatt L -> strict OrthoLattStr means :Def11: :: ROBBINS1:def 11 ( the carrier of it = the carrier of L & the L_join of it = the L_join of L & the Compl of it = the Compl of L & ( for a, b being Element of L holds the L_meet of it . (a,b) = a *' b ) ); existence ex b1 being strict OrthoLattStr st ( the carrier of b1 = the carrier of L & the L_join of b1 = the L_join of L & the Compl of b1 = the Compl of L & ( for a, b being Element of L holds the L_meet of b1 . (a,b) = a *' b ) ) proof deffunc H1( Element of L, Element of L) -> Element of L = $1 *' $2; consider K being BinOp of the carrier of L such that A1: for a, b being Element of L holds K . (a,b) = H1(a,b) from BINOP_1:sch_4(); take OrthoLattStr(# the carrier of L, the L_join of L,K, the Compl of L #) ; ::_thesis: ( the carrier of OrthoLattStr(# the carrier of L, the L_join of L,K, the Compl of L #) = the carrier of L & the L_join of OrthoLattStr(# the carrier of L, the L_join of L,K, the Compl of L #) = the L_join of L & the Compl of OrthoLattStr(# the carrier of L, the L_join of L,K, the Compl of L #) = the Compl of L & ( for a, b being Element of L holds the L_meet of OrthoLattStr(# the carrier of L, the L_join of L,K, the Compl of L #) . (a,b) = a *' b ) ) thus ( the carrier of OrthoLattStr(# the carrier of L, the L_join of L,K, the Compl of L #) = the carrier of L & the L_join of OrthoLattStr(# the carrier of L, the L_join of L,K, the Compl of L #) = the L_join of L & the Compl of OrthoLattStr(# the carrier of L, the L_join of L,K, the Compl of L #) = the Compl of L & ( for a, b being Element of L holds the L_meet of OrthoLattStr(# the carrier of L, the L_join of L,K, the Compl of L #) . (a,b) = a *' b ) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being strict OrthoLattStr st the carrier of b1 = the carrier of L & the L_join of b1 = the L_join of L & the Compl of b1 = the Compl of L & ( for a, b being Element of L holds the L_meet of b1 . (a,b) = a *' b ) & the carrier of b2 = the carrier of L & the L_join of b2 = the L_join of L & the Compl of b2 = the Compl of L & ( for a, b being Element of L holds the L_meet of b2 . (a,b) = a *' b ) holds b1 = b2 proof let L1, L2 be strict OrthoLattStr ; ::_thesis: ( the carrier of L1 = the carrier of L & the L_join of L1 = the L_join of L & the Compl of L1 = the Compl of L & ( for a, b being Element of L holds the L_meet of L1 . (a,b) = a *' b ) & the carrier of L2 = the carrier of L & the L_join of L2 = the L_join of L & the Compl of L2 = the Compl of L & ( for a, b being Element of L holds the L_meet of L2 . (a,b) = a *' b ) implies L1 = L2 ) assume that A2: the carrier of L1 = the carrier of L and A3: ( the L_join of L1 = the L_join of L & the Compl of L1 = the Compl of L ) and A4: for a, b being Element of L holds the L_meet of L1 . (a,b) = a *' b and A5: the carrier of L2 = the carrier of L and A6: ( the L_join of L2 = the L_join of L & the Compl of L2 = the Compl of L ) and A7: for a, b being Element of L holds the L_meet of L2 . (a,b) = a *' b ; ::_thesis: L1 = L2 reconsider A = the L_meet of L1, B = the L_meet of L2 as BinOp of the carrier of L by A2, A5; now__::_thesis:_for_a,_b_being_Element_of_L_holds_A_._(a,b)_=_B_._(a,b) let a, b be Element of L; ::_thesis: A . (a,b) = B . (a,b) thus A . (a,b) = a *' b by A4 .= B . (a,b) by A7 ; ::_thesis: verum end; hence L1 = L2 by A2, A3, A5, A6, BINOP_1:2; ::_thesis: verum end; end; :: deftheorem Def11 defines CLatt ROBBINS1:def_11_:_ for L being non empty ComplLLattStr for b2 being strict OrthoLattStr holds ( b2 = CLatt L iff ( the carrier of b2 = the carrier of L & the L_join of b2 = the L_join of L & the Compl of b2 = the Compl of L & ( for a, b being Element of L holds the L_meet of b2 . (a,b) = a *' b ) ) ); registration let L be non empty ComplLLattStr ; cluster CLatt L -> non empty strict ; coherence not CLatt L is empty proof the carrier of (CLatt L) = the carrier of L by Def11; hence not CLatt L is empty ; ::_thesis: verum end; end; registration let L be non empty join-commutative ComplLLattStr ; cluster CLatt L -> join-commutative strict ; coherence CLatt L is join-commutative proof let a, b be Element of (CLatt L); :: according to LATTICES:def_4 ::_thesis: a + b = b + a ( the carrier of L = the carrier of (CLatt L) & the L_join of L = the L_join of (CLatt L) ) by Def11; hence a + b = b + a by BINOP_1:def_2; ::_thesis: verum end; end; registration let L be non empty join-associative ComplLLattStr ; cluster CLatt L -> join-associative strict ; coherence CLatt L is join-associative proof set K = the L_join of L; set M = the L_join of (CLatt L); let a, b, c be Element of (CLatt L); :: according to LATTICES:def_5 ::_thesis: a + (b + c) = (a + b) + c ( the carrier of L = the carrier of (CLatt L) & the L_join of L = the L_join of (CLatt L) ) by Def11; hence a + (b + c) = (a + b) + c by BINOP_1:def_3; ::_thesis: verum end; end; registration let L be non empty join-commutative join-associative ComplLLattStr ; cluster CLatt L -> meet-commutative strict ; coherence CLatt L is meet-commutative proof let a, b be Element of (CLatt L); :: according to LATTICES:def_6 ::_thesis: a "/\" b = b "/\" a reconsider a9 = a, b9 = b as Element of L by Def11; thus a "/\" b = b9 *' a9 by Def11 .= b "/\" a by Def11 ; ::_thesis: verum end; end; theorem :: ROBBINS1:34 for L being non empty ComplLLattStr for a, b being Element of L for a9, b9 being Element of (CLatt L) st a = a9 & b = b9 holds ( a *' b = a9 "/\" b9 & a + b = a9 "\/" b9 & a ` = a9 ` ) by Def11; registration let L be non empty join-commutative join-associative Huntington ComplLLattStr ; cluster CLatt L -> meet-associative meet-absorbing join-absorbing strict ; coherence ( CLatt L is meet-associative & CLatt L is join-absorbing & CLatt L is meet-absorbing ) proof hereby :: according to LATTICES:def_7 ::_thesis: ( CLatt L is join-absorbing & CLatt L is meet-absorbing ) let a, b, c be Element of (CLatt L); ::_thesis: (a "/\" b) "/\" c = a "/\" (b "/\" c) reconsider a9 = a, b9 = b, c9 = c as Element of L by Def11; A1: b9 *' c9 = b "/\" c by Def11; a9 *' b9 = a "/\" b by Def11; hence (a "/\" b) "/\" c = (a9 *' b9) *' c9 by Def11 .= a9 *' (b9 *' c9) by Th16 .= a "/\" (b "/\" c) by A1, Def11 ; ::_thesis: verum end; hereby :: according to LATTICES:def_9 ::_thesis: CLatt L is meet-absorbing let a, b be Element of (CLatt L); ::_thesis: a "/\" (a "\/" b) = a reconsider a9 = a, b9 = b as Element of L by Def11; a9 + b9 = a "\/" b by Def11; hence a "/\" (a "\/" b) = a9 *' (a9 + b9) by Def11 .= a by Th21 ; ::_thesis: verum end; let a, b be Element of (CLatt L); :: according to LATTICES:def_8 ::_thesis: (a "/\" b) + b = b reconsider a9 = a, b9 = b as Element of L by Def11; a9 *' b9 = a "/\" b by Def11; hence (a "/\" b) "\/" b = (a9 *' b9) + b9 by Def11 .= b by Th20 ; ::_thesis: verum end; end; registration let L be non empty Huntington ComplLLattStr ; cluster CLatt L -> strict Huntington ; coherence CLatt L is Huntington proof let x, y be Element of (CLatt L); :: according to ROBBINS1:def_6 ::_thesis: (((x `) + (y `)) `) + (((x `) + y) `) = x reconsider x9 = x, y9 = y as Element of L by Def11; A1: x ` = x9 ` by Def11; y ` = y9 ` by Def11; then (x `) + (y `) = (x9 `) + (y9 `) by A1, Def11; then A2: ((x `) + (y `)) ` = ((x9 `) + (y9 `)) ` by Def11; (x `) + y = (x9 `) + y9 by A1, Def11; then ((x `) + y) ` = ((x9 `) + y9) ` by Def11; hence (((x `) + (y `)) `) + (((x `) + y) `) = (((x9 `) + (y9 `)) `) + (((x9 `) + y9) `) by A2, Def11 .= x by Def6 ; ::_thesis: verum end; end; registration let L be non empty join-commutative join-associative Huntington ComplLLattStr ; cluster CLatt L -> lower-bounded strict ; coherence CLatt L is lower-bounded proof thus CLatt L is lower-bounded ::_thesis: verum proof set c9 = Bot L; reconsider c = Bot L as Element of (CLatt L) by Def11; take c ; :: according to LATTICES:def_13 ::_thesis: for b1 being M2( the carrier of (CLatt L)) holds ( c "/\" b1 = c & b1 "/\" c = c ) let a be Element of (CLatt L); ::_thesis: ( c "/\" a = c & a "/\" c = c ) reconsider a9 = a as Element of L by Def11; thus c "/\" a = (Bot L) *' a9 by Def11 .= c by Def9 ; ::_thesis: a "/\" c = c hence a "/\" c = c ; ::_thesis: verum end; end; end; theorem Th35: :: ROBBINS1:35 for L being non empty join-commutative join-associative Huntington ComplLLattStr holds Bot L = Bottom (CLatt L) proof let L be non empty join-commutative join-associative Huntington ComplLLattStr ; ::_thesis: Bot L = Bottom (CLatt L) reconsider C = Bot L as Element of (CLatt L) by Def11; for a being Element of (CLatt L) holds ( C "/\" a = C & a "/\" C = C ) proof let a be Element of (CLatt L); ::_thesis: ( C "/\" a = C & a "/\" C = C ) reconsider a9 = a as Element of L by Def11; thus C "/\" a = (Bot L) *' a9 by Def11 .= C by Def9 ; ::_thesis: a "/\" C = C hence a "/\" C = C ; ::_thesis: verum end; hence Bot L = Bottom (CLatt L) by LATTICES:def_16; ::_thesis: verum end; registration let L be non empty join-commutative join-associative Huntington ComplLLattStr ; cluster CLatt L -> distributive bounded complemented strict ; coherence ( CLatt L is complemented & CLatt L is distributive & CLatt L is bounded ) proof thus CLatt L is complemented ::_thesis: ( CLatt L is distributive & CLatt L is bounded ) proof let b be Element of (CLatt L); :: according to LATTICES:def_19 ::_thesis: ex b1 being M2( the carrier of (CLatt L)) st b1 is_a_complement_of b take a = b ` ; ::_thesis: a is_a_complement_of b reconsider a9 = a, b9 = b as Element of L by Def11; thus a + b = Top (CLatt L) by Def8; :: according to LATTICES:def_18 ::_thesis: ( b + a = Top (CLatt L) & a "/\" b = Bottom (CLatt L) & b "/\" a = Bottom (CLatt L) ) thus b + a = Top (CLatt L) by Def8; ::_thesis: ( a "/\" b = Bottom (CLatt L) & b "/\" a = Bottom (CLatt L) ) A1: a9 ` = a ` by Def11 .= b9 by Th3 ; thus a "/\" b = a9 *' b9 by Def11 .= Bot L by A1, Th8 .= Bottom (CLatt L) by Th35 ; ::_thesis: b "/\" a = Bottom (CLatt L) hence b "/\" a = Bottom (CLatt L) ; ::_thesis: verum end; hereby :: according to LATTICES:def_11 ::_thesis: CLatt L is bounded let a, b, c be Element of (CLatt L); ::_thesis: a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) reconsider a9 = a, b9 = b, c9 = c as Element of L by Def11; A2: ( a "/\" b = a9 *' b9 & a "/\" c = a9 *' c9 ) by Def11; b9 + c9 = b "\/" c by Def11; hence a "/\" (b "\/" c) = a9 *' (b9 + c9) by Def11 .= (a9 *' b9) + (a9 *' c9) by Th30 .= (a "/\" b) "\/" (a "/\" c) by A2, Def11 ; ::_thesis: verum end; thus CLatt L is lower-bounded ; :: according to LATTICES:def_15 ::_thesis: CLatt L is upper-bounded thus CLatt L is upper-bounded ; ::_thesis: verum end; end; begin notation let G be non empty ComplLLattStr ; let x be Element of G; synonym - x for x ` ; end; definition let G be non empty join-commutative ComplLLattStr ; redefine attr G is Huntington means :Def12: :: ROBBINS1:def 12 for x, y being Element of G holds (- ((- x) + (- y))) + (- (x + (- y))) = y; compatibility ( G is Huntington iff for x, y being Element of G holds (- ((- x) + (- y))) + (- (x + (- y))) = y ) proof thus ( G is Huntington implies for x, y being Element of G holds (- ((- x) + (- y))) + (- (x + (- y))) = y ) by Def6; ::_thesis: ( ( for x, y being Element of G holds (- ((- x) + (- y))) + (- (x + (- y))) = y ) implies G is Huntington ) assume A1: for x, y being Element of G holds (- ((- x) + (- y))) + (- (x + (- y))) = y ; ::_thesis: G is Huntington let x, y be Element of G; :: according to ROBBINS1:def_6 ::_thesis: (((x `) + (y `)) `) + (((x `) + y) `) = x (((x `) + (y `)) `) + (((x `) + y) `) = x by A1; hence (((x `) + (y `)) `) + (((x `) + y) `) = x ; ::_thesis: verum end; end; :: deftheorem Def12 defines Huntington ROBBINS1:def_12_:_ for G being non empty join-commutative ComplLLattStr holds ( G is Huntington iff for x, y being Element of G holds (- ((- x) + (- y))) + (- (x + (- y))) = y ); definition let G be non empty ComplLLattStr ; attrG is with_idempotent_element means :Def13: :: ROBBINS1:def 13 ex x being Element of G st x + x = x; correctness ; end; :: deftheorem Def13 defines with_idempotent_element ROBBINS1:def_13_:_ for G being non empty ComplLLattStr holds ( G is with_idempotent_element iff ex x being Element of G st x + x = x ); definition let G be non empty ComplLLattStr ; let x, y be Element of G; func \delta (x,y) -> Element of G equals :: ROBBINS1:def 14 - ((- x) + y); coherence - ((- x) + y) is Element of G ; end; :: deftheorem defines \delta ROBBINS1:def_14_:_ for G being non empty ComplLLattStr for x, y being Element of G holds \delta (x,y) = - ((- x) + y); definition let G be non empty ComplLLattStr ; let x, y be Element of G; func Expand (x,y) -> Element of G equals :: ROBBINS1:def 15 \delta ((x + y),(\delta (x,y))); coherence \delta ((x + y),(\delta (x,y))) is Element of G ; end; :: deftheorem defines Expand ROBBINS1:def_15_:_ for G being non empty ComplLLattStr for x, y being Element of G holds Expand (x,y) = \delta ((x + y),(\delta (x,y))); definition let G be non empty ComplLLattStr ; let x be Element of G; funcx _0 -> Element of G equals :: ROBBINS1:def 16 - ((- x) + x); coherence - ((- x) + x) is Element of G ; func Double x -> Element of G equals :: ROBBINS1:def 17 x + x; coherence x + x is Element of G ; end; :: deftheorem defines _0 ROBBINS1:def_16_:_ for G being non empty ComplLLattStr for x being Element of G holds x _0 = - ((- x) + x); :: deftheorem defines Double ROBBINS1:def_17_:_ for G being non empty ComplLLattStr for x being Element of G holds Double x = x + x; definition let G be non empty ComplLLattStr ; let x be Element of G; funcx _1 -> Element of G equals :: ROBBINS1:def 18 (x _0) + x; coherence (x _0) + x is Element of G ; funcx _2 -> Element of G equals :: ROBBINS1:def 19 (x _0) + (Double x); coherence (x _0) + (Double x) is Element of G ; funcx _3 -> Element of G equals :: ROBBINS1:def 20 (x _0) + ((Double x) + x); coherence (x _0) + ((Double x) + x) is Element of G ; funcx _4 -> Element of G equals :: ROBBINS1:def 21 (x _0) + ((Double x) + (Double x)); coherence (x _0) + ((Double x) + (Double x)) is Element of G ; end; :: deftheorem defines _1 ROBBINS1:def_18_:_ for G being non empty ComplLLattStr for x being Element of G holds x _1 = (x _0) + x; :: deftheorem defines _2 ROBBINS1:def_19_:_ for G being non empty ComplLLattStr for x being Element of G holds x _2 = (x _0) + (Double x); :: deftheorem defines _3 ROBBINS1:def_20_:_ for G being non empty ComplLLattStr for x being Element of G holds x _3 = (x _0) + ((Double x) + x); :: deftheorem defines _4 ROBBINS1:def_21_:_ for G being non empty ComplLLattStr for x being Element of G holds x _4 = (x _0) + ((Double x) + (Double x)); theorem Th36: :: ROBBINS1:36 for G being non empty join-commutative join-associative Robbins ComplLLattStr for x, y being Element of G holds \delta ((x + y),(\delta (x,y))) = y proof let G be non empty join-commutative join-associative Robbins ComplLLattStr ; ::_thesis: for x, y being Element of G holds \delta ((x + y),(\delta (x,y))) = y let x, y be Element of G; ::_thesis: \delta ((x + y),(\delta (x,y))) = y thus \delta ((x + y),(\delta (x,y))) = - ((- (x + y)) + (- ((- x) + y))) .= y by Def5 ; ::_thesis: verum end; theorem :: ROBBINS1:37 for G being non empty join-commutative join-associative Robbins ComplLLattStr for x, y being Element of G holds Expand (x,y) = y by Th36; theorem :: ROBBINS1:38 for G being non empty join-commutative join-associative Robbins ComplLLattStr for x, y, z being Element of G holds \delta (((- x) + y),z) = - ((\delta (x,y)) + z) ; theorem :: ROBBINS1:39 for G being non empty join-commutative join-associative Robbins ComplLLattStr for x being Element of G holds \delta (x,x) = x _0 ; theorem Th40: :: ROBBINS1:40 for G being non empty join-commutative join-associative Robbins ComplLLattStr for x being Element of G holds \delta ((Double x),(x _0)) = x proof let G be non empty join-commutative join-associative Robbins ComplLLattStr ; ::_thesis: for x being Element of G holds \delta ((Double x),(x _0)) = x let x be Element of G; ::_thesis: \delta ((Double x),(x _0)) = x thus \delta ((Double x),(x _0)) = Expand (x,x) .= x by Th36 ; ::_thesis: verum end; theorem Th41: :: ROBBINS1:41 for G being non empty join-commutative join-associative Robbins ComplLLattStr for x being Element of G holds \delta ((x _2),x) = x _0 proof let G be non empty join-commutative join-associative Robbins ComplLLattStr ; ::_thesis: for x being Element of G holds \delta ((x _2),x) = x _0 let x be Element of G; ::_thesis: \delta ((x _2),x) = x _0 thus \delta ((x _2),x) = \delta (((Double x) + (x _0)),(\delta ((Double x),(x _0)))) by Th40 .= x _0 by Th36 ; ::_thesis: verum end; theorem Th42: :: ROBBINS1:42 for G being non empty join-commutative join-associative Robbins ComplLLattStr for x being Element of G holds (x _4) + (x _0) = (x _3) + (x _1) proof let G be non empty join-commutative join-associative Robbins ComplLLattStr ; ::_thesis: for x being Element of G holds (x _4) + (x _0) = (x _3) + (x _1) let x be Element of G; ::_thesis: (x _4) + (x _0) = (x _3) + (x _1) thus (x _4) + (x _0) = (((x _0) + (Double x)) + (Double x)) + (x _0) by LATTICES:def_5 .= ((((x _0) + (Double x)) + x) + x) + (x _0) by LATTICES:def_5 .= ((x _3) + x) + (x _0) by LATTICES:def_5 .= (x _3) + (x _1) by LATTICES:def_5 ; ::_thesis: verum end; theorem Th43: :: ROBBINS1:43 for G being non empty join-commutative join-associative Robbins ComplLLattStr for x being Element of G holds (x _3) + (x _0) = (x _2) + (x _1) proof let G be non empty join-commutative join-associative Robbins ComplLLattStr ; ::_thesis: for x being Element of G holds (x _3) + (x _0) = (x _2) + (x _1) let x be Element of G; ::_thesis: (x _3) + (x _0) = (x _2) + (x _1) thus (x _3) + (x _0) = (((x _0) + (Double x)) + x) + (x _0) by LATTICES:def_5 .= (x _2) + (x _1) by LATTICES:def_5 ; ::_thesis: verum end; theorem Th44: :: ROBBINS1:44 for G being non empty join-commutative join-associative Robbins ComplLLattStr for x being Element of G holds (x _3) + x = x _4 proof let G be non empty join-commutative join-associative Robbins ComplLLattStr ; ::_thesis: for x being Element of G holds (x _3) + x = x _4 let x be Element of G; ::_thesis: (x _3) + x = x _4 thus (x _3) + x = (x _0) + (((Double x) + x) + x) by LATTICES:def_5 .= x _4 by LATTICES:def_5 ; ::_thesis: verum end; theorem Th45: :: ROBBINS1:45 for G being non empty join-commutative join-associative Robbins ComplLLattStr for x being Element of G holds \delta ((x _3),(x _0)) = x proof let G be non empty join-commutative join-associative Robbins ComplLLattStr ; ::_thesis: for x being Element of G holds \delta ((x _3),(x _0)) = x let x be Element of G; ::_thesis: \delta ((x _3),(x _0)) = x thus x = Expand ((x _2),x) by Th36 .= \delta ((x + (x _2)),(x _0)) by Th41 .= \delta ((x _3),(x _0)) by LATTICES:def_5 ; ::_thesis: verum end; theorem :: ROBBINS1:46 for G being non empty join-commutative join-associative Robbins ComplLLattStr for x, y, z being Element of G st - x = - y holds \delta (x,z) = \delta (y,z) ; theorem Th47: :: ROBBINS1:47 for G being non empty join-commutative join-associative Robbins ComplLLattStr for x, y being Element of G holds \delta (x,(- y)) = \delta (y,(- x)) proof let G be non empty join-commutative join-associative Robbins ComplLLattStr ; ::_thesis: for x, y being Element of G holds \delta (x,(- y)) = \delta (y,(- x)) let x, y be Element of G; ::_thesis: \delta (x,(- y)) = \delta (y,(- x)) thus \delta (x,(- y)) = - ((- x) + (- y)) .= \delta (y,(- x)) ; ::_thesis: verum end; theorem Th48: :: ROBBINS1:48 for G being non empty join-commutative join-associative Robbins ComplLLattStr for x being Element of G holds \delta ((x _3),x) = x _0 proof let G be non empty join-commutative join-associative Robbins ComplLLattStr ; ::_thesis: for x being Element of G holds \delta ((x _3),x) = x _0 let x be Element of G; ::_thesis: \delta ((x _3),x) = x _0 set alpha = ((- (x _3)) + (x _1)) + (- (Double x)); x = Expand (((- (x _3)) + (x _0)),x) by Th36 .= \delta (((- (x _3)) + (x _1)),(- ((\delta ((x _3),(x _0))) + x))) by LATTICES:def_5 .= \delta (((- (x _3)) + (x _1)),(- (Double x))) by Th45 ; then A1: - (Double x) = \delta ((((- (x _3)) + (x _1)) + (- (Double x))),x) by Th36; A2: x = \delta ((Double x),(x _0)) by Th40 .= \delta (((- (((- (x _3)) + (x _1)) + (- (Double x)))) + x),(x _0)) by A1 ; - (x _3) = Expand (((x _1) + (- (Double x))),(- (x _3))) by Th36 .= \delta ((((- (x _3)) + (x _1)) + (- (Double x))),(\delta (((x _1) + (- (Double x))),(- (x _3))))) by LATTICES:def_5 .= \delta ((((- (x _3)) + (x _1)) + (- (Double x))),(\delta (((x _0) + (x + (Double x))),(\delta ((Double x),(x _1)))))) by Th47 .= \delta ((((- (x _3)) + (x _1)) + (- (Double x))),(\delta (((Double x) + (x _1)),(\delta ((Double x),(x _1)))))) by LATTICES:def_5 .= - ((- (((- (x _3)) + (x _1)) + (- (Double x)))) + (x _1)) by Th36 ; hence \delta ((x _3),x) = \delta (((- (((- (x _3)) + (x _1)) + (- (Double x)))) + ((x _0) + x)),x) .= Expand (((- (((- (x _3)) + (x _1)) + (- (Double x)))) + x),(x _0)) by A2, LATTICES:def_5 .= x _0 by Th36 ; ::_thesis: verum end; theorem Th49: :: ROBBINS1:49 for G being non empty join-commutative join-associative Robbins ComplLLattStr for x being Element of G holds \delta (((x _1) + (x _3)),x) = x _0 proof let G be non empty join-commutative join-associative Robbins ComplLLattStr ; ::_thesis: for x being Element of G holds \delta (((x _1) + (x _3)),x) = x _0 let x be Element of G; ::_thesis: \delta (((x _1) + (x _3)),x) = x _0 x _0 = Expand ((x _4),(x _0)) by Th36 .= \delta (((x _4) + (x _0)),(\delta ((x _4),(\delta ((x _3),x))))) by Th48 .= \delta (((x _3) + (x _1)),(\delta ((x _4),(\delta ((x _3),x))))) by Th42 .= \delta (((x _3) + (x _1)),(Expand ((x _3),x))) by Th44 .= \delta (((x _3) + (x _1)),x) by Th36 ; hence \delta (((x _1) + (x _3)),x) = x _0 ; ::_thesis: verum end; theorem Th50: :: ROBBINS1:50 for G being non empty join-commutative join-associative Robbins ComplLLattStr for x being Element of G holds \delta (((x _1) + (x _2)),x) = x _0 proof let G be non empty join-commutative join-associative Robbins ComplLLattStr ; ::_thesis: for x being Element of G holds \delta (((x _1) + (x _2)),x) = x _0 let x be Element of G; ::_thesis: \delta (((x _1) + (x _2)),x) = x _0 thus x _0 = Expand ((x _3),(x _0)) by Th36 .= \delta (((x _1) + (x _2)),(\delta ((x _3),(x _0)))) by Th43 .= \delta (((x _1) + (x _2)),x) by Th45 ; ::_thesis: verum end; theorem Th51: :: ROBBINS1:51 for G being non empty join-commutative join-associative Robbins ComplLLattStr for x being Element of G holds \delta (((x _1) + (x _3)),(x _0)) = x proof let G be non empty join-commutative join-associative Robbins ComplLLattStr ; ::_thesis: for x being Element of G holds \delta (((x _1) + (x _3)),(x _0)) = x let x be Element of G; ::_thesis: \delta (((x _1) + (x _3)),(x _0)) = x thus x = Expand (((x _1) + (x _2)),x) by Th36 .= \delta (((x _1) + ((x _2) + x)),(\delta (((x _1) + (x _2)),x))) by LATTICES:def_5 .= \delta (((x _1) + (x _3)),(\delta (((x _1) + (x _2)),x))) by LATTICES:def_5 .= \delta (((x _1) + (x _3)),(x _0)) by Th50 ; ::_thesis: verum end; definition let G be non empty join-commutative join-associative Robbins ComplLLattStr ; let x be Element of G; func \beta x -> Element of G equals :: ROBBINS1:def 22 ((- ((x _1) + (x _3))) + x) + (- (x _3)); coherence ((- ((x _1) + (x _3))) + x) + (- (x _3)) is Element of G ; end; :: deftheorem defines \beta ROBBINS1:def_22_:_ for G being non empty join-commutative join-associative Robbins ComplLLattStr for x being Element of G holds \beta x = ((- ((x _1) + (x _3))) + x) + (- (x _3)); theorem Th52: :: ROBBINS1:52 for G being non empty join-commutative join-associative Robbins ComplLLattStr for x being Element of G holds \delta ((\beta x),x) = - (x _3) proof let G be non empty join-commutative join-associative Robbins ComplLLattStr ; ::_thesis: for x being Element of G holds \delta ((\beta x),x) = - (x _3) let x be Element of G; ::_thesis: \delta ((\beta x),x) = - (x _3) thus - (x _3) = \delta ((\beta x),(\delta (((- ((x _1) + (x _3))) + x),(- (x _3))))) by Th36 .= \delta ((\beta x),(\delta ((x _3),(\delta (((x _1) + (x _3)),x))))) by Th47 .= \delta ((\beta x),(\delta ((x _3),(x _0)))) by Th49 .= \delta ((\beta x),x) by Th45 ; ::_thesis: verum end; theorem Th53: :: ROBBINS1:53 for G being non empty join-commutative join-associative Robbins ComplLLattStr for x being Element of G holds \delta ((\beta x),x) = - ((x _1) + (x _3)) proof let G be non empty join-commutative join-associative Robbins ComplLLattStr ; ::_thesis: for x being Element of G holds \delta ((\beta x),x) = - ((x _1) + (x _3)) let x be Element of G; ::_thesis: \delta ((\beta x),x) = - ((x _1) + (x _3)) thus - ((x _1) + (x _3)) = \delta (((- ((x _1) + (x _3))) + (x + (- (x _3)))),(\delta ((x + (- (x _3))),(- ((x _1) + (x _3)))))) by Th36 .= \delta ((\beta x),(\delta ((x + (- (x _3))),(- ((x _1) + (x _3)))))) by LATTICES:def_5 .= \delta ((\beta x),(\delta (((x _1) + (x _3)),(\delta ((x _3),x))))) by Th47 .= \delta ((\beta x),(\delta (((x _1) + (x _3)),(x _0)))) by Th48 .= \delta ((\beta x),x) by Th51 ; ::_thesis: verum end; theorem :: ROBBINS1:54 for G being non empty join-commutative join-associative Robbins ComplLLattStr ex y, z being Element of G st - (y + z) = - z proof let G be non empty join-commutative join-associative Robbins ComplLLattStr ; ::_thesis: ex y, z being Element of G st - (y + z) = - z set x = the Element of G; take y = the Element of G _1 ; ::_thesis: ex z being Element of G st - (y + z) = - z take z = the Element of G _3 ; ::_thesis: - (y + z) = - z - (y + z) = \delta ((\beta the Element of G), the Element of G) by Th53 .= - z by Th52 ; hence - (y + z) = - z ; ::_thesis: verum end; begin theorem :: ROBBINS1:55 for G being non empty join-commutative join-associative Robbins ComplLLattStr st ( for z being Element of G holds - (- z) = z ) holds G is Huntington proof let G be non empty join-commutative join-associative Robbins ComplLLattStr ; ::_thesis: ( ( for z being Element of G holds - (- z) = z ) implies G is Huntington ) assume A1: for z being Element of G holds - (- z) = z ; ::_thesis: G is Huntington let x be Element of G; :: according to ROBBINS1:def_12 ::_thesis: for y being Element of G holds (- ((- x) + (- y))) + (- (x + (- y))) = y let y be Element of G; ::_thesis: (- ((- x) + (- y))) + (- (x + (- y))) = y A2: - (- ((- ((- x) + (- y))) + (- (x + (- y))))) = - (- y) by Def5; (- ((- x) + (- y))) + (- (x + (- y))) = - (- ((- ((- x) + (- y))) + (- (x + (- y))))) by A1 .= y by A1, A2 ; hence (- ((- x) + (- y))) + (- (x + (- y))) = y ; ::_thesis: verum end; theorem Th56: :: ROBBINS1:56 for G being non empty join-commutative join-associative Robbins ComplLLattStr st G is with_idempotent_element holds G is Huntington proof let G be non empty join-commutative join-associative Robbins ComplLLattStr ; ::_thesis: ( G is with_idempotent_element implies G is Huntington ) assume G is with_idempotent_element ; ::_thesis: G is Huntington then consider C being Element of G such that A1: C + C = C by Def13; A2: now__::_thesis:_for_x_being_Element_of_G_holds_C_+_x_=_-_((-_((C_+_(-_C))_+_x))_+_(-_(C_+_x))) let x be Element of G; ::_thesis: C + x = - ((- ((C + (- C)) + x)) + (- (C + x))) thus C + x = - ((- ((- C) + (C + x))) + (- (C + (C + x)))) by Def5 .= - ((- (((- C) + C) + x)) + (- (C + (C + x)))) by LATTICES:def_5 .= - ((- ((C + (- C)) + x)) + (- (C + x))) by A1, LATTICES:def_5 ; ::_thesis: verum end; assume not G is Huntington ; ::_thesis: contradiction then consider B, A being Element of G such that A3: (- ((- B) + (- A))) + (- (B + (- A))) <> A by Def12; set D = (C + (- C)) + (- C); A4: C = - ((- C) + (- (C + (- C)))) by A1, Def5; then A5: - (C + (- ((C + (- C)) + (- C)))) = - C by Def5; then - ((- C) + (- ((C + (- C)) + (- C)))) = - ((- ((- ((C + (- C)) + (- C))) + C)) + (- ((C + C) + ((- C) + (- C))))) by A1, LATTICES:def_5 .= - ((- ((- ((C + (- C)) + (- C))) + C)) + (- (C + (C + ((- C) + (- C)))))) by LATTICES:def_5 .= - ((- ((- ((C + (- C)) + (- C))) + C)) + (- (((C + (- C)) + (- C)) + C))) by LATTICES:def_5 .= C by Def5 ; then A6: - (C + (- C)) = - ((C + (- C)) + (- C)) by A5, Def5; C = - ((- (C + C)) + (- (((- C) + (- (C + (- C)))) + C))) by A4, Def5 .= - ((- C) + (- ((C + (- C)) + (- (C + (- C)))))) by A1, LATTICES:def_5 ; then A7: C = C + (- (C + (- C))) by A2, A5, A6; A8: now__::_thesis:_for_x_being_Element_of_G_holds_x_=_(-_(C_+_(-_C)))_+_x let x be Element of G; ::_thesis: x = (- (C + (- C))) + x thus x = - ((- ((C + (- (C + (- C)))) + x)) + (- (((- C) + (- (C + (- C)))) + x))) by A4, A7, Def5 .= - ((- (C + ((- (C + (- C))) + x))) + (- (((- C) + (- (C + (- C)))) + x))) by LATTICES:def_5 .= - ((- (C + ((- (C + (- C))) + x))) + (- ((- C) + ((- (C + (- C))) + x)))) by LATTICES:def_5 .= (- (C + (- C))) + x by Def5 ; ::_thesis: verum end; A9: now__::_thesis:_for_x_being_Element_of_G_holds_-_(C_+_(-_C))_=_-_((-_(-_x))_+_(-_x)) let x be Element of G; ::_thesis: - (C + (- C)) = - ((- (- x)) + (- x)) thus - (C + (- C)) = - ((- ((- x) + (- (C + (- C))))) + (- (x + (- (C + (- C)))))) by Def5 .= - ((- (- x)) + (- (x + (- (C + (- C)))))) by A8 .= - ((- (- x)) + (- x)) by A8 ; ::_thesis: verum end; A10: now__::_thesis:_for_x_being_Element_of_G_holds_-_(-_x)_=_-_(-_(x_+_(-_(-_x)))) let x be Element of G; ::_thesis: - (- x) = - (- (x + (- (- x)))) thus - (- x) = - ((- ((- x) + (- (- x)))) + (- (x + (- (- x))))) by Def5 .= - ((- (C + (- C))) + (- (x + (- (- x))))) by A9 .= - (- (x + (- (- x)))) by A8 ; ::_thesis: verum end; A11: now__::_thesis:_for_x_being_Element_of_G_holds_-_x_=_-_(-_(-_x)) let x be Element of G; ::_thesis: - x = - (- (- x)) thus - x = - ((- ((- (- (- x))) + (- x))) + (- ((- (- x)) + (- x)))) by Def5 .= - ((- ((- (- (- x))) + (- x))) + (- (C + (- C)))) by A9 .= - (- ((- (- (- x))) + (- x))) by A8 .= - (- (- x)) by A10 ; ::_thesis: verum end; A12: now__::_thesis:_for_x,_y_being_Element_of_G_holds_y_=_-_(-_y) let x, y be Element of G; ::_thesis: y = - (- y) thus y = - ((- ((- x) + y)) + (- (x + y))) by Def5 .= - (- (- ((- ((- x) + y)) + (- (x + y))))) by A11 .= - (- y) by Def5 ; ::_thesis: verum end; now__::_thesis:_for_x,_y_being_Element_of_G_holds_(-_((-_x)_+_y))_+_(-_(x_+_y))_=_-_y let x, y be Element of G; ::_thesis: (- ((- x) + y)) + (- (x + y)) = - y thus (- ((- x) + y)) + (- (x + y)) = - (- ((- ((- x) + y)) + (- (x + y)))) by A12 .= - y by Def5 ; ::_thesis: verum end; then (- ((- B) + (- A))) + (- (B + (- A))) = - (- A) .= A by A12 ; hence contradiction by A3; ::_thesis: verum end; registration cluster TrivComplLat -> strict with_idempotent_element ; coherence TrivComplLat is with_idempotent_element proof set x = the Element of TrivComplLat; take the Element of TrivComplLat ; :: according to ROBBINS1:def_13 ::_thesis: the Element of TrivComplLat + the Element of TrivComplLat = the Element of TrivComplLat thus the Element of TrivComplLat = the Element of TrivComplLat + the Element of TrivComplLat by STRUCT_0:def_10; ::_thesis: verum end; end; registration cluster non empty join-commutative join-associative Robbins with_idempotent_element -> non empty join-commutative join-associative Robbins Huntington for ComplLLattStr ; coherence for b1 being non empty join-commutative join-associative Robbins ComplLLattStr st b1 is with_idempotent_element holds b1 is Huntington by Th56; end; theorem Th57: :: ROBBINS1:57 for G being non empty join-commutative join-associative Robbins ComplLLattStr st ex c, d being Element of G st c + d = c holds G is Huntington proof let G be non empty join-commutative join-associative Robbins ComplLLattStr ; ::_thesis: ( ex c, d being Element of G st c + d = c implies G is Huntington ) A1: now__::_thesis:_for_x,_y,_z_being_Element_of_G_holds_-_((-_(((-_((-_x)_+_y))_+_x)_+_y))_+_y)_=_-_((-_x)_+_y) let x, y, z be Element of G; ::_thesis: - ((- (((- ((- x) + y)) + x) + y)) + y) = - ((- x) + y) set k = - ((- x) + y); thus - ((- (((- ((- x) + y)) + x) + y)) + y) = - ((- (((- ((- x) + y)) + x) + y)) + (- ((- ((- x) + y)) + (- (x + y))))) by Def5 .= - ((- ((- ((- x) + y)) + (x + y))) + (- ((- ((- x) + y)) + (- (x + y))))) by LATTICES:def_5 .= - ((- x) + y) by Def5 ; ::_thesis: verum end; A2: now__::_thesis:_for_x,_y,_z_being_Element_of_G_holds_z_=_-_((-_(((-_(((-_((-_x)_+_y))_+_x)_+_y))_+_y)_+_z))_+_(-_((-_((-_x)_+_y))_+_z))) let x, y, z be Element of G; ::_thesis: z = - ((- (((- (((- ((- x) + y)) + x) + y)) + y) + z)) + (- ((- ((- x) + y)) + z))) set k = - ((- x) + y); - ((- (((- ((- x) + y)) + x) + y)) + y) = - ((- x) + y) by A1; hence z = - ((- (((- (((- ((- x) + y)) + x) + y)) + y) + z)) + (- ((- ((- x) + y)) + z))) by Def5; ::_thesis: verum end; given C, D being Element of G such that A3: C + D = C ; ::_thesis: G is Huntington A4: now__::_thesis:_for_x,_y,_z_being_Element_of_G_holds_-_((-_(((-_((-_x)_+_y))_+_(-_(x_+_y)))_+_z))_+_(-_(y_+_z)))_=_z let x, y, z be Element of G; ::_thesis: - ((- (((- ((- x) + y)) + (- (x + y))) + z)) + (- (y + z))) = z set k = (- ((- x) + y)) + (- (x + y)); thus - ((- (((- ((- x) + y)) + (- (x + y))) + z)) + (- (y + z))) = - ((- (((- ((- x) + y)) + (- (x + y))) + z)) + (- ((- ((- ((- x) + y)) + (- (x + y)))) + z))) by Def5 .= z by Def5 ; ::_thesis: verum end; A5: now__::_thesis:_for_x_being_Element_of_G_holds_D_=_-_((-_C)_+_(-_((D_+_(-_(C_+_(-_x))))_+_(-_(C_+_x))))) let x be Element of G; ::_thesis: D = - ((- C) + (- ((D + (- (C + (- x)))) + (- (C + x))))) thus D = - ((- (((- ((- x) + C)) + (- (x + C))) + D)) + (- (C + D))) by A4 .= - ((- C) + (- ((D + (- (C + (- x)))) + (- (C + x))))) by A3, LATTICES:def_5 ; ::_thesis: verum end; set e = - (C + (- C)); set K = - ((C + C) + (- (C + (- C)))); A6: - ((C + C) + (- (C + (- C)))) = - ((C + (- (C + (- C)))) + C) by LATTICES:def_5; A7: now__::_thesis:_for_x,_y_being_Element_of_G_holds_-_((-_((D_+_(-_(C_+_x)))_+_y))_+_(-_((C_+_x)_+_y)))_=_D_+_y let x, y be Element of G; ::_thesis: - ((- ((D + (- (C + x))) + y)) + (- ((C + x) + y))) = D + y thus - ((- ((D + (- (C + x))) + y)) + (- ((C + x) + y))) = - ((- ((- (C + x)) + (D + y))) + (- (((C + D) + x) + y))) by A3, LATTICES:def_5 .= - ((- ((- (C + x)) + (D + y))) + (- (((C + x) + D) + y))) by LATTICES:def_5 .= - ((- ((- (C + x)) + (D + y))) + (- ((C + x) + (D + y)))) by LATTICES:def_5 .= D + y by Def5 ; ::_thesis: verum end; set L = - (D + (- C)); set E = D + (- C); A8: - ((- C) + (- (D + (- C)))) = D by A3, Def5; then A9: - (D + (- (C + (- (D + (- C)))))) = - (D + (- C)) by Def5; - ((- (D + (- C))) + (- (C + (- (D + (- C)))))) = - ((- (D + (- (C + (- (D + (- C))))))) + (- ((D + C) + (- (D + (- C)))))) by A3, A8, Def5 .= - ((- (D + (- (C + (- (D + (- C))))))) + (- (D + (C + (- (D + (- C))))))) by LATTICES:def_5 .= D by Def5 ; then - (D + (- ((D + (- C)) + (- (C + (- (D + (- C)))))))) = - (C + (- (D + (- C)))) by Def5; then A10: - (C + (- (D + (- C)))) = - (D + (- ((D + (- (C + (- (D + (- C)))))) + (- C)))) by LATTICES:def_5 .= - C by A8, A9, Def5 ; set L = C + (- (D + (- C))); A11: C = - ((- ((D + (- (C + (- (D + (- C)))))) + C)) + (- ((- (D + (- C))) + C))) by A9, Def5 .= - ((- (C + (- (D + (- C))))) + (- (C + (- (C + (- (D + (- C)))))))) by A3, LATTICES:def_5 ; then - (C + (- (C + (- (C + (- C)))))) = - (C + (- C)) by A10, Def5; then C = - ((- (C + (- C))) + (- ((C + C) + (- (C + (- C)))))) by A6, Def5; then - (C + (- ((C + (- C)) + (- ((C + C) + (- (C + (- C)))))))) = - ((C + C) + (- (C + (- C)))) by Def5; then - ((C + C) + (- (C + (- C)))) = - ((- (((- ((C + C) + (- (C + (- C))))) + C) + (- C))) + C) by LATTICES:def_5 .= - ((- (((- (((- (C + (- C))) + C) + C)) + C) + (- C))) + C) by LATTICES:def_5 .= - C by A11, A2, A10 ; then D + (- (C + (- C))) = - ((- ((D + (- (C + C))) + (- (C + (- C))))) + (- C)) by A7 .= - ((- C) + (- ((D + (- (C + (- C)))) + (- (C + C))))) by LATTICES:def_5 .= D by A5 ; then A12: C + (- (C + (- C))) = C by A3, LATTICES:def_5; now__::_thesis:_for_x_being_Element_of_G_holds_x_=_(-_(C_+_(-_C)))_+_x let x be Element of G; ::_thesis: x = (- (C + (- C))) + x thus x = - ((- ((C + (- (C + (- C)))) + x)) + (- (((- C) + (- (C + (- C)))) + x))) by A11, A10, A12, Def5 .= - ((- (C + ((- (C + (- C))) + x))) + (- (((- C) + (- (C + (- C)))) + x))) by LATTICES:def_5 .= - ((- (C + ((- (C + (- C))) + x))) + (- ((- C) + ((- (C + (- C))) + x)))) by LATTICES:def_5 .= (- (C + (- C))) + x by Def5 ; ::_thesis: verum end; then - (C + (- C)) = (- (C + (- C))) + (- (C + (- C))) ; then G is with_idempotent_element by Def13; hence G is Huntington ; ::_thesis: verum end; theorem Th58: :: ROBBINS1:58 for G being non empty join-commutative join-associative Robbins ComplLLattStr ex y, z being Element of G st y + z = z proof let G be non empty join-commutative join-associative Robbins ComplLLattStr ; ::_thesis: ex y, z being Element of G st y + z = z A1: now__::_thesis:_for_x,_y_being_Element_of_G_holds_-_(x_+_y)_=_-_((-_(((-_(x_+_y))_+_(-_x))_+_y))_+_y) let x, y be Element of G; ::_thesis: - (x + y) = - ((- (((- (x + y)) + (- x)) + y)) + y) thus - (x + y) = - ((- ((- ((- x) + y)) + (- (x + y)))) + (- (((- x) + y) + (- (x + y))))) by Def5 .= - (y + (- (((- x) + y) + (- (x + y))))) by Def5 .= - ((- (((- (x + y)) + (- x)) + y)) + y) by LATTICES:def_5 ; ::_thesis: verum end; A2: now__::_thesis:_for_x,_y_being_Element_of_G_holds_-_((-_x)_+_y)_=_-_((-_(((-_((-_x)_+_y))_+_x)_+_y))_+_y) let x, y be Element of G; ::_thesis: - ((- x) + y) = - ((- (((- ((- x) + y)) + x) + y)) + y) thus - ((- x) + y) = - ((- ((- (x + y)) + (- ((- x) + y)))) + (- ((x + y) + (- ((- x) + y))))) by Def5 .= - (y + (- ((x + y) + (- ((- x) + y))))) by Def5 .= - ((- (((- ((- x) + y)) + x) + y)) + y) by LATTICES:def_5 ; ::_thesis: verum end; A3: now__::_thesis:_for_x,_y_being_Element_of_G_holds_y_=_-_((-_(((-_((-_x)_+_y))_+_x)_+_(Double_y)))_+_(-_((-_x)_+_y))) let x, y be Element of G; ::_thesis: y = - ((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) thus y = - ((- ((- (((- ((- x) + y)) + x) + y)) + y)) + (- ((((- ((- x) + y)) + x) + y) + y))) by Def5 .= - ((- ((- x) + y)) + (- ((((- ((- x) + y)) + x) + y) + y))) by A2 .= - ((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) by LATTICES:def_5 ; ::_thesis: verum end; A4: now__::_thesis:_for_x,_y,_z_being_Element_of_G_holds_z_=_-_((-_(((-_(((-_((-_x)_+_y))_+_x)_+_(Double_y)))_+_(-_((-_x)_+_y)))_+_z))_+_(-_(y_+_z))) let x, y, z be Element of G; ::_thesis: z = - ((- (((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) + z)) + (- (y + z))) thus z = - ((- ((- ((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y)))) + z)) + (- (((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) + z))) by Def5 .= - ((- (((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) + z)) + (- (y + z))) by A3 ; ::_thesis: verum end; A5: now__::_thesis:_for_x,_y,_z_being_Element_of_G_holds_-_(y_+_z)_=_-_((-_((((-_(((-_((-_x)_+_y))_+_x)_+_(Double_y)))_+_(-_((-_x)_+_y)))_+_(-_(y_+_z)))_+_z))_+_z) let x, y, z be Element of G; ::_thesis: - (y + z) = - ((- ((((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) + (- (y + z))) + z)) + z) set k = ((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) + z; thus - (y + z) = - ((- ((- (((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) + z)) + (- (y + z)))) + (- ((((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) + z) + (- (y + z))))) by Def5 .= - (z + (- ((((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) + z) + (- (y + z))))) by A4 .= - ((- ((((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) + (- (y + z))) + z)) + z) by LATTICES:def_5 ; ::_thesis: verum end; A6: now__::_thesis:_for_x,_y,_z,_u_being_Element_of_G_holds_u_=_-_((-_((-_(y_+_z))_+_u))_+_(-_(((-_((((-_(((-_((-_x)_+_y))_+_x)_+_(Double_y)))_+_(-_((-_x)_+_y)))_+_(-_(y_+_z)))_+_z))_+_z)_+_u))) let x, y, z, u be Element of G; ::_thesis: u = - ((- ((- (y + z)) + u)) + (- (((- ((((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) + (- (y + z))) + z)) + z) + u))) set k = (- ((((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) + (- (y + z))) + z)) + z; thus u = - ((- ((- ((- ((((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) + (- (y + z))) + z)) + z)) + u)) + (- (((- ((((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) + (- (y + z))) + z)) + z) + u))) by Def5 .= - ((- ((- (y + z)) + u)) + (- (((- ((((- (((- ((- x) + y)) + x) + (Double y))) + (- ((- x) + y))) + (- (y + z))) + z)) + z) + u))) by A5 ; ::_thesis: verum end; A7: now__::_thesis:_for_x,_y,_z,_v_being_Element_of_G_holds_-_((-_((Double_v)_+_v))_+_v)_=_-_((-_((-_((Double_v)_+_v))_+_(-_((-_((Double_v)_+_v))_+_v))))_+_(-_((((Double_v)_+_(Double_v))_+_v)_+_(-_((-_((Double_v)_+_v))_+_v))))) let x, y, z, v be Element of G; ::_thesis: - ((- ((Double v) + v)) + v) = - ((- ((- ((Double v) + v)) + (- ((- ((Double v) + v)) + v)))) + (- ((((Double v) + (Double v)) + v) + (- ((- ((Double v) + v)) + v))))) set k = - ((- ((Double v) + v)) + v); set l = (- ((- ((Double v) + v)) + v)) + (Double v); set v5 = ((Double v) + (Double v)) + v; A8: - (((Double v) + v) + ((- ((- ((Double v) + v)) + v)) + (Double v))) = - ((- (((- (((Double v) + v) + ((- ((- ((Double v) + v)) + v)) + (Double v)))) + (- ((Double v) + v))) + ((- ((- ((Double v) + v)) + v)) + (Double v)))) + ((- ((- ((Double v) + v)) + v)) + (Double v))) by A1 .= - ((- (((- (((Double v) + v) + ((- ((- ((Double v) + v)) + v)) + (Double v)))) + ((- ((- ((Double v) + v)) + v)) + (Double v))) + (- ((Double v) + v)))) + ((- ((- ((Double v) + v)) + v)) + (Double v))) by LATTICES:def_5 ; thus - ((- ((Double v) + v)) + v) = - ((- ((- (v + (Double v))) + (- ((- ((Double v) + v)) + v)))) + (- (((- ((((- (((- ((- ((Double v) + v)) + v)) + ((Double v) + v)) + (Double v))) + (- ((- ((Double v) + v)) + v))) + (- (v + (Double v)))) + (Double v))) + (Double v)) + (- ((- ((Double v) + v)) + v))))) by A6 .= - ((- ((- (v + (Double v))) + (- ((- ((Double v) + v)) + v)))) + (- (((- ((((- ((((Double v) + v) + (- ((- ((Double v) + v)) + v))) + (Double v))) + (- ((- ((Double v) + v)) + v))) + (Double v)) + (- (v + (Double v))))) + (Double v)) + (- ((- ((Double v) + v)) + v))))) by LATTICES:def_5 .= - ((- ((- (v + (Double v))) + (- ((- ((Double v) + v)) + v)))) + (- (((- (((- ((((Double v) + v) + (- ((- ((Double v) + v)) + v))) + (Double v))) + ((- ((- ((Double v) + v)) + v)) + (Double v))) + (- (v + (Double v))))) + (Double v)) + (- ((- ((Double v) + v)) + v))))) by LATTICES:def_5 .= - ((- ((- (v + (Double v))) + (- ((- ((Double v) + v)) + v)))) + (- (((- (((- (((Double v) + v) + ((- ((- ((Double v) + v)) + v)) + (Double v)))) + ((- ((- ((Double v) + v)) + v)) + (Double v))) + (- (v + (Double v))))) + (Double v)) + (- ((- ((Double v) + v)) + v))))) by LATTICES:def_5 .= - ((- ((- (v + (Double v))) + (- ((- ((Double v) + v)) + v)))) + (- ((- (((- (((Double v) + v) + ((- ((- ((Double v) + v)) + v)) + (Double v)))) + ((- ((- ((Double v) + v)) + v)) + (Double v))) + (- (v + (Double v))))) + ((- ((- ((Double v) + v)) + v)) + (Double v))))) by LATTICES:def_5 .= - ((- ((- ((Double v) + v)) + (- ((- ((Double v) + v)) + v)))) + (- ((((Double v) + v) + (Double v)) + (- ((- ((Double v) + v)) + v))))) by A8, LATTICES:def_5 .= - ((- ((- ((Double v) + v)) + (- ((- ((Double v) + v)) + v)))) + (- ((((Double v) + (Double v)) + v) + (- ((- ((Double v) + v)) + v))))) by LATTICES:def_5 ; ::_thesis: verum end; A9: now__::_thesis:_for_x_being_Element_of_G_holds_-_((-_((-_((Double_x)_+_x))_+_x))_+_(((Double_x)_+_(Double_x))_+_x))_=_-_((Double_x)_+_x) let x be Element of G; ::_thesis: - ((- ((- ((Double x) + x)) + x)) + (((Double x) + (Double x)) + x)) = - ((Double x) + x) set k = (- ((- ((Double x) + x)) + x)) + (- ((Double x) + x)); set l = - ((- ((- ((Double x) + x)) + x)) + (((Double x) + (Double x)) + x)); A10: - ((Double x) + x) = - ((- (((- (((- ((- ((Double x) + x)) + x)) + ((Double x) + x)) + (Double x))) + (- ((- ((Double x) + x)) + x))) + (- ((Double x) + x)))) + (- (x + (- ((Double x) + x))))) by A4 .= - ((- ((- (((- ((- ((Double x) + x)) + x)) + ((Double x) + x)) + (Double x))) + ((- ((- ((Double x) + x)) + x)) + (- ((Double x) + x))))) + (- (x + (- ((Double x) + x))))) by LATTICES:def_5 .= - ((- ((- ((- ((- ((Double x) + x)) + x)) + (((Double x) + x) + (Double x)))) + ((- ((- ((Double x) + x)) + x)) + (- ((Double x) + x))))) + (- (x + (- ((Double x) + x))))) by LATTICES:def_5 .= - ((- ((- ((- ((- ((Double x) + x)) + x)) + (((Double x) + (Double x)) + x))) + ((- ((- ((Double x) + x)) + x)) + (- ((Double x) + x))))) + (- (x + (- ((Double x) + x))))) by LATTICES:def_5 ; - ((- ((- ((Double x) + x)) + x)) + (((Double x) + (Double x)) + x)) = - ((- ((- ((- ((- ((Double x) + x)) + x)) + (- ((Double x) + x)))) + (- ((- ((- ((Double x) + x)) + x)) + (((Double x) + (Double x)) + x))))) + (- (((- ((- ((Double x) + x)) + x)) + (- ((Double x) + x))) + (- ((- ((- ((Double x) + x)) + x)) + (((Double x) + (Double x)) + x)))))) by Def5 .= - ((- ((- ((Double x) + x)) + x)) + (- (((- ((- ((Double x) + x)) + x)) + (- ((Double x) + x))) + (- ((- ((- ((Double x) + x)) + x)) + (((Double x) + (Double x)) + x)))))) by A7 ; hence - ((- ((- ((Double x) + x)) + x)) + (((Double x) + (Double x)) + x)) = - ((Double x) + x) by A10; ::_thesis: verum end; A11: now__::_thesis:_for_x_being_Element_of_G_holds_x_=_-_((-_((-_((Double_x)_+_x))_+_x))_+_(-_((Double_x)_+_x))) let x be Element of G; ::_thesis: x = - ((- ((- ((Double x) + x)) + x)) + (- ((Double x) + x))) A12: - ((- ((Double x) + x)) + x) = - ((- (((- ((- ((Double x) + x)) + x)) + ((Double x) + x)) + x)) + x) by A2 .= - ((- ((- ((- ((Double x) + x)) + x)) + (((Double x) + x) + x))) + x) by LATTICES:def_5 .= - ((- ((- ((- ((Double x) + x)) + x)) + ((Double x) + (Double x)))) + x) by LATTICES:def_5 ; thus x = - ((- ((- ((- ((- ((Double x) + x)) + x)) + ((Double x) + (Double x)))) + x)) + (- (((- ((- ((Double x) + x)) + x)) + ((Double x) + (Double x))) + x))) by Def5 .= - ((- ((- ((- ((- ((Double x) + x)) + x)) + ((Double x) + (Double x)))) + x)) + (- ((- ((- ((Double x) + x)) + x)) + (((Double x) + (Double x)) + x)))) by LATTICES:def_5 .= - ((- ((- ((Double x) + x)) + x)) + (- ((Double x) + x))) by A9, A12 ; ::_thesis: verum end; A13: now__::_thesis:_for_x,_y_being_Element_of_G_holds_y_=_-_((-_(((-_((-_((Double_x)_+_x))_+_x))_+_(-_((Double_x)_+_x)))_+_y))_+_(-_(x_+_y))) let x, y be Element of G; ::_thesis: y = - ((- (((- ((- ((Double x) + x)) + x)) + (- ((Double x) + x))) + y)) + (- (x + y))) thus y = - ((- ((- ((- ((- ((Double x) + x)) + x)) + (- ((Double x) + x)))) + y)) + (- (((- ((- ((Double x) + x)) + x)) + (- ((Double x) + x))) + y))) by Def5 .= - ((- (((- ((- ((Double x) + x)) + x)) + (- ((Double x) + x))) + y)) + (- (x + y))) by A11 ; ::_thesis: verum end; A14: now__::_thesis:_for_x_being_Element_of_G_holds_(-_((-_((Double_x)_+_x))_+_x))_+_(Double_x)_=_-_((-_(((-_((-_((Double_x)_+_x))_+_x))_+_(-_((Double_x)_+_x)))_+_(Double_x)))_+_(-_((Double_x)_+_x))) let x be Element of G; ::_thesis: (- ((- ((Double x) + x)) + x)) + (Double x) = - ((- (((- ((- ((Double x) + x)) + x)) + (- ((Double x) + x))) + (Double x))) + (- ((Double x) + x))) thus (- ((- ((Double x) + x)) + x)) + (Double x) = - ((- ((- ((Double x) + x)) + ((- ((- ((Double x) + x)) + x)) + (Double x)))) + (- (((Double x) + x) + ((- ((- ((Double x) + x)) + x)) + (Double x))))) by Def5 .= - ((- ((- ((Double x) + x)) + ((- ((- ((Double x) + x)) + x)) + (Double x)))) + (- ((- ((- ((Double x) + x)) + x)) + (((Double x) + x) + (Double x))))) by LATTICES:def_5 .= - ((- ((- ((Double x) + x)) + ((- ((- ((Double x) + x)) + x)) + (Double x)))) + (- ((- ((- ((Double x) + x)) + x)) + (((Double x) + (Double x)) + x)))) by LATTICES:def_5 .= - ((- ((- ((Double x) + x)) + ((- ((- ((Double x) + x)) + x)) + (Double x)))) + (- ((Double x) + x))) by A9 .= - ((- (((- ((- ((Double x) + x)) + x)) + (- ((Double x) + x))) + (Double x))) + (- ((Double x) + x))) by LATTICES:def_5 ; ::_thesis: verum end; A15: now__::_thesis:_for_x,_y_being_Element_of_G_holds_Double_x_=_(-_((-_((Double_x)_+_x))_+_x))_+_(Double_x) let x, y be Element of G; ::_thesis: Double x = (- ((- ((Double x) + x)) + x)) + (Double x) thus Double x = - ((- (((- ((- ((Double x) + x)) + x)) + (- ((Double x) + x))) + (Double x))) + (- (x + (Double x)))) by A13 .= (- ((- ((Double x) + x)) + x)) + (Double x) by A14 ; ::_thesis: verum end; set x = the Element of G; set c = Double the Element of G; set d = - ((- ((Double the Element of G) + the Element of G)) + the Element of G); take - ((- ((Double the Element of G) + the Element of G)) + the Element of G) ; ::_thesis: ex z being Element of G st (- ((- ((Double the Element of G) + the Element of G)) + the Element of G)) + z = z take Double the Element of G ; ::_thesis: (- ((- ((Double the Element of G) + the Element of G)) + the Element of G)) + (Double the Element of G) = Double the Element of G thus (- ((- ((Double the Element of G) + the Element of G)) + the Element of G)) + (Double the Element of G) = Double the Element of G by A15; ::_thesis: verum end; registration cluster non empty join-commutative join-associative Robbins -> non empty join-commutative join-associative Huntington for ComplLLattStr ; coherence for b1 being non empty join-commutative join-associative ComplLLattStr st b1 is Robbins holds b1 is Huntington proof let K be non empty join-commutative join-associative ComplLLattStr ; ::_thesis: ( K is Robbins implies K is Huntington ) assume A1: K is Robbins ; ::_thesis: K is Huntington then ex y, z being Element of K st y + z = z by Th58; hence K is Huntington by A1, Th57; ::_thesis: verum end; end; definition let L be non empty OrthoLattStr ; attrL is de_Morgan means :Def23: :: ROBBINS1:def 23 for x, y being Element of L holds x "/\" y = ((x `) "\/" (y `)) ` ; end; :: deftheorem Def23 defines de_Morgan ROBBINS1:def_23_:_ for L being non empty OrthoLattStr holds ( L is de_Morgan iff for x, y being Element of L holds x "/\" y = ((x `) "\/" (y `)) ` ); registration let L be non empty ComplLLattStr ; cluster CLatt L -> strict de_Morgan ; coherence CLatt L is de_Morgan proof let x, y be Element of (CLatt L); :: according to ROBBINS1:def_23 ::_thesis: x "/\" y = ((x `) "\/" (y `)) ` reconsider x9 = x, y9 = y as Element of L by Def11; ( x9 ` = x ` & y9 ` = y ` ) by Def11; then (x9 `) "\/" (y9 `) = (x `) "\/" (y `) by Def11; then ((x `) "\/" (y `)) ` = x9 *' y9 by Def11; hence x "/\" y = ((x `) "\/" (y `)) ` by Def11; ::_thesis: verum end; end; theorem Th59: :: ROBBINS1:59 for L being non empty join-commutative meet-commutative well-complemented OrthoLattStr for x being Element of L holds ( x + (x `) = Top L & x "/\" (x `) = Bottom L ) proof let L be non empty join-commutative meet-commutative well-complemented OrthoLattStr ; ::_thesis: for x being Element of L holds ( x + (x `) = Top L & x "/\" (x `) = Bottom L ) let x be Element of L; ::_thesis: ( x + (x `) = Top L & x "/\" (x `) = Bottom L ) A1: x ` is_a_complement_of x by Def10; hence x + (x `) = Top L by LATTICES:def_18; ::_thesis: x "/\" (x `) = Bottom L thus x "/\" (x `) = Bottom L by A1, LATTICES:def_18; ::_thesis: verum end; theorem Th60: :: ROBBINS1:60 for L being distributive bounded well-complemented preOrthoLattice holds (Top L) ` = Bottom L proof let L be distributive bounded well-complemented preOrthoLattice; ::_thesis: (Top L) ` = Bottom L set x = the Element of L; (Top L) ` = ((( the Element of L `) `) + ( the Element of L `)) ` by Th59 .= ( the Element of L `) "/\" the Element of L by Th33 .= Bottom L by Th59 ; hence (Top L) ` = Bottom L ; ::_thesis: verum end; registration cluster TrivOrtLat -> strict de_Morgan ; coherence TrivOrtLat is de_Morgan proof let x, y be Element of TrivOrtLat; :: according to ROBBINS1:def_23 ::_thesis: x "/\" y = ((x `) "\/" (y `)) ` thus x "/\" y = ((x `) "\/" (y `)) ` by STRUCT_0:def_10; ::_thesis: verum end; end; registration cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like Boolean strict Robbins Huntington de_Morgan for OrthoLattStr ; existence ex b1 being preOrthoLattice st ( b1 is strict & b1 is de_Morgan & b1 is Boolean & b1 is Robbins & b1 is Huntington ) proof take TrivOrtLat ; ::_thesis: ( TrivOrtLat is strict & TrivOrtLat is de_Morgan & TrivOrtLat is Boolean & TrivOrtLat is Robbins & TrivOrtLat is Huntington ) thus ( TrivOrtLat is strict & TrivOrtLat is de_Morgan & TrivOrtLat is Boolean & TrivOrtLat is Robbins & TrivOrtLat is Huntington ) ; ::_thesis: verum end; end; registration cluster non empty join-commutative join-associative de_Morgan -> non empty meet-commutative for OrthoLattStr ; coherence for b1 being non empty OrthoLattStr st b1 is join-associative & b1 is join-commutative & b1 is de_Morgan holds b1 is meet-commutative proof let L be non empty OrthoLattStr ; ::_thesis: ( L is join-associative & L is join-commutative & L is de_Morgan implies L is meet-commutative ) assume ( L is join-associative & L is join-commutative & L is de_Morgan ) ; ::_thesis: L is meet-commutative then reconsider L1 = L as non empty join-commutative join-associative de_Morgan OrthoLattStr ; let a, b be Element of L; :: according to LATTICES:def_6 ::_thesis: a "/\" b = b "/\" a reconsider a1 = a, b1 = b as Element of L1 ; thus a "/\" b = a1 *' b1 by Def23 .= b1 *' a1 .= b "/\" a by Def23 ; ::_thesis: verum end; end; theorem Th61: :: ROBBINS1:61 for L being Huntington de_Morgan preOrthoLattice holds Bot L = Bottom L proof let L be Huntington de_Morgan preOrthoLattice; ::_thesis: Bot L = Bottom L reconsider C = Bot L as Element of L ; A1: for a being Element of L holds ( C "/\" a = C & a "/\" C = C ) proof let a be Element of L; ::_thesis: ( C "/\" a = C & a "/\" C = C ) reconsider a9 = a as Element of L ; thus C "/\" a = (Bot L) *' a9 by Def23 .= C by Def9 ; ::_thesis: a "/\" C = C hence a "/\" C = C ; ::_thesis: verum end; then L is lower-bounded by LATTICES:def_13; hence Bot L = Bottom L by A1, LATTICES:def_16; ::_thesis: verum end; registration cluster non empty Lattice-like Boolean well-complemented -> Huntington well-complemented for OrthoLattStr ; coherence for b1 being well-complemented preOrthoLattice st b1 is Boolean holds b1 is Huntington proof let L be well-complemented preOrthoLattice; ::_thesis: ( L is Boolean implies L is Huntington ) assume A1: L is Boolean ; ::_thesis: L is Huntington then reconsider L9 = L as Boolean preOrthoLattice ; A2: for x being Element of L9 holds (Top L9) "/\" x = x ; now__::_thesis:_for_x,_y_being_Element_of_L_holds_(((x_`)_"\/"_(y_`))_`)_"\/"_(((x_`)_"\/"_y)_`)_=_x let x, y be Element of L; ::_thesis: (((x `) "\/" (y `)) `) "\/" (((x `) "\/" y) `) = x thus (((x `) "\/" (y `)) `) "\/" (((x `) "\/" y) `) = (x "/\" y) + (((x `) + y) `) by A1, Th33 .= (x + (((x `) + y) `)) "/\" (y + (((x `) + y) `)) by A1, LATTICES:11 .= (x + (((x `) + ((y `) `)) `)) "/\" (y + (((x `) + y) `)) by A1, Th32 .= (x + (x "/\" (y `))) "/\" (y + (((x `) + y) `)) by A1, Th33 .= x "/\" (y + (((x `) + y) `)) by LATTICES:def_8 .= x "/\" (y + (((x `) + ((y `) `)) `)) by A1, Th32 .= x "/\" (y + (x "/\" (y `))) by A1, Th33 .= x "/\" ((y + x) "/\" (y + (y `))) by A1, LATTICES:11 .= (x "/\" (y + x)) "/\" (y + (y `)) by LATTICES:def_7 .= x "/\" (y + (y `)) by LATTICES:def_9 .= x "/\" (Top L) by Th59 .= x by A2 ; ::_thesis: verum end; hence L is Huntington by Def6; ::_thesis: verum end; end; registration cluster non empty Lattice-like Huntington de_Morgan -> Boolean de_Morgan for OrthoLattStr ; coherence for b1 being de_Morgan preOrthoLattice st b1 is Huntington holds b1 is Boolean proof let L be de_Morgan preOrthoLattice; ::_thesis: ( L is Huntington implies L is Boolean ) assume A1: L is Huntington ; ::_thesis: L is Boolean then reconsider L9 = L as Huntington preOrthoLattice ; A2: L is lower-bounded proof set c9 = Bot L9; reconsider c = Bot L9 as Element of L ; take c ; :: according to LATTICES:def_13 ::_thesis: for b1 being M2( the carrier of L) holds ( c "/\" b1 = c & b1 "/\" c = c ) let a be Element of L; ::_thesis: ( c "/\" a = c & a "/\" c = c ) reconsider a9 = a as Element of L9 ; thus c "/\" a = (Bot L9) *' a9 by Def23 .= c by Def9 ; ::_thesis: a "/\" c = c thus a "/\" c = (Bot L9) *' a9 by Def23 .= c by Def9 ; ::_thesis: verum end; L9 is upper-bounded ; hence L is bounded by A2; :: according to LATTICES:def_20 ::_thesis: ( L is complemented & L is distributive ) thus L is complemented ::_thesis: L is distributive proof let b be Element of L; :: according to LATTICES:def_19 ::_thesis: ex b1 being M2( the carrier of L) st b1 is_a_complement_of b take a = b ` ; ::_thesis: a is_a_complement_of b A3: L9 is join-idempotent ; hence a + b = Top L by Def8; :: according to LATTICES:def_18 ::_thesis: ( b + a = Top L & a "/\" b = Bottom L & b "/\" a = Bottom L ) thus b + a = Top L by A3, Def8; ::_thesis: ( a "/\" b = Bottom L & b "/\" a = Bottom L ) thus a "/\" b = ((a `) + (b `)) ` by Def23 .= Bot L9 by Th8 .= Bottom L by Th61 ; ::_thesis: b "/\" a = Bottom L hence b "/\" a = Bottom L ; ::_thesis: verum end; thus L is distributive ::_thesis: verum proof let a, b, c be Element of L; :: according to LATTICES:def_11 ::_thesis: a "/\" (b + c) = (a "/\" b) + (a "/\" c) A4: ( a "/\" b = a *' b & a "/\" c = a *' c ) by Def23; thus a "/\" (b "\/" c) = a *' (b + c) by Def23 .= (a "/\" b) "\/" (a "/\" c) by A1, A4, Th30 ; ::_thesis: verum end; end; end; registration cluster non empty Lattice-like Robbins de_Morgan -> Boolean for OrthoLattStr ; coherence for b1 being preOrthoLattice st b1 is Robbins & b1 is de_Morgan holds b1 is Boolean ; cluster non empty Lattice-like Boolean well-complemented -> Robbins well-complemented for OrthoLattStr ; coherence for b1 being well-complemented preOrthoLattice st b1 is Boolean holds b1 is Robbins proof let L be well-complemented preOrthoLattice; ::_thesis: ( L is Boolean implies L is Robbins ) assume L is Boolean ; ::_thesis: L is Robbins then reconsider L9 = L as Boolean well-complemented preOrthoLattice ; now__::_thesis:_for_x,_y_being_Element_of_L9_holds_(((x_+_y)_`)_+_((x_+_(y_`))_`))_`_=_x let x, y be Element of L9; ::_thesis: (((x + y) `) + ((x + (y `)) `)) ` = x thus (((x + y) `) + ((x + (y `)) `)) ` = (x + y) "/\" (x + (y `)) by Th33 .= ((x + y) "/\" x) + ((x + y) "/\" (y `)) by LATTICES:def_11 .= ((x + y) "/\" x) + ((x "/\" (y `)) + (y "/\" (y `))) by LATTICES:def_11 .= ((x + y) "/\" x) + ((x "/\" (y `)) + (((y `) + ((y `) `)) `)) by Th33 .= x + ((x "/\" (y `)) + (((y `) + ((y `) `)) `)) by LATTICES:def_9 .= (x + (x "/\" (y `))) + (((y `) + ((y `) `)) `) by LATTICES:def_5 .= x + (((y `) + ((y `) `)) `) by LATTICES:def_8 .= x + ((Top L9) `) by Th59 .= x + (Bottom L9) by Th60 .= x ; ::_thesis: verum end; hence L is Robbins by Def5; ::_thesis: verum end; end;