Copyright (c) 2001 Association of Mizar Users
environ vocabulary LATTICES, BINOP_1, BOOLE, MIDSP_1, VECTSP_2, REALSET1, SUBSET_1, FUNCT_1, ARYTM_3, ARYTM_1, MIDSP_2, ROBBINS1; notation TARSKI, XBOOLE_0, REALSET1, STRUCT_0, LATTICES, VECTSP_2, BINOP_1, FUNCT_1, FUNCT_2, MIDSP_1; constructors VECTSP_2, BINOP_1, LATTICES, REALSET1, MIDSP_2, PARTFUN1; clusters STRUCT_0, RELSET_1, LATTICES, TEX_2, LATTICE2; definitions LATTICES; theorems STRUCT_0, LATTICES, REALSET1, BINOP_1; schemes BINOP_1; begin :: Preliminaries definition struct (1-sorted) ComplStr (# carrier -> set, Compl -> UnOp of the carrier #); end; definition struct(\/-SemiLattStr, ComplStr) ComplLattStr (# carrier -> set, L_join -> BinOp of the carrier, Compl -> UnOp of the carrier #); end; definition struct (ComplLattStr, LattStr) OrthoLattStr (# carrier -> set, L_join, L_meet -> BinOp of the carrier, Compl -> UnOp of the carrier #); end; definition func TrivComplLat -> strict ComplLattStr equals :Def1: ComplLattStr (# {{}}, op2, op1 #); coherence; end; definition func TrivOrtLat -> strict OrthoLattStr equals :Def2: OrthoLattStr (# {{}}, op2, op2, op1 #); coherence; end; definition cluster TrivComplLat -> non empty trivial; coherence by Def1,REALSET1:def 13,STRUCT_0:def 1; cluster TrivOrtLat -> non empty trivial; coherence by Def2,REALSET1:def 13,STRUCT_0:def 1; end; definition cluster strict non empty trivial OrthoLattStr; existence proof take TrivOrtLat; thus thesis; end; cluster strict non empty trivial ComplLattStr; existence proof take TrivComplLat; thus thesis; end; end; definition let L be non empty trivial ComplLattStr; cluster the ComplStr of L -> non empty trivial; coherence proof the carrier of the ComplStr of L is trivial by REALSET1:def 13; hence thesis by REALSET1:def 13,STRUCT_0:def 1; end; end; definition cluster strict non empty trivial ComplStr; existence proof take the ComplStr of TrivOrtLat; thus thesis; end; end; definition let L be non empty ComplStr; let x be Element of L; func x` -> Element of L equals :Def3: (the Compl of L).x; coherence; end; definition let L be non empty ComplLattStr, x,y be Element of L; redefine func x "\/" y; synonym x + y; end; definition let L be non empty ComplLattStr; let x,y be Element of L; func x *' y -> Element of L equals :Def4: (x` "\/" y`)`; coherence; end; definition let L be non empty ComplLattStr; attr L is Robbins means :Def5: for x, y being Element of L holds ((x + y)` + (x + y`)`)` = x; attr L is Huntington means :Def6: for x, y being Element of L holds (x` + y`)` + (x` + y)` = x; end; definition let G be non empty \/-SemiLattStr; attr G is join-idempotent means :Def7: for x being Element of G holds x "\/" x = x; end; definition cluster TrivComplLat -> join-commutative join-associative Robbins Huntington join-idempotent; coherence proof set L = TrivComplLat; thus for x, y being Element of L holds x + y = y + x by REALSET1:def 20; thus for x, y, z being Element of L holds x + y + z = x + (y + z) by REALSET1:def 20; thus for x, y be Element of L holds ((x + y)` + (x + y`)`)` = x by REALSET1:def 20; thus for x, y being Element of L holds (x` + y`)` + (x` + y)` = x by REALSET1:def 20; let x be Element of L; thus thesis by REALSET1:def 20; end; cluster TrivOrtLat -> join-commutative join-associative Huntington Robbins; coherence proof set L = TrivOrtLat; thus for x, y being Element of L holds x + y = y + x by REALSET1:def 20; thus for x, y, z being Element of L holds x + y + z = x + (y + z) by REALSET1:def 20; thus for x, y being Element of L holds (x` + y`)` + (x` + y)` = x by REALSET1:def 20; let x, y be Element of L; thus thesis by REALSET1:def 20; end; end; definition cluster TrivOrtLat -> meet-commutative meet-associative meet-absorbing join-absorbing; coherence proof set L = TrivOrtLat; thus for x, y being Element of L holds x "/\" y = y "/\" x by REALSET1:def 20; thus for x, y, z being Element of L holds x "/\" y "/\" z = x "/\" (y "/\" z) by REALSET1:def 20; thus for x, y being Element of L holds (x "/\" y) "\/" y = y by REALSET1:def 20; let x, y be Element of L; thus x "/\" (x "\/" y) = x by REALSET1:def 20; end; end; definition cluster strict join-associative join-commutative Robbins join-idempotent Huntington (non empty ComplLattStr); existence proof take TrivComplLat; thus thesis; end; end; definition cluster strict Lattice-like Robbins Huntington (non empty OrthoLattStr); existence proof take TrivOrtLat; thus thesis; end; end; definition let L be join-commutative (non empty ComplLattStr), x,y be Element of L; redefine func x + y; commutativity by LATTICES:def 4; end; theorem Th1: :: 4.8 for L being Huntington join-commutative join-associative (non empty ComplLattStr), a, b being Element of L holds (a *' b) + (a *' b`) = a proof let L be Huntington join-commutative join-associative (non empty ComplLattStr), a, b be Element of L; thus (a *' b) + (a *' b`) = (a` + b`)` + (a *' b`) by Def4 .= (a` + b`)` + (a` + b``)` by Def4 .= a by Def6; end; theorem Th2: :: 4.9 for L being Huntington join-commutative join-associative (non empty ComplLattStr), a being Element of L holds a + a` = a` + a`` proof let L be Huntington join-commutative join-associative (non empty ComplLattStr), a be Element of L; set y = a`, z = y``; A1: a = ((a` + y``)` + (a` + y`)`) by Def6; a` = ((a`` + a```)` + (a`` + a``)`) by Def6; then a + a` = (y + z)` + (y + y`)` + (y` + y`)` + (y` + z)` by A1,LATTICES:def 5 .= (y` + y`)` + (y + y`)` + (y + z)` + (y` + z)` by LATTICES:def 5 .= (y` + y)` + (y` + y`)` + ((y + z)` + (y` + z)`) by LATTICES:def 5 .= y + ((y + z)` + (y` + z)`) by Def6 .= y + y` by Def6; hence thesis; end; theorem Th3: :: 4.10 for L being join-commutative join-associative Huntington (non empty ComplLattStr), x being Element of L holds x`` = x proof let L be join-commutative join-associative Huntington (non empty ComplLattStr), x be Element of L; set y = x`; A1: (y`` + y`)` + (y`` + y)` = y` by Def6; (y + y``)` + (y + y`)` = x by Def6; hence thesis by A1,Th2; end; theorem Th4: :: 4.11 revised p. 557 without idempotency for L being join-commutative join-associative Huntington (non empty ComplLattStr), a, b being Element of L holds a + a` = b + b` proof let L be join-commutative join-associative Huntington (non empty ComplLattStr), a, b be Element of L; 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; end; theorem Th5: :: 4.12 for L being join-commutative join-associative join-idempotent Huntington (non empty ComplLattStr) ex c being Element of L st for a being Element of L holds c + a = c & a + a` = c proof let L be join-commutative join-associative join-idempotent Huntington (non empty ComplLattStr); consider b be Element of L; take c = b` + b; let a be Element of L; thus c + a = a` + a + a by Th4 .= a` + (a + a) by LATTICES:def 5 .= a` + a by Def7 .= c by Th4; thus thesis by Th4; end; theorem Th6: :: 4.12 for L being join-commutative join-associative join-idempotent Huntington (non empty ComplLattStr) holds L is upper-bounded proof let L be join-commutative join-associative join-idempotent Huntington (non empty ComplLattStr); 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 thesis by A1,LATTICES:def 14; end; definition cluster join-commutative join-associative join-idempotent Huntington -> upper-bounded (non empty ComplLattStr); coherence by Th6; end; definition let L be join-commutative join-associative join-idempotent Huntington (non empty ComplLattStr); redefine func Top L means :Def8: ex a being Element of L st it = a + a`; compatibility proof let IT be Element of L; hereby assume A1: IT = Top L; consider a being Element of L; take 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; a + a` + b = b + b` + b by Th4 .= b` + (b + b) by LATTICES:def 5 .= b` + b by Def7 .= a` + a by Th4; hence thesis; end; hence IT = a + a` by A1,LATTICES:def 17; end; given a being Element of L such that A2: IT = a + a`; A3: for b being Element of L holds a + a` + b = a + a` proof let b be Element of L; a + a` + b = b + b` + b by Th4 .= b` + (b + b) by LATTICES:def 5 .= b` + b by Def7 .= a` + a by Th4; hence thesis; end; then for b being Element of L holds b + (a + a`) = a + a`; hence IT = Top L by A2,A3,LATTICES:def 17; end; end; theorem Th7: :: 4.13 for L being join-commutative join-associative join-idempotent Huntington (non empty ComplLattStr) ex c being Element of L st for a being Element of L holds c *' a = c & (a + a`)` = c proof let L be join-commutative join-associative join-idempotent Huntington (non empty ComplLattStr); consider b be Element of L; take c = (b` + b)`; let a be Element of L; thus c *' a = ((b` + b)`` + a`)` by Def4 .= ((b` + b) + a`)` by Th3 .= ((a` + a) + a`)` by Th4 .= (a + (a` + a`))` by LATTICES:def 5 .= (a + a`)` by Def7 .= c by Th4; thus thesis by Th4; end; theorem Th8: :: 4.18 for L being join-commutative join-associative (non empty ComplLattStr), a, b being Element of L holds a *' b = b *' a proof let L be join-commutative join-associative (non empty ComplLattStr), a, b be Element of L; thus a *' b = (a` + b`)` by Def4 .= b *' a by Def4; end; definition let L be join-commutative join-associative (non empty ComplLattStr); let x,y be Element of L; redefine func x *' y; commutativity by Th8; end; definition let L be join-commutative join-associative join-idempotent Huntington (non empty ComplLattStr); func Bot L -> Element of L means :Def9: for a being Element of L holds it *' a = it; existence proof consider c being Element of L such that A1: for a being Element of L holds c *' a = c & (a + a`)` = c by Th7; thus thesis by A1; end; uniqueness proof let c1,c2 be Element of L such that A2: for a being Element of L holds c1 *' a = c1 and A3: for a being Element of L holds c2 *' a = c2; thus c1 = c2 *' c1 by A2 .= c2 by A3; end; end; theorem Th9: for L being join-commutative join-associative join-idempotent Huntington (non empty ComplLattStr), a being Element of L holds Bot L = (a + a`)` proof let L be join-commutative join-associative join-idempotent Huntington (non empty ComplLattStr), a be Element of L; for b being Element of L holds (a + a`)` *' b = (a + a`)` proof let b be Element of L; (a + a`)` *' b = (b + b`)` *' b by Th4 .= ((b + b`)`` + b`)` by Def4 .= ((b + b`) + b`)` by Th3 .= (b + (b` + b`))` by LATTICES:def 5 .= (b + b`)` by Def7 .= (a` + a)` by Th4; hence thesis; end; hence thesis by Def9; end; theorem Th10: for L being join-commutative join-associative join-idempotent Huntington (non empty ComplLattStr) holds (Top L)` = Bot L & Top L = (Bot L)` proof let L be join-commutative join-associative join-idempotent Huntington (non empty ComplLattStr); consider a be Element of L; thus (Top L)` = (a + a`)` by Def8 .= Bot L by Th9; hence Top L = (Bot L)` by Th3; end; theorem Th11: :: 4.14 for L being join-commutative join-associative Huntington (non empty ComplLattStr), a, b being Element of L st a` = b` holds a = b proof let L be join-commutative join-associative Huntington (non empty ComplLattStr), a, b being Element of L; assume A1: a` = b`; thus a = a`` by Th3 .= b by A1,Th3; end; theorem Th12: :: 4.15 proof without join-idempotency, no top at all for L being join-commutative join-associative Huntington (non empty ComplLattStr), a, b being Element of L holds a + (b + b`)` = a proof let L be join-commutative join-associative Huntington (non empty ComplLattStr), a, b be Element of L; set O = b + b`; A1:O`` = O by Th3; A2:O` = (O`` + O``)` + (O`` + O`)` by Def6 .= (O + O)` + O` by A1,Th4; O = O + O` by Th4 .= O + O` + (O + O)` by A2,LATTICES:def 5 .= O + (O + O)` by Th4; then A3:O + O = O + O + (O + O)` by LATTICES:def 5 .= O by Th4; A4:O = a` + a by Th4; hence a + O` = ((a` + a`)` + (a` + a)`) + ((a` + a)` + (a` + a)`) by A2,A3,Def6 .= (a` + a`)` + ((a` + a)` + (a` + a)`) by A2,A3,A4,LATTICES:def 5 .= a by A2,A3,A4,Def6; end; theorem Th13: :: 4.5 for L being join-commutative join-associative Huntington (non empty ComplLattStr), a being Element of L holds a + a = a proof let L be join-commutative join-associative Huntington (non empty ComplLattStr), a be Element of L; A1:(a + a)` = (a`` + a`)` + (a + a)` by Th12 .= (a`` + a`)` + (a`` + a)` by Th3 .= a` by Def6; thus a + a = (a + a)`` by Th3 .= a by A1,Th3; end; definition cluster join-commutative join-associative Huntington -> join-idempotent (non empty ComplLattStr); coherence proof let L be non empty ComplLattStr; assume L is join-commutative join-associative Huntington; then for a being Element of L holds a + a = a by Th13; hence thesis by Def7; end; end; theorem Th14: :: 4.15 for L being join-commutative join-associative Huntington (non empty ComplLattStr), a being Element of L holds a + Bot L = a proof let L be join-commutative join-associative Huntington (non empty ComplLattStr), a be Element of L; a = (a` + a`)` + (a` + a)` by Def6 .= a`` + (a` + a)` by Def7 .= a + (a` + a)` by Th3; hence thesis by Th9; end; theorem :: 4.16 for L being join-commutative join-associative Huntington (non empty ComplLattStr), a being Element of L holds a *' Top L = a proof let L be join-commutative join-associative Huntington (non empty ComplLattStr), a be Element of L; a *' Top L = (a` + (Top L)`)` by Def4 .= (a` + Bot L)` by Th10 .= a`` by Th14 .= a by Th3; hence thesis; end; theorem Th16: :: 4.17 for L being join-commutative join-associative Huntington (non empty ComplLattStr), a being Element of L holds a *' a` = Bot L proof let L be join-commutative join-associative Huntington (non empty ComplLattStr), a be Element of L; thus a *' a` = (a` + a``)` by Def4 .= (Top L)` by Def8 .= Bot L by Th10; end; theorem Th17: :: 4.19 for L being join-commutative join-associative Huntington (non empty ComplLattStr), a, b, c being Element of L holds a *' (b *' c) = a *' b *' c proof let L be join-commutative join-associative Huntington (non empty ComplLattStr), a, b, c be Element of L; thus a *' b *' c = (a` + b`)` *' c by Def4 .= ((a` + b`)`` + c`)` by Def4 .= (a` + b` + c`)` by Th3 .= (a` + (b` + c`))` by LATTICES:def 5 .= (a` + (b` + c`)``)` by Th3 .= (a` + (b *' c)`)` by Def4 .= a *' (b *' c) by Def4; end; theorem Th18: :: 4.20 for L being join-commutative join-associative Huntington (non empty ComplLattStr), a, b being Element of L holds a + b = (a` *' b`)` proof let L be join-commutative join-associative Huntington (non empty ComplLattStr), a, b be Element of L; a` *' b` = (a`` + b``)` by Def4 .= (a`` + b)` by Th3 .= (a + b)` by Th3; hence (a` *' b`)` = a + b by Th3; end; theorem :: 4.21 for L being join-commutative join-associative Huntington (non empty ComplLattStr), a being Element of L holds a *' a = a proof let L be join-commutative join-associative Huntington (non empty ComplLattStr), a be Element of L; thus a *' a = (a` + a`)` by Def4 .= a`` by Def7 .= a by Th3; end; theorem :: 4.22 for L being join-commutative join-associative Huntington (non empty ComplLattStr), a being Element of L holds a + Top L = Top L proof let L be join-commutative join-associative Huntington (non empty ComplLattStr), a be Element of 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; end; theorem Th21: :: 4.24 for L being join-commutative join-associative Huntington (non empty ComplLattStr), a, b being Element of L holds a + (a *' b) = a proof let L be join-commutative join-associative Huntington (non empty ComplLattStr), a,b be Element of L; thus a + (a *' b) = (a *' b) + ((a *' b) + (a *' b`)) by Th1 .= (a *' b) + (a *' b) + (a *' b`) by LATTICES:def 5 .= (a *' b) + (a *' b`) by Def7 .= a by Th1; end; theorem Th22: :: 4.25 for L being join-commutative join-associative Huntington (non empty ComplLattStr), a, b being Element of L holds a *' (a + b) = a proof let L be join-commutative join-associative Huntington (non empty ComplLattStr), a,b be Element of L; thus a *' (a + b) = (a` + (a + b)`)` by Def4 .= (a` + (a` *' b`)``)` by Th18 .= (a` + (a` *' b`))` by Th3 .= a`` by Th21 .= a by Th3; end; theorem Th23: :: 4.26 for L being join-commutative join-associative Huntington (non empty ComplLattStr), a, b being Element of L st a` + b = Top L & b` + a = Top L holds a = b proof let L be join-commutative join-associative Huntington (non empty ComplLattStr), a, b be Element of L; assume A1: a` + b = Top L & b` + a = Top L; thus a = (a` + b`)` + (a` + b)` by Def6 .= b by A1,Def6; end; theorem Th24: :: 4.27 for L being join-commutative join-associative Huntington (non empty ComplLattStr), a, b being Element of L st a + b = Top L & a *' b = Bot L holds a` = b proof let L be join-commutative join-associative Huntington (non empty ComplLattStr), a, b be Element of L; assume a + b = Top L; then A1: a`` + b = Top L by Th3; assume a *' b = Bot L; then A2:(a` + b`)` = Bot L by Def4; b` + a` = (a` + b`)`` by Th3 .= Top L by A2,Th10; hence thesis by A1,Th23; end; theorem Th25: :: 4.28 for L being join-commutative join-associative Huntington (non empty ComplLattStr), 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 join-commutative join-associative Huntington (non empty ComplLattStr), a, b, c be Element of L; set A = a *' b *' c, B = a *' b *' c`, C = a *' b` *' c; set D = a *' b` *' c`, E = a` *' b *' c, F = a` *' b *' c`; set G = a` *' b` *' c, H = a` *' b` *' c`; A + B + C + D + E + F + G + H = (a *' b) + C + D + E + F + G + H by Th1 .= (a *' b) + (C + D) + E + F + G + H by LATTICES:def 5 .= (a *' b) + (a *' b`) + E + F + G + H by Th1 .= (a *' b) + (a *' b`) + (E + F) + G + H by LATTICES:def 5 .= (a *' b) + (a *' b`) + (a` *' b) + G + H by Th1 .= (a *' b) + (a *' b`) + (a` *' b) + (G + H) by LATTICES:def 5 .= (a *' b) + (a *' b`) + (a` *' b) + (a` *' b`) by Th1 .= a + (a` *' b) + (a` *' b`) by Th1 .= a + ((a` *' b) + (a` *' b`)) by LATTICES:def 5 .= a + a` by Th1; hence thesis by Def8; end; theorem Th26: :: 4.29 for L being join-commutative join-associative Huntington (non empty ComplLattStr), 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 & (a *' b` *' c) *' (a` *' b *' c) = Bot L proof let L be join-commutative join-associative Huntington (non empty ComplLattStr), a, b, c be Element of 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; thus (a *' c) *' (b *' c`) = (a *' c) *' c` *' b by Th17 .= a *' (c *' c`) *' b by Th17 .= a *' Bot L *' b by Th16 .= Bot L *' b by Def9 .= Bot L by Def9; end; hence (a *' c) *' (b *' c`) = Bot L; thus a *' b *' c *' (a` *' b *' c) = a *' (b *' c) *' (a` *' b *' c) by Th17 .= b *' c *' a *' (a` *' b) *' c by Th17 .= b *' c *' a *' a` *' b *' c by Th17 .= b *' c *' (a *' a`) *' b *' c by Th17 .= b *' c *' (a *' a`) *' (b *' c) by Th17 .= b *' c *' Bot L *' (b *' c) by Th16 .= Bot L *' (b *' c) by Def9 .= Bot L by Def9; thus (a *' b` *' c) *' (a` *' b *' c) = a *' (b` *' c) *' (a` *' b *' c) by Th17 .= (b` *' c) *' a *' (a` *' (b *' c)) by Th17 .= (b` *' c) *' a *' a` *' (b *' c) by Th17 .= (b` *' c) *' (a *' a`) *' (b *' c) by Th17 .= (b` *' c) *' Bot L *' (b *' c) by Th16 .= Bot L *' (b *' c) by Def9 .= Bot L by Def9; thus (a *' b *' c) *' (a` *' b` *' c) = (a *' (b *' c)) *' (a` *' b` *' c) by Th17 .= (a *' (b *' c)) *' (a` *' (b` *' c)) by Th17 .= Bot L by A1; thus (a *' b *' c`) *' (a` *' b` *' c`) = (a *' (b *' c`)) *' (a` *' b` *' c`) by Th17 .= (a *' (b *' c`)) *' (a` *' (b` *' c`)) by Th17 .= Bot L by A1; thus (a *' b` *' c) *' (a` *' b *' c) = (a *' (b` *' c)) *' (a` *' b *' c) by Th17 .= (a *' (b` *' c)) *' (a` *' (b *' c)) by Th17 .= Bot L by A1; end; theorem Th27: :: 4.30 for L being join-commutative join-associative Huntington (non empty ComplLattStr), 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 join-commutative join-associative Huntington (non empty ComplLattStr), a, b, c be Element of L; set A = a *' b *' c; a *' c = (a *' c *' b) + (a *' c *' b`) by Th1 .= A + (a *' c *' b`) by Th17 .= A + (a *' b` *' c) by Th17; hence (a *' b) + (a *' c) = A + (a *' b *' c`) + (A + (a *' b` *' c)) by Th1 .= A + ((a *' b *' c`) + A) + (a *' b` *' c) by LATTICES:def 5 .= A + A + (a *' b *' c`) + (a *' b` *' c) by LATTICES:def 5 .= A + (a *' b *' c`) + (a *' b` *' c) by Def7; end; theorem Th28: :: 4.31 for L being join-commutative join-associative Huntington (non empty ComplLattStr), 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 join-commutative join-associative Huntington (non empty ComplLattStr), a, b, c be Element of L; set D = a *' b` *' c`, E = a` *' b *' c, F = a` *' b *' c`; set G = a` *' b` *' c, H = a` *' b` *' c`; A1:(a *' (b + c))` = (a` + (b + c)`)`` by Def4 .= a` + (b + c)` by Th3 .= a` + (b` *' c`)`` by Th18 .= a` + (b` *' c`) by Th3; A2:a` = (a` *' b) + (a` *' b`) by Th1 .= E + F + (a` *' b`) by Th1 .= E + F + (G + H) by Th1; b` *' c` = (a *' (b` *' c`)) + (a` *' (b` *' c`)) by Th1 .= D + (a` *' (b` *' c`)) by Th17 .= D + H by Th17; hence (a *' (b + c))` = E + F + (G + H) + H + D by A1,A2,LATTICES:def 5 .= E + F + G + H + H + D by LATTICES:def 5 .= E + F + G + (H + H) + D by LATTICES:def 5 .= E + F + G + H + D by Def7 .= D + (E + F + (G + H)) by LATTICES:def 5 .= D + (E + F) + (G + H) by LATTICES:def 5 .= D + (E + F) + G + H by LATTICES:def 5 .= D + E + F + G + H by LATTICES:def 5; end; theorem Th29: :: 4.32 for L being join-commutative join-associative Huntington (non empty ComplLattStr), a, b, c being Element of L holds ((a *' b) + (a *' c)) + (a *' (b + c))` = Top L proof let L be join-commutative join-associative Huntington (non empty ComplLattStr), a, b, c be Element of L; set A = a *' b *' c, B = a *' b *' c`, C = a *' b` *' c; set D = a *' b` *' c`, E = a` *' b *' c, F = a` *' b *' c`; set G = a` *' b` *' c, H = a` *' b` *' c`; set ABC = A + B + C, GH = G + H; A1:(a *' (b + c))` = D + E + F + G + H by Th28; (a *' b) + (a *' c) = ABC by Th27; then (a *' b) + (a *' c) + (a *' (b + c))` = ABC + (D + E + F + GH) by A1,LATTICES:def 5 .= ABC + (D + E + (F + GH)) by LATTICES:def 5 .= ABC + (D + E) + (F + GH) by LATTICES:def 5 .= ABC + D + E + (F + GH) by LATTICES:def 5 .= ABC + D + (E + (F + GH)) by LATTICES:def 5 .= ABC + D + (E + (F + G + H)) by LATTICES:def 5 .= ABC + D + E + (F + G + H) by LATTICES:def 5 .= ABC + D + E + (F + GH) by LATTICES:def 5 .= ABC + D + E + F + GH by LATTICES:def 5 .= ABC + D + E + F + G + H by LATTICES:def 5 .= Top L by Th25; hence thesis; end; theorem Th30: :: 4.33 for L being join-commutative join-associative Huntington (non empty ComplLattStr), a, b, c being Element of L holds ((a *' b) + (a *' c)) *' (a *' (b + c))` = Bot L proof let L be join-commutative join-associative Huntington (non empty ComplLattStr), a, b, c be Element of L; set A = a *' b *' c, B = a *' b *' c`, C = a *' b` *' c; set D = a *' b` *' c`, E = a` *' b *' c, F = a` *' b *' c`; set G = a` *' b` *' c, H = a` *' b` *' c`; set DEFG = D + E + F + G; A1: C *' D = Bot L by Th26; A2: A *' G = Bot L & B *' H = Bot L & C *' E = Bot L by Th26; A3:(a *' (b + c))` = DEFG + H by Th28; (A *' D) + (A *' E) = Bot L + (A *' E) by Th26 .= Bot L + Bot L by Th26 .= Bot L by Def7; then Top L = Bot L + (A *' (D + E))` by Th29 .= (A *' (D + E))` by Th14; then Bot L = (A *' (D + E))`` by Th10 .= A *' (D + E) by Th3; then (A *' (D + E)) + (A *' F) = Bot L + Bot L by Th26 .= Bot L by Def7; then Top L = Bot L + (A *' (D + E + F))` by Th29 .= (A *' (D + E + F))` by Th14; then Bot L = (A *' (D + E + F))`` by Th10 .= A *' (D + E + F) by Th3; then (A *' (D + E + F)) + (A *' G) = Bot L by A2,Def7; then Top L = Bot L + (A *' DEFG)` by Th29 .= (A *' DEFG)` by Th14; then Bot L = (A *' DEFG)`` by Th10 .= A *' DEFG by Th3; then A4:(A *' DEFG) + (A *' H) = Bot L + Bot L by Th26 .= Bot L by Def7; (B *' D) + (B *' E) = Bot L + (B *' E) by Th26 .= Bot L + Bot L by Th26 .= Bot L by Def7; then Top L = Bot L + (B *' (D + E))` by Th29 .= (B *' (D + E))` by Th14; then Bot L = (B *' (D + E))`` by Th10 .= B *' (D + E) by Th3; then (B *' (D + E)) + (B *' F) = Bot L + Bot L by Th26 .= Bot L by Def7; then Top L = Bot L + (B *' (D + E + F))` by Th29 .= (B *' (D + E + F))` by Th14; then Bot L = (B *' (D + E + F))`` by Th10 .= B *' (D + E + F) by Th3; then (B *' (D + E + F)) + (B *' G) = Bot L + Bot L by Th26 .= Bot L by Def7; then Top L = Bot L + (B *' DEFG)` by Th29 .= (B *' DEFG)` by Th14; then Bot L = (B *' DEFG)`` by Th10 .= B *' DEFG by Th3; then A5:(B *' DEFG) + (B *' H) = Bot L by A2,Def7; A6:Top L = Bot L + (A *' (DEFG + H))` by A4,Th29 .= (A *' (DEFG + H))` by Th14; A7:Top L = Bot L + (B *' (DEFG + H))` by A5,Th29 .= (B *' (DEFG + H))` by Th14; (C *' D) + (C *' E) = Bot L + Bot L by A1,Th26 .= Bot L by Def7; then Top L = Bot L + (C *' (D + E))` by Th29 .= (C *' (D + E))` by Th14; then Bot L = (C *' (D + E))`` by Th10 .= C *' (D + E) by Th3; then (C *' (D + E)) + (C *' F) = Bot L + Bot L by Th26 .= Bot L by Def7; then Top L = Bot L + (C *' (D + E + F))` by Th29 .= (C *' (D + E + F))` by Th14; then Bot L = (C *' (D + E + F))`` by Th10 .= C *' (D + E + F) by Th3; then (C *' (D + E + F)) + (C *' G) = Bot L + Bot L by Th26 .= Bot L by Def7; then Top L = Bot L + (C *' DEFG)` by Th29 .= (C *' DEFG)` by Th14; then Bot L = (C *' DEFG)`` by Th10 .= C *' DEFG by Th3; then (C *' DEFG) + (C *' H) = Bot L + Bot L by Th26 .= Bot L by Def7; then A8:Top L = Bot L + (C *' (DEFG + H))` by Th29 .= (C *' (DEFG + H))` by Th14; A9: A *' (DEFG + H) = (A *' (DEFG + H))`` by Th3 .= Bot L by A6,Th10; A10: B *' (DEFG + H) = (B *' (DEFG + H))`` by Th3 .= Bot L by A7,Th10; A11: C *' (DEFG + H) = (C *' (DEFG + H))`` by Th3 .= Bot L by A8,Th10; (A *' (DEFG + H)) + (B *' (DEFG + H)) = Bot L by A9,A10,Def7; then Top L = Bot L + ((A + B) *' (DEFG + H))` by Th29 .= ((A + B) *' (DEFG + H))` by Th14; then Bot L = ((A + B) *' (DEFG + H))`` by Th10 .= (A + B) *' (DEFG + H) by Th3; then ((A + B) *' (DEFG + H)) + (C *' (DEFG + H)) = Bot L by A11,Def7; then Top L = Bot L + ((A + B + C) *' (DEFG + H))` by Th29 .= ((A + B + C) *' (DEFG + H))` by Th14; then Bot L = ((A + B + C) *' (DEFG + H))`` by Th10 .= (A + B + C) *' (DEFG + H) by Th3; hence thesis by A3,Th27; end; theorem Th31: :: 4.34 for L being join-commutative join-associative Huntington (non empty ComplLattStr), a, b, c being Element of L holds a *' (b + c) = (a *' b) + (a *' c) proof let L be join-commutative join-associative Huntington (non empty ComplLattStr), a, b, c be Element of L; A1:(a *' b) + (a *' c) + (a *' (b + c))` = Top L by Th29; ((a *' b) + (a *' c)) *' (a *' (b + c))` = Bot L by Th30; then ((a *' b) + (a *' c))` = (a *' (b + c))` by A1,Th24; hence thesis by Th11; end; theorem :: 4.35 for L being join-commutative join-associative Huntington (non empty ComplLattStr), a, b, c being Element of L holds a + (b *' c) = (a + b) *' (a + c) proof let L be join-commutative join-associative Huntington (non empty ComplLattStr), a, b, c be Element of L; thus a + (b *' c) = a + (b` + c`)` by Def4 .= (a` *' (b` + c`)``)` by Th18 .= (a` *' (b` + c`))` by Th3 .= ((a` *' b`) + (a` *' c`))` by Th31 .= ((a` *' b`)` *' (a` *' c`)`)`` by Th18 .= (a` *' b`)` *' (a` *' c`)` by Th3 .= (a + b) *' (a` *' c`)` by Th18 .= (a + b) *' (a + c) by Th18; end; begin :: Pre-Ortholattices definition let L be non empty OrthoLattStr; attr L is well-complemented means :Def10: for a being Element of L holds a` is_a_complement_of a; end; definition cluster TrivOrtLat -> Boolean well-complemented; coherence proof set L = TrivOrtLat; thus L is lower-bounded proof consider c being Element of L; take c; thus thesis by REALSET1:def 20; end; thus L is upper-bounded; thus L is complemented proof let b be Element of L; take a = b; a is_a_complement_of b proof thus a "\/" b = Top L & b "\/" a = Top L & a "/\" b = Bottom L & b "/\" a = Bottom L by REALSET1:def 20; end; hence thesis; end; thus L is distributive proof let x, y, z be Element of L; thus thesis by REALSET1:def 20; end; thus L is well-complemented proof let a be Element of L; thus a` is_a_complement_of a proof thus a` "\/" a = Top L & a "\/" a` = Top L & a` "/\" a = Bottom L & a "/\" a` = Bottom L by REALSET1:def 20; end; end; end; end; definition mode preOrthoLattice is Lattice-like (non empty OrthoLattStr); end; definition cluster strict Boolean well-complemented preOrthoLattice; existence proof take TrivOrtLat; thus thesis; end; end; theorem Th33: for L being distributive well-complemented preOrthoLattice, x being Element of L holds x`` = x proof let L be distributive well-complemented preOrthoLattice; let x be Element of L; A1: x` is_a_complement_of x by Def10; x`` is_a_complement_of x` by Def10; then A2: x`` + x` = Top L & x`` "/\" x` = Bottom L by LATTICES:def 18; x` "\/" x = Top L & x` "/\" x = Bottom L by A1,LATTICES:def 18; hence thesis by A2,LATTICES:32; end; theorem Th34: for L being bounded distributive well-complemented preOrthoLattice, x, y being Element of L holds x "/\" y = (x` "\/" y`)` proof let L be bounded distributive well-complemented preOrthoLattice; let x, y be Element of L; x` is_a_complement_of x by Def10; then A1: x` "\/" x = Top L & x` "/\" x = Bottom L by LATTICES:def 18; y` is_a_complement_of y by Def10; then A2: y` "\/" y = Top L & y` "/\" y = Bottom L by LATTICES:def 18; A3: (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 A1,LATTICES:def 7 .= Bottom L "\/" (x "/\" Bottom L) by A2,LATTICES:40 .= Bottom L "\/" Bottom L by LATTICES:40 .= Bottom L by LATTICES:39; A4: x` "\/" Top L = Top L "\/" x` by LATTICES:def 4 .= Top L by LATTICES:44; A5: y` "\/" Top L = Top L "\/" y` by LATTICES:def 4 .= Top L by LATTICES:44; A6: (x` "\/" y`) "\/" (x "/\" y) = (x` "\/" y` "\/" x) "/\" (x` "\/" y` "\/" y) by LATTICES:31 .= (y` "\/" x` "\/" x) "/\" (x` "\/" y` "\/" y) by LATTICES:def 4 .= (y` "\/" x` "\/" x) "/\" Top L by A2,A4,LATTICES:def 5 .= Top L "/\" Top L by A1,A5,LATTICES:def 5 .= Top L by LATTICES:43; A7: (x "/\" y)` is_a_complement_of (x "/\" y) by Def10; then A8: (x "/\" y)` "\/" (x "/\" y) = Top L & (x "/\" y)` "/\" (x "/\" y) = Bottom L by LATTICES:def 18; (x "/\" y) + (x "/\" y)` = (x "/\" y) + (x` + y`) by A6,A7,LATTICES:def 18 ; then (x "/\" y)` = x` "\/" y` by A3,A8,LATTICES:32; hence thesis by Th33; end; begin :: Correspondence between boolean preOrthoLattice and boolean lattice :: according to the definition given in \cite{LATTICES.ABS} definition let L be non empty ComplLattStr; func CLatt L -> strict OrthoLattStr means :Def11: 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 proof deffunc F(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) = F(a,b) from BinOpLambda; take OrthoLattStr (# the carrier of L, the L_join of L, K, the Compl of L #); thus thesis by A1; end; uniqueness proof let L1, L2 be strict OrthoLattStr such that A2: 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 and A3: 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; reconsider A = the L_meet of L1, B = the L_meet of L2 as BinOp of the carrier of L by A2,A3; now let a, b be Element of L; thus A.(a,b) = a *' b by A2 .= B.(a,b) by A3; end; hence thesis by A2,A3,BINOP_1:2; end; end; definition let L be non empty ComplLattStr; cluster CLatt L -> non empty; coherence proof the carrier of CLatt L = the carrier of L by Def11; hence thesis by STRUCT_0:def 1; end; end; definition let L be join-commutative (non empty ComplLattStr); cluster CLatt L -> join-commutative; coherence proof let a,b be Element of CLatt L; A1: the carrier of L = the carrier of CLatt L by Def11; the L_join of L = the L_join of CLatt L by Def11; hence a "\/" b = (the L_join of L).(a,b) by LATTICES:def 1 .= (the L_join of L).(b,a) by A1,BINOP_1:def 2 .= (the L_join of CLatt L).(b,a) by Def11 .= b "\/" a by LATTICES:def 1; end; end; definition let L be join-associative (non empty ComplLattStr); cluster CLatt L -> join-associative; coherence proof let a, b, c be Element of CLatt L; set K = the L_join of L, M = the L_join of CLatt L; A1: the carrier of L = the carrier of CLatt L by Def11; A2: K = M by Def11; thus (a "\/" b) "\/" c = M.(a "\/" b,c) by LATTICES:def 1 .= M.(M.(a,b),c) by LATTICES:def 1 .= K.(a,K.(b,c)) by A1,A2,BINOP_1:def 3 .= M.(a,b "\/" c) by A2,LATTICES:def 1 .= a "\/" (b "\/" c) by LATTICES:def 1; end; end; definition let L be join-commutative join-associative (non empty ComplLattStr); cluster CLatt L -> meet-commutative; coherence proof let a, b be Element of CLatt L; reconsider a' = a, b' = b as Element of L by Def11; thus a "/\" b = (the L_meet of CLatt L).(a,b) by LATTICES:def 2 .= b' *' a' by Def11 .= (the L_meet of CLatt L).(b,a) by Def11 .= b "/\" a by LATTICES:def 2; end; end; theorem Th35: for L being non empty ComplLattStr, a, b being Element of L, a', b' being Element of CLatt L st a = a' & b = b' holds a *' b = a' "/\" b' & a + b = a' "\/" b' & a` = a'` proof let L be non empty ComplLattStr, a, b be Element of L, a', b' be Element of CLatt L; assume A1: a = a' & b = b'; thus a *' b = (the L_meet of CLatt L).(a,b) by Def11 .= a' "/\" b' by A1,LATTICES:def 2; thus a + b = (the L_join of L).(a,b) by LATTICES:def 1 .= (the L_join of CLatt L).(a,b) by Def11 .= a' "\/" b' by A1,LATTICES:def 1; thus a` = (the Compl of L).a by Def3 .= (the Compl of CLatt L).a by Def11 .= a'` by A1,Def3; end; definition let L be join-commutative join-associative Huntington (non empty ComplLattStr); cluster CLatt L -> meet-associative join-absorbing meet-absorbing; coherence proof hereby let a, b, c be Element of CLatt L; reconsider a' = a, b' = b, c' = c as Element of L by Def11; A1: a' *' b' = a "/\" b & b' *' c' = b "/\" c by Th35; hence a "/\" b "/\" c = a' *' b' *' c' by Th35 .= a' *' (b' *' c') by Th17 .= a "/\" (b "/\" c) by A1,Th35; end; hereby let a, b be Element of CLatt L; reconsider a' = a, b' = b as Element of L by Def11; a' + b' = a "\/" b by Th35; hence a "/\" (a "\/" b) = a' *' (a' + b') by Th35 .= a by Th22; end; let a, b be Element of CLatt L; reconsider a' = a, b' = b as Element of L by Def11; a' *' b' = a "/\" b by Th35; hence (a "/\" b) "\/" b = (a' *' b') + b' by Th35 .= b by Th21; end; end; definition let L be Huntington (non empty ComplLattStr); cluster CLatt L -> Huntington; coherence proof let x, y be Element of CLatt L; reconsider x' = x, y' = y as Element of L by Def11; A1: x` = x'` & y` = y'` by Th35; then x` + y` = x'` + y'` by Th35; then A2: (x` + y`)` = (x'` + y'`)` by Th35; x` + y = x'` + y' by A1,Th35; then (x` + y)` = (x'` + y')` by Th35; hence (x` + y`)` + (x` + y)` = (x'` + y'`)` + (x'` + y')` by A2,Th35 .= x by Def6; end; end; definition let L be join-commutative join-associative Huntington (non empty ComplLattStr); cluster CLatt L -> lower-bounded; coherence proof thus CLatt L is lower-bounded proof set c' = Bot L; reconsider c = c' as Element of CLatt L by Def11; take c; let a be Element of CLatt L; reconsider a' = a as Element of L by Def11; thus c "/\" a = c' *' a' by Th35 .= c by Def9; hence a "/\" c = c; end; end; end; theorem Th36: for L being join-commutative join-associative Huntington (non empty ComplLattStr) holds Bot L = Bottom CLatt L proof let L be join-commutative join-associative Huntington (non empty ComplLattStr); the carrier of CLatt L = the carrier of L by Def11; then reconsider C = Bot L as Element of CLatt L; for a being Element of CLatt L holds C "/\" a = C & a "/\" C = C proof let a be Element of CLatt L; reconsider a' = a as Element of L by Def11; thus C "/\" a = Bot L *' a' by Th35 .= C by Def9; hence thesis; end; hence thesis by LATTICES:def 16; end; definition let L be join-commutative join-associative Huntington (non empty ComplLattStr); cluster CLatt L -> complemented distributive bounded; coherence proof A1: the Compl of CLatt L = the Compl of L by Def11; thus CLatt L is complemented proof let b be Element of CLatt L; take a = b`; reconsider a' = a, b' = b as Element of L by Def11; thus a + b = Top CLatt L by Def8; thus b + a = Top CLatt L by Def8; A2: a'` = (the Compl of L).a' by Def3 .= a` by A1,Def3 .= b' by Th3; thus a "/\" b = a' *' b' by Th35 .= (a'` + b'`)` by Def4 .= Bot L by A2,Th9 .= Bottom CLatt L by Th36; hence b "/\" a = Bottom CLatt L; end; hereby let a, b, c be Element of CLatt L; reconsider a' = a, b' = b, c' = c as Element of L by Def11; A3: b' + c' = b "\/" c & a "/\" b = a' *' b' & a "/\" c = a' *' c' by Th35; hence a "/\" (b "\/" c) = a' *' (b' + c') by Th35 .= (a' *' b') + (a' *' c') by Th31 .= (a "/\" b) "\/" (a "/\" c) by A3,Th35; end; thus CLatt L is lower-bounded; thus CLatt L is upper-bounded; end; end; begin :: Proofs according to Bernd Ingo Dahn definition let G be non empty ComplLattStr, x be Element of G; redefine func x`; synonym -x; end; definition let G be join-commutative (non empty ComplLattStr); redefine attr G is Huntington means :Def12: for x, y being Element of G holds -(-x + -y) + -(x + -y) = y; compatibility proof thus G is Huntington implies for x, y being Element of G holds -(-x + -y) + -(x + -y) = y by Def6; assume A1: for x, y being Element of G holds -(-x + -y) + -(x + -y) = y; let x, y be Element of G; (x` + y`)` + (x` + y)` = x by A1; hence thesis; end; end; definition let G be non empty ComplLattStr; attr G is with_idempotent_element means :Def13: ex x being Element of G st x + x = x; correctness; end; reserve G for Robbins join-associative join-commutative (non empty ComplLattStr); reserve x, y, z, u, v for Element of G; definition let G be non empty ComplLattStr, x, y be Element of G; func \delta (x, y) -> Element of G equals :Def14: -(-x + y); coherence; end; definition let G be non empty ComplLattStr, x, y be Element of G; func Expand (x, y) -> Element of G equals :Def15: \delta (x + y, \delta(x, y)); coherence; end; definition let G be non empty ComplLattStr, x be Element of G; func x _0 -> Element of G equals :Def16: -(-x + x); coherence; func Double x -> Element of G equals :Def17: x + x; coherence; end; definition let G be non empty ComplLattStr, x be Element of G; func x _1 -> Element of G equals :Def18: x _0 + x; coherence; func x _2 -> Element of G equals :Def19: x _0 + Double x; coherence; func x _3 -> Element of G equals :Def20: x _0 + (Double x + x); coherence; func x _4 -> Element of G equals :Def21: x _0 + (Double x + Double x); coherence; end; theorem Th37: \delta ((x + y), (\delta (x, y))) = y proof thus \delta ((x + y), (\delta (x, y))) = \delta (x + y, -(-x + y)) by Def14 .= -(-(x + y) + -(-x + y)) by Def14 .= y by Def5; end; theorem Th38: Expand (x, y) = y proof thus Expand (x, y) = \delta (x + y, \delta(x, y)) by Def15 .= y by Th37; end; theorem Th39: \delta (-x + y, z) = -(\delta (x, y) + z) proof thus \delta (-x + y, z) = -(-(-x + y) + z) by Def14 .= -(\delta (x, y) + z) by Def14; end; theorem Th40: \delta (x, x) = x _0 proof thus \delta (x, x) = -(-x + x) by Def14 .= x _0 by Def16; end; theorem Th41: \delta (Double x, x _0) = x proof thus \delta (Double x, x _0) = \delta (Double x, \delta (x, x)) by Th40 .= \delta (x + x, \delta (x, x)) by Def17 .= Expand (x, x) by Def15 .= x by Th38; end; theorem Th42: :: Lemma 1 \delta (x _2, x) = x _0 proof thus \delta (x _2, x) = \delta (Double x + x _0, x) by Def19 .= \delta (Double x + x _0, \delta (Double x, x _0)) by Th41 .= Expand (Double x, x _0) by Def15 .= x _0 by Th38; end; theorem Th43: x _2 + x = x _3 proof thus x _2 + x = x _0 + Double x + x by Def19 .= x _0 + (Double x + x) by LATTICES:def 5 .= x _3 by Def20; end; theorem Th44: x _4 + x _0 = x _3 + x _1 proof thus x _4 + x _0 = x _0 + (Double x + Double x) + x _0 by Def21 .= (x _0 + Double x) + Double x + x _0 by LATTICES:def 5 .= (x _0 + Double x) + (x + x) + x _0 by Def17 .= (x _0 + Double x) + x + 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 Def20 .= x _3 + (x + x _0) by LATTICES:def 5 .= x _3 + x _1 by Def18; end; theorem Th45: x _3 + x _0 = x _2 + x _1 proof thus x _3 + x _0 = x _0 + (Double x + x) + x _0 by Def20 .= (x _0 + Double x) + x + x _0 by LATTICES:def 5 .= x _2 + x + x _0 by Def19 .= x _2 + (x + x _0) by LATTICES:def 5 .= x _2 + x _1 by Def18; end; theorem Th46: x _3 + x = x _4 proof thus x _3 + x = x _0 + (Double x + x) + x by Def20 .= x _0 + (Double x + x + x) by LATTICES:def 5 .= x _0 + (Double x + (x + x)) by LATTICES:def 5 .= x _0 + (Double x + Double x) by Def17 .= x _4 by Def21; end; theorem Th47: :: Lemma 2 \delta (x _3, x _0) = x proof thus x = Expand (x _2, x) by Th38 .= \delta (x + x _2, \delta (x _2, x)) by Def15 .= \delta (x + x _2, x _0) by Th42 .= \delta (x _3, x _0) by Th43; end; theorem Th48: :: Left Argument Substitution -x = -y implies \delta (x, z) = \delta (y,z) proof assume A1: -x = -y; thus \delta (x, z) = -(-x + z) by Def14 .= \delta (y,z) by A1,Def14; end; theorem Th49: :: Exchange \delta (x, -y) = \delta (y, -x) proof thus \delta (x, -y) = -(-x + -y) by Def14 .= \delta (y, -x) by Def14; end; theorem Th50: :: Lemma 3 \delta (x _3, x) = x _0 proof A1: x = Expand (-x _3 + x _0, x) by Th38 .= \delta (-x _3 + x _0 + x, \delta (-x _3 + x _0, x)) by Def15 .= \delta (-x _3 + (x _0 + x), \delta (-x _3 + x _0, x)) by LATTICES:def 5 .= \delta (-x _3 + x _1, \delta (-x _3 + x _0, x)) by Def18 .= \delta (-x _3 + x _1, -(\delta (x _3, x _0) + x)) by Th39 .= \delta (-x _3 + x _1, -(x + x)) by Th47 .= \delta (-x _3 + x _1, -Double x) by Def17; A2: -Double x = Expand (-x _3 + x _1, -Double x) by Th38 .= \delta (-x _3 + x _1 + -Double x, x) by A1,Def15; set alpha = -x _3 + x _1 + -Double x; A3:-Double x = -(-alpha + x) by A2,Def14; A4:x = \delta (Double x, x _0) by Th41 .= \delta (-alpha + x, x _0) by A3,Th48; -x _3 = Expand (x _1 + -Double x, -x _3) by Th38 .= \delta (x _1 + -Double x + -x _3, \delta (x _1 + -Double x, -x _3)) by Def15 .= \delta (-x _3 + x _1 + -Double x, \delta (x _1 + -Double x, -x _3)) by LATTICES:def 5 .= \delta (alpha, \delta (x _3, -(x _1 + -Double x))) by Th49 .= \delta (alpha, \delta (x _3, \delta (Double x, x _1))) by Def14 .= \delta (alpha, \delta (x _0 + (x + Double x), \delta (Double x, x _1))) by Def20 .= \delta (alpha, \delta (x _0 + x + Double x, \delta (Double x, x _1))) by LATTICES:def 5 .= \delta (alpha, \delta (Double x + x _1, \delta (Double x, x _1))) by Def18 .= \delta (alpha, Expand (Double x, x _1)) by Def15 .= \delta (alpha, x _1) by Th38 .= -(-alpha + x _1) by Def14; hence \delta (x _3, x) = \delta (-alpha + x _1, x) by Th48 .= \delta (-alpha + (x _0 + x), x) by Def18 .= \delta (-alpha + x + x _0, \delta (-alpha + x, x _0)) by A4,LATTICES:def 5 .= Expand (-alpha + x, x _0) by Def15 .= x _0 by Th38; end; theorem Th51: :: Lemma 4 \delta (x _1 + x _3, x) = x _0 proof x _0 = Expand (x _4, x _0) by Th38 .= \delta (x _4 + x _0, \delta (x _4, x _0)) by Def15 .= \delta (x _4 + x _0, \delta (x _4, \delta (x _3, x))) by Th50 .= \delta (x _3 + x _1, \delta (x _4, \delta (x _3, x))) by Th44 .= \delta (x _3 + x _1, \delta (x _3 + x, \delta (x _3, x))) by Th46 .= \delta (x _3 + x _1, Expand (x _3, x)) by Def15 .= \delta (x _3 + x _1, x) by Th38; hence thesis; end; theorem Th52: :: Lemma 5 \delta (x _1 + x _2, x) = x _0 proof thus x _0 = Expand (x _3, x _0) by Th38 .= \delta (x _3 + x _0, \delta(x _3, x _0)) by Def15 .= \delta (x _1 + x _2, \delta(x _3, x _0)) by Th45 .= \delta (x _1 + x _2, x) by Th47; end; theorem Th53: :: Lemma 6 \delta (x _1 + x _3, x _0) = x proof thus x = Expand (x _1 + x _2, x) by Th38 .= \delta (x _1 + x _2 + x, \delta(x _1 + x _2, x)) by Def15 .= \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 Th43 .= \delta (x _1 + x _3, x _0) by Th52; end; definition let G, x; func \beta x -> Element of G equals :Def22: -(x _1 + x _3) + x + -(x _3); coherence; end; theorem Th54: :: Lemma 7 \delta (\beta x, x) = -x _3 proof thus -x _3 = \delta (-(x _1 + x _3) + x + -(x _3), \delta (-(x _1 + x _3) + x, -(x _3))) by Th37 .= \delta (\beta x, \delta (-(x _1 + x _3) + x, -(x _3))) by Def22 .= \delta (\beta x, \delta (x _3, -(-(x _1 + x _3) + x))) by Th49 .= \delta (\beta x, \delta (x _3, \delta (x _1 + x _3, x))) by Def14 .= \delta (\beta x, \delta (x _3, x _0)) by Th51 .= \delta (\beta x, x) by Th47; end; theorem Th55: :: Lemma 8 \delta (\beta x, x) = -(x _1 + x _3) proof thus -(x _1 + x _3) = \delta (-(x _1 + x _3) + (x + -(x _3)), \delta (x + -(x _3), -(x _1 + x _3))) by Th37 .=\delta (-(x _1 + x _3) + x + -(x _3), \delta (x + -(x _3), -(x _1 + x _3))) by LATTICES:def 5 .= \delta (\beta x, \delta (x + -(x _3), -(x _1 + x _3))) by Def22 .= \delta (\beta x, \delta (x _1 + x _3, -(x + -x _3))) by Th49 .= \delta (\beta x, \delta (x _1 + x _3, \delta (x _3, x))) by Def14 .= \delta (\beta x, \delta (x _1 + x _3, x _0)) by Th50 .= \delta (\beta x, x) by Th53; end; theorem :: Winker Second Condition ex y, z st -(y + z) = -z proof consider x; take y = x _1, z = x _3; -(y + z) = \delta (\beta x, x) by Th55 .= -z by Th54; hence thesis; end; begin :: Proofs according to Bill McCune theorem (for z holds --z = z) implies G is Huntington proof assume A1: for z holds --z = z; let x, y; A2: --(-(-x + -y) + -(x + -y)) = --y by Def5; -(-x + -y) + -(x + -y) = --(-(-x + -y) + -(x + -y)) by A1 .= y by A1,A2; hence thesis; end; theorem Th58: G is with_idempotent_element implies G is Huntington proof assume G is with_idempotent_element; then consider C being Element of G such that A1: C + C = C by Def13; assume G is non Huntington; then consider B, A being Element of G such that A2: -(-B + -A) + -(B + -A) <> A by Def12; A3: C = -(-C + -(C + -C)) by A1,Def5; A4: now let 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; end; A5: -(C + -(C + -C + -C)) = -C by A3,Def5; A6: C = -(-(C + C) + -(-C + -(C + -C) + C)) by A3,Def5 .= -(-C + -(C + -C + -(C + -C))) by A1,LATTICES:def 5; set D = C + -C + -C; -(-C + -(C + -C + -C)) = -(-(-(C + -C + -C) + C) + -(C + C + (-C + -C))) by A1,A5,LATTICES:def 5 .= -(-(-(C + -C + -C) + C) + -(C + (C + (-C + -C)))) by LATTICES:def 5 .= -(-(-D + C) + -(D + C)) by LATTICES:def 5 .= C by Def5; then -(C + -C) = -(C + -C + -C) by A5,Def5; then A7:C = C + -(C + -C) by A4,A5,A6; A8:now let x; thus x = -(-(C + -(C + -C) + x) + -(-C + -(C + -C) + x)) by A3,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; end; A9:now let x; thus -(C + -C) = -(-(-x + -(C + -C)) + -(x + -(C + -C))) by Def5 .= -(--x + -(x + -(C + -C))) by A8 .= -(--x + -x) by A8; end; A10:now let x; thus --x = -(-(-x + --x) + -(x + --x)) by Def5 .= -(-(C + -C) + -(x + --x)) by A9 .= --(x + --x) by A8; end; A11:now let x; thus -x = -(-(---x + -x) + -(--x + -x)) by Def5 .= -(-(---x + -x) + -(C + -C)) by A9 .= --(---x + -x) by A8 .= ---x by A10; end; A12:now let x, y; thus y = -(-(-x + y) + -(x + y)) by Def5 .= ---(-(-x + y) + -(x + y)) by A11 .= --y by Def5; end; now let x, y; thus -(-x + y) + -(x + y) = --(-(-x + y) + -(x + y)) by A12 .= -y by Def5; end; then -(-B + -A) + -(B + -A) = --A .= A by A12; hence thesis by A2; end; definition cluster TrivComplLat -> with_idempotent_element; coherence proof consider x be Element of TrivComplLat; take x; thus x = x + x by REALSET1:def 20; end; end; definition cluster with_idempotent_element -> Huntington (Robbins join-associative join-commutative (non empty ComplLattStr)); coherence by Th58; end; theorem Th59: (ex c, d being Element of G st c + d = c) implies G is Huntington proof given C, D being Element of G such that A1: C + D = C; A2: -(-C + -(D + -C)) = D by A1,Def5; A3: now let x, y; thus -(-(D + -(C + x) + y) + -(C + x + y)) = -(-(-(C + x) + (D + y)) + -(C + D + x + y)) by A1,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; end; A4: now let x, y, z; set k = -(-x + y) + -(x + y); thus -(-(-(-x + y) + -(x + y) + z) + -(y + z)) = -(-(k + z) + -(-k + z)) by Def5 .= z by Def5; end; A5: now let x, y, z; set k = -(-x + y); thus -(-(-(-x + y) + x + y) + y) = -(-(k + x + y) + -(k + -(x + y))) by Def5 .= -(-(k + (x + y)) + -(k + -(x + y))) by LATTICES:def 5 .= -(-x + y) by Def5; end; A6: now let x; thus D = -(-(-(-x + C) + -(x + C) + D) + -(C + D)) by A4 .= -(-C + -(D + -(C + -x) + -(C + x))) by A1,LATTICES:def 5; end; set E = D + -C; set L = -(D + -C); A7: -(D + -(C + -E)) = -E by A2,Def5; now thus -(L + -(C + L)) = -(-(D + -(C + L)) + -((D + C) + L)) by A1,A2,Def5 .= -(-(D + -(C + L)) + -(D + (C + L))) by LATTICES:def 5 .= D by Def5; end; then A8: -(D + -(D + -C + -(C + -(D + -C)))) = -(C + -(D + -C)) by Def5; set L = C + -(D + -C); A9: C = -(-(D + -L + C) + -(-(D + -C) + C)) by A7,Def5 .= -(-L + -(C + -L)) by A1,LATTICES:def 5; A10: now let x, y, z; set k = -(-x + y); -(-(k + x + y) + y) = k by A5; hence z = -(-(-(-(-x + y) + x + y) + y + z) + -(-(-x + y) + z)) by Def5; end; A11: -(C + -(D + -C)) = -(D + -(D + -(C + -(D + -C)) + -C)) by A8,LATTICES:def 5 .= -C by A2,A7,Def5; then A12: -(C + -(C + -(C + -C))) = -(C + -C) by A9,Def5; set K = -(C + C + -(C + -C)); K = -(C + -(C + -C) + C) by LATTICES:def 5; then C = -(-(C + -C) + K) by A12,Def5; then -(C + -(C + -C + K)) = K by Def5; then K = -(-(K + C + -C) + C) by LATTICES:def 5 .= -(-(-(-(C + -C) + C + C) + C + -C) + C) by LATTICES:def 5 .= -C by A9,A10,A11; then D + -(C + -C) = -(-(D + -(C + C) + -(C + -C)) + -C) by A3 .= -(-C + -(D + -(C + -C) + -(C + C))) by LATTICES:def 5 .= D by A6; then A13: C + -(C + -C) = C by A1,LATTICES:def 5; A14: now let x; thus x = -(-(C + -(C + -C) + x) + -(-C + -(C + -C) + x)) by A9,A11,A13, 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; end; set e = -(C + -C); e = e + e by A14; then G is with_idempotent_element by Def13; hence thesis by Th58; end; theorem Th60: ex y, z st y + z = z proof A1: now let x, 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; end; A2: now let x, 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; end; A3: now let 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 + (y + y)) + -(-x + y)) by LATTICES:def 5 .= -(-(-(-x + y) + x + Double y) + -(-x + y)) by Def17; end; A4: now let x, 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; end; A5:now let x, y, z; set k = -(-(-x + y) + x + Double y) + -(-x + y) + z; thus -(y + z) = -(-(-k + -(y + z)) + -(k + -(y + z))) by Def5 .= -(z + -(k + -(y + z))) by A4 .= -(-(-(-(-x + y) + x + Double y) + -(-x + y) + -(y + z) + z) + z) by LATTICES:def 5; end; A6: now let x, y, z, u; set k = -(-(-(-x + y) + x + Double y) + -(-x + y) + -(y + z) + z) + z; thus u = -(-(-k + u) + -(k + u)) by Def5 .= -(-(-(y + z) + u) + -(k + u)) by A5; end; A7: now let x, y, z, 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 + l) = -(-(-(Double v + v + l) + -(Double v + v) + l) + l) by A1 .= -(-(-(Double v + v + l) + l + -(Double v + v)) + l) by LATTICES:def 5; thus k = -(-(-(v + Double v) + k) + -((-(-(-(-(Double v + v) + v) + (Double v + v) + Double v) + -(-(Double v + v) + v) + -(v + Double v) + Double v) + Double v) + k)) by A6 .= -(-(-(v + Double v) + k) + -((-(-(Double v + v + k + Double v) + k + Double v + -(v + Double v)) + Double v) + k)) by LATTICES:def 5 .= -(-(-(v + Double v) + k) + -((-(-((Double v + v) + k + Double v) + (k + Double v) + -(v + Double v)) + Double v) + k)) by LATTICES:def 5 .= -(-(-(v + Double v) + k) + -((-(-(Double v + v + (k + Double v)) + l + -(v + Double v)) + Double v) + k)) by LATTICES:def 5 .= -(-(-(v + Double v) + k) + -(-(-(Double v + v + l) + l + -(v + Double v)) + l)) by LATTICES:def 5 .= -(-(-(Double v + v) + k) + -(Double v + v + Double v + k)) by A8,LATTICES:def 5 .= -(-(-(Double v + v) + k) + -(v5 + k)) by LATTICES:def 5; end; A9:now let 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) + k) + -(x + -(Double x + x))) by LATTICES:def 5 .= -(-(-(-(-(Double x + x) + x) + (Double x + x + Double x)) + k) + -(x + -(Double x + x))) by LATTICES:def 5 .= -(-(l + k) + -(x + -(Double x + x))) by LATTICES:def 5; l = -(-(-k + l) + -(k + l)) by Def5 .= -(-(-(Double x + x) + x) + -(k + l)) by A7; hence -(-(-(Double x + x) + x) + (Double x + Double x + x)) = -(Double x + x) by A10; end; A11:now let 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; end; A12: now let x; A13: -(-(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 + (x + x))) + x) by LATTICES:def 5 .= -(-(-(-(Double x + x) + x) + (Double x + Double x)) + x) by Def17; 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,A13; end; A14:now let 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 A12; end; A15: now let x, y; thus Double x = -(-(-(-(Double x + x) + x) + -(Double x + x) + Double x) + -(x + Double x)) by A14 .= -(-(Double x + x) + x) + Double x by A11; end; consider x; set c = Double x, d = -(-(Double x + x) + x); take d, c; thus thesis by A15; end; definition cluster Robbins -> Huntington (join-associative join-commutative (non empty ComplLattStr)); coherence proof let K be join-associative join-commutative (non empty ComplLattStr); assume A1: K is Robbins; then consider y, z be Element of K such that A2: y + z = z by Th60; thus thesis by A1,A2,Th59; end; end; definition let L be non empty OrthoLattStr; attr L is de_Morgan means :Def23: for x, y being Element of L holds x "/\" y = (x` "\/" y`)`; end; definition let L be non empty ComplLattStr; cluster CLatt L -> de_Morgan; coherence proof let x, y be Element of CLatt L; reconsider x' = x, y' = y as Element of L by Def11; x'` = x` & y'` = y` by Th35; then x'` "\/" y'` = x` "\/" y` by Th35; then (x'` "\/" y'`)` = (x` "\/" y`)` by Th35; then (x` "\/" y`)` = x' *' y' by Def4; hence thesis by Th35; end; end; theorem Th61: for L being well-complemented join-commutative meet-commutative (non empty OrthoLattStr), x being Element of L holds x + x` = Top L & x "/\" x` = Bottom L proof let L be well-complemented join-commutative meet-commutative (non empty OrthoLattStr), x be Element of L; A1: x` is_a_complement_of x by Def10; hence x + x` = Top L by LATTICES:def 18; thus thesis by A1,LATTICES:def 18; end; theorem Th62: for L being bounded distributive well-complemented preOrthoLattice holds (Top L)` = Bottom L proof let L be bounded distributive well-complemented preOrthoLattice; consider x being Element of L; (Top L)` = (x`` + x`)` by Th61 .= x` "/\" x by Th34 .= Bottom L by Th61; hence thesis; end; definition cluster TrivOrtLat -> de_Morgan; coherence proof let x, y be Element of TrivOrtLat; thus thesis by REALSET1:def 20; end; end; definition cluster strict de_Morgan Boolean Robbins Huntington preOrthoLattice; existence proof take TrivOrtLat; thus thesis; end; end; Lm1: for L being de_Morgan (non empty OrthoLattStr), a,b being Element of L holds a *' b = a "/\" b proof let L be de_Morgan (non empty OrthoLattStr), a,b be Element of L; thus a *' b = (a` "\/" b`)` by Def4 .= a "/\" b by Def23; end; definition cluster join-associative join-commutative de_Morgan -> meet-commutative (non empty OrthoLattStr); coherence proof let L be non empty OrthoLattStr; assume A1: L is join-associative join-commutative de_Morgan; let a,b be Element of L; thus a "/\" b = a *' b by A1,Lm1 .= b *' a by A1,Th8 .= b "/\" a by A1,Lm1; end; end; theorem Th63: for L being Huntington de_Morgan preOrthoLattice holds Bot L = Bottom L proof let L be Huntington de_Morgan preOrthoLattice; 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; reconsider a' = a as Element of L; thus C "/\" a = Bot L *' a' by Lm1 .= C by Def9; hence thesis; end; then L is lower-bounded by LATTICES:def 13; hence thesis by A1,LATTICES:def 16; end; definition cluster Boolean -> Huntington (well-complemented preOrthoLattice); coherence proof let L be well-complemented preOrthoLattice; assume A1: L is Boolean; then A2: L is bounded distributive complemented by LATTICES:def 20; reconsider L' = L as Boolean preOrthoLattice by A1; A3: for x being Element of L' holds Top L' "/\" x = x by LATTICES:43; now let x, y be Element of L; thus (x` "\/" y`)` "\/" (x` "\/" y)` = (x "/\" y) + (x` + y)` by A2,Th34 .= (x + (x` + y)`) "/\" (y + (x` + y)`) by A2,LATTICES:31 .= (x + (x` + y``)`) "/\" (y + (x` + y)`) by A2,Th33 .= (x + (x "/\" y`)) "/\" (y + (x` + y)`) by A2,Th34 .= x "/\" (y + (x` + y)`) by LATTICES:def 8 .= x "/\" (y + (x` + y``)`) by A2,Th33 .= x "/\" (y + (x "/\" y`)) by A2,Th34 .= x "/\" ((y + x) "/\" (y + y`)) by A2,LATTICES:31 .= (x "/\" (y + x)) "/\" (y + y`) by LATTICES:def 7 .= x "/\" (y + y`) by LATTICES:def 9 .= x "/\" Top L by Th61 .= x by A3; end; hence thesis by Def6; end; end; definition cluster Huntington -> Boolean (de_Morgan preOrthoLattice); coherence proof let L be de_Morgan preOrthoLattice; assume A1: L is Huntington; then reconsider L' = L as Huntington preOrthoLattice; thus L is bounded proof A2: L' is upper-bounded; L is lower-bounded proof set c' = Bot L'; reconsider c = c' as Element of L; take c; let a be Element of L; reconsider a' = a as Element of L'; thus c "/\" a = c' *' a' by Lm1 .= c by Def9; thus a "/\" c = c' *' a' by Lm1 .= c by Def9; end; hence thesis by A2,LATTICES:def 15; end; thus L is complemented proof let b be Element of L; take a = b`; A3: L' is join-idempotent; hence a + b = Top L by Def8; thus b + a = Top L by A3,Def8; thus a "/\" b = a *' b by Lm1 .= (a` + b`)` by Def4 .= Bot L' by Th9 .= Bottom L by Th63; hence b "/\" a = Bottom L; end; thus L is distributive proof let a, b, c be Element of L; A4: a "/\" b = a *' b & a "/\" c = a *' c by Lm1; thus a "/\" (b "\/" c) = a *' (b + c) by Lm1 .= (a "/\" b) "\/" (a "/\" c) by A1,A4,Th31; end; end; end; definition cluster Robbins de_Morgan -> Boolean preOrthoLattice; coherence proof let L be preOrthoLattice; assume L is Robbins de_Morgan; then reconsider L' = L as Robbins de_Morgan preOrthoLattice; thus L is bounded proof L' is upper-bounded; hence thesis; end; now let b be Element of L'; take a = b`; thus a + b = Top L' by Def8; thus a "/\" b = a *' b by Lm1 .= (a` + b`)` by Def4 .= Bot L' by Th9 .= Bottom L' by Th63; end; hence L is complemented; now let a, b, c be Element of L'; A1: a "/\" b = a *' b & a "/\" c = a *' c by Lm1; thus a "/\" (b "\/" c) = a *' (b + c) by Lm1 .= (a "/\" b) "\/" (a "/\" c) by A1,Th31; end; hence L is distributive; end; cluster Boolean -> Robbins (well-complemented preOrthoLattice); coherence proof let L be well-complemented preOrthoLattice; assume L is Boolean; then reconsider L' = L as Boolean well-complemented preOrthoLattice; now let x, y be Element of L'; thus ((x + y)` + (x + y`)`)` = (x + y) "/\" (x + y`) by Th34 .= ((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 Th34 .= 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 L')` by Th61 .= x + Bottom L' by Th62 .= x by LATTICES:39; end; hence thesis by Def5; end; end;