### The Mizar article:

### Introduction to Lattice Theory

**by****Stanislaw Zukowski**

- Received April 14, 1989
Copyright (c) 1989 Association of Mizar Users

- MML identifier: LATTICES
- [ MML identifier index ]

environ vocabulary BINOP_1, BOOLE, FINSUB_1, FUNCT_1, SUBSET_1, LATTICES; notation XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, BINOP_1, FINSUB_1; constructors STRUCT_0, BINOP_1, FINSUB_1, XBOOLE_0; clusters FINSUB_1, STRUCT_0, SUBSET_1, ZFMISC_1, XBOOLE_0; requirements SUBSET, BOOLE; theorems TARSKI, ZFMISC_1, STRUCT_0, FINSUB_1; begin definition struct(1-sorted) /\-SemiLattStr (# carrier -> set, L_meet -> BinOp of the carrier #); end; definition struct(1-sorted) \/-SemiLattStr (# carrier -> set, L_join -> BinOp of the carrier #); end; definition struct(/\-SemiLattStr,\/-SemiLattStr) LattStr (# carrier -> set, L_join, L_meet -> BinOp of the carrier #); end; set DD=bool {}; DD is preBoolean proof now let X,Y be set; assume X in DD & Y in DD; then reconsider X'=X,Y'=Y as Element of DD; X' \/ Y' in DD & X' \ Y' in DD; hence X \/ Y in DD & X \ Y in DD; end; hence thesis by FINSUB_1:10; end; then reconsider DD as non empty preBoolean set; consider uu,nn being BinOp of DD; set GG=LattStr(#DD,uu,nn#); set GGj=\/-SemiLattStr(#DD,uu#); set GGm=/\-SemiLattStr(#DD,uu#); Lm1: GG is strict non empty by STRUCT_0:def 1; Lm2: GGj is strict non empty by STRUCT_0:def 1; Lm3: GGm is strict non empty by STRUCT_0:def 1; definition cluster strict non empty \/-SemiLattStr; existence by Lm2; cluster strict non empty /\-SemiLattStr; existence by Lm3; cluster strict non empty LattStr; existence by Lm1; end; reconsider GG as strict non empty LattStr by STRUCT_0:def 1; reconsider GGj as strict non empty \/-SemiLattStr by STRUCT_0:def 1; reconsider GGm as strict non empty /\-SemiLattStr by STRUCT_0:def 1; definition let G be non empty \/-SemiLattStr, p, q be Element of G; func p"\/"q -> Element of G equals (the L_join of G).(p,q); coherence; end; definition let G be non empty /\-SemiLattStr, p, q be Element of G; func p"/\"q -> Element of G equals (the L_meet of G).(p,q); coherence; end; definition let G be non empty \/-SemiLattStr, p, q be Element of G; pred p [= q means :Def3: p"\/"q = q; end; Lm4: for x,y being Element of GG holds x = y proof let x,y be Element of GG; x = {} & y = {} by TARSKI:def 1,ZFMISC_1:1; hence thesis; end; Lm5: for x,y being Element of GGj holds x = y proof let x,y be Element of GGj; x = {} & y = {} by TARSKI:def 1,ZFMISC_1:1; hence thesis; end; Lm6: for x,y being Element of GGm holds x = y proof let x,y be Element of GGm; x = {} & y = {} by TARSKI:def 1,ZFMISC_1:1; hence thesis; end; Lm7: for x,y being Element of GG holds x"\/"y = y"\/"x by Lm4; Lm8: for x,y being Element of GGj holds x"\/"y = y"\/"x by Lm5; Lm9: for x,y being Element of GGm holds x"/\"y = y"/\"x by Lm6; Lm10: for x,y,z being Element of GG holds x"\/"(y"\/"z) = (x"\/"y)"\/"z by Lm4; Lm11: for x,y,z being Element of GGj holds x"\/"(y"\/"z) = (x"\/"y)"\/"z by Lm5; Lm12: for x,y,z being Element of GGm holds x"/\"(y"/\"z) = (x"/\"y)"/\"z by Lm6; Lm13: for x,y being Element of GG holds (x"/\"y)"\/"y = y by Lm4; Lm14: for x,y being Element of GG holds x"/\"y = y"/\"x by Lm4; Lm15: for x,y,z being Element of GG holds x"/\"(y"/\"z) = (x"/\"y)"/\"z by Lm4; Lm16: for x,y being Element of GG holds x"/\"(x"\/"y) = x by Lm4; Lm17: for x,y,z being Element of GG holds x"/\"(y"\/"z) = (x"/\"y)"\/"(x"/\"z) by Lm4; Lm18: for x,y,z being Element of GG holds x [= z implies x"\/"(y"/\"z) = (x"\/"y)"/\"z by Lm4; reconsider 0_GG={} as Element of GG by ZFMISC_1:def 1; reconsider D={} as Element of GG by ZFMISC_1:def 1; Lm19: for x being Element of GG holds 0_GG"/\"x = 0_GG & x"/\"0_GG = 0_GG by Lm4; Lm20: for x being Element of GG holds D"\/"x = D & x"\/"D = D by Lm4; definition let IT be non empty \/-SemiLattStr; attr IT is join-commutative means :Def4: for a,b being Element of IT holds a"\/"b = b"\/"a; attr IT is join-associative means :Def5: for a,b,c being Element of IT holds a"\/"(b"\/"c) = (a"\/"b) "\/"c; end; definition let IT be non empty /\-SemiLattStr; attr IT is meet-commutative means :Def6: for a,b being Element of IT holds a"/\"b = b"/\"a; attr IT is meet-associative means :Def7: for a,b,c being Element of IT holds a"/\"(b"/\"c) = (a"/\"b) "/\"c; end; definition let IT be non empty LattStr; attr IT is meet-absorbing means :Def8: for a,b being Element of IT holds (a"/\"b)"\/"b = b; attr IT is join-absorbing means :Def9: for a,b being Element of IT holds a"/\"(a"\/"b)=a; end; definition let IT be non empty LattStr; attr IT is Lattice-like means :Def10: IT is join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing; end; definition cluster Lattice-like -> join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing (non empty LattStr); coherence by Def10; cluster join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing -> Lattice-like (non empty LattStr); coherence by Def10; end; definition cluster strict join-commutative join-associative (non empty \/-SemiLattStr); existence proof GGj is join-commutative join-associative by Def4,Def5,Lm8,Lm11; hence thesis; end; cluster strict meet-commutative meet-associative (non empty /\-SemiLattStr); existence proof GGm is meet-commutative meet-associative by Def6,Def7,Lm9,Lm12; hence thesis; end; cluster strict Lattice-like (non empty LattStr); existence proof GG is join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing by Def4,Def5,Def6,Def7,Def8,Def9,Lm7,Lm10,Lm13,Lm14,Lm15,Lm16; then GG is Lattice-like by Def10; hence thesis; end; end; definition mode Lattice is Lattice-like (non empty LattStr); end; GG is join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing by Def4,Def5,Def6,Def7,Def8,Def9,Lm7,Lm10,Lm13,Lm14,Lm15,Lm16; then reconsider GG as Lattice by Def10; definition let L be join-commutative (non empty \/-SemiLattStr), a, b be Element of L; redefine func a"\/"b; commutativity by Def4; end; definition let L be meet-commutative (non empty /\-SemiLattStr), a, b be Element of L; redefine func a"/\"b; commutativity by Def6; end; definition let IT be non empty LattStr; attr IT is distributive means :Def11: for a,b,c being Element of IT holds a"/\"(b"\/"c) = (a"/\"b)"\/"(a"/\"c); end; Lm21: GG is distributive by Def11,Lm17; definition let IT be non empty LattStr; attr IT is modular means :Def12: for a,b,c being Element of IT st a [= c holds a"\/"(b"/\"c) = (a"\/"b)"/\"c; end; definition let IT be non empty /\-SemiLattStr; attr IT is lower-bounded means :Def13: ex c being Element of IT st for a being Element of IT holds c"/\"a = c & a"/\"c = c; end; definition let IT be non empty \/-SemiLattStr; attr IT is upper-bounded means :Def14: ex c being Element of IT st for a being Element of IT holds c"\/"a = c & a"\/"c = c; end; definition cluster strict distributive lower-bounded upper-bounded modular Lattice; existence proof A1: GG is modular by Def12,Lm18; A2: GG is lower-bounded by Def13,Lm19; GG is upper-bounded by Def14,Lm20; hence thesis by A1,A2,Lm21; end; end; definition mode D_Lattice is distributive Lattice; mode M_Lattice is modular Lattice; mode 0_Lattice is lower-bounded Lattice; mode 1_Lattice is upper-bounded Lattice; end; Lm22: GG is 0_Lattice by Def13,Lm19; Lm23: GG is 1_Lattice by Def14,Lm20; definition let IT be non empty LattStr; attr IT is bounded means :Def15: IT is lower-bounded upper-bounded; end; definition cluster lower-bounded upper-bounded -> bounded (non empty LattStr); coherence by Def15; cluster bounded -> lower-bounded upper-bounded (non empty LattStr); coherence by Def15; end; definition cluster bounded strict Lattice; existence proof GG is 0_Lattice & GG is 1_Lattice by Def13,Def14,Lm19,Lm20; then GG is bounded by Def15; hence thesis; end; end; definition mode 01_Lattice is bounded Lattice; end; definition let L be non empty /\-SemiLattStr; assume A1: L is lower-bounded; func Bottom L -> Element of L means :Def16: for a being Element of L holds it "/\" a = it & a "/\" it = it; existence by A1,Def13; uniqueness proof let c1,c2 be Element of L such that A2: for a being Element of L holds c1"/\"a = c1 & a"/\"c1 = c1 and A3: for a being Element of L holds c2"/\"a = c2 & a"/\"c2 = c2; thus c1 = c2"/\"c1 by A2 .= c2 by A3; end; end; definition let L be non empty \/-SemiLattStr; assume A1: L is upper-bounded; func Top L -> Element of L means :Def17: for a being Element of L holds it "\/" a = it & a "\/" it = it; existence by A1,Def14; uniqueness proof let c1,c2 be Element of L such that A2: for a being Element of L holds c1"\/"a = c1 & a"\/" c1 = c1 and A3: for a being Element of L holds c2"\/"a = c2 & a"\/"c2 = c2; thus c1 = c2"\/"c1 by A2 .= c2 by A3; end; end; definition let L be non empty LattStr, a, b be Element of L; pred a is_a_complement_of b means :Def18: a"\/"b = Top L & b"\/"a = Top L & a"/\"b = Bottom L & b"/\"a = Bottom L; end; definition let IT be non empty LattStr; attr IT is complemented means :Def19: for b being Element of IT ex a being Element of IT st a is_a_complement_of b; end; definition cluster bounded complemented strict Lattice; existence proof take GG; thus GG is bounded by Def15,Lm22,Lm23; thus GG is complemented proof let b be Element of GG; consider a being Element of GG; take a; thus a"\/"b = Top GG & b"\/"a = Top GG by Lm4; thus a"/\"b = Bottom GG & b"/\"a = Bottom GG by Lm4; end; thus thesis; end; end; definition mode C_Lattice is complemented 01_Lattice; end; reconsider GG as 01_Lattice by Def15,Lm22,Lm23; Lm24: GG is complemented proof let b be Element of GG; take b; thus b"\/"b = Top GG & b"\/"b = Top GG by Lm4; thus b"/\"b = Bottom GG & b"/\"b = Bottom GG by Lm4; end; definition let IT be non empty LattStr; attr IT is Boolean means :Def20: IT is bounded complemented distributive; end; definition cluster Boolean -> bounded complemented distributive (non empty LattStr); coherence by Def20; cluster bounded complemented distributive -> Boolean (non empty LattStr); coherence by Def20; end; definition cluster Boolean strict Lattice; existence proof reconsider GG as C_Lattice by Lm24; GG is Boolean by Def20,Lm21; hence thesis; end; end; definition mode B_Lattice is Boolean Lattice; end; reserve L for meet-absorbing join-absorbing meet-commutative (non empty LattStr); reserve a for Element of L; canceled 16; theorem Th17: a"\/"a = a proof thus a"\/"a = ( a "/\" ( a"\/"a ) ) "\/" a by Def9 .= a by Def8; end; theorem a"/\"a = a proof a"/\"( a"\/"a ) = a by Def9; hence thesis by Th17; end; reserve L for Lattice; reserve a, b, c for Element of L; theorem Th19: (for a,b,c holds a"/\"(b"\/"c) = (a"/\"b)"\/"(a"/\"c)) iff (for a,b,c holds a"\/"(b"/\"c) = (a"\/"b)"/\"(a"\/"c)) proof hereby assume A1:for a,b,c holds a"/\"(b"\/"c)=(a"/\"b)"\/"(a"/\"c); let a,b,c; thus a"\/"(b"/\"c)=(a"\/"(c"/\"a))"\/"(c"/\"b) by Def8 .=a"\/"((c"/\"a)"\/"(c"/\"b)) by Def5 .=a"\/"((a"\/"b)"/\"c) by A1 .=((a"\/"b)"/\"a)"\/"((a"\/"b)"/\"c) by Def9 .=(a"\/"b)"/\"(a"\/"c) by A1; end; assume A2:for a,b,c holds a"\/"(b"/\"c)=(a"\/"b)"/\"(a"\/"c); let a,b,c; thus a"/\"(b"\/"c)=(a"/\"(c"\/"a))"/\"(c"\/"b) by Def9 .=a"/\"((c"\/"a)"/\"(c"\/"b)) by Def7 .=a"/\"((a"/\"b)"\/"c) by A2 .=((a"/\"b)"\/"a)"/\"((a"/\"b)"\/"c) by Def8 .=(a"/\"b)"\/"(a"/\"c) by A2; end; canceled; theorem Th21: for L being meet-absorbing join-absorbing (non empty LattStr), a, b being Element of L holds a [= b iff a"/\"b = a proof let L be meet-absorbing join-absorbing (non empty LattStr), a, b be Element of L; a [= b iff a"\/"b = b by Def3; hence thesis by Def8,Def9; end; theorem Th22: for L being meet-absorbing join-absorbing join-associative meet-commutative (non empty LattStr), a, b being Element of L holds a [= a"\/"b proof let L be meet-absorbing join-absorbing join-associative meet-commutative (non empty LattStr), a, b be Element of L; thus a"\/"( a"\/"b) = (a"\/"a)"\/"b by Def5 .= a"\/"b by Th17; end; theorem Th23: for L being meet-absorbing meet-commutative (non empty LattStr), a, b being Element of L holds a"/\"b [= a proof let L be meet-absorbing meet-commutative (non empty LattStr), a, b be Element of L; thus ( a"/\"b )"\/"a = a by Def8; end; definition let L be meet-absorbing join-absorbing meet-commutative (non empty LattStr), a, b be Element of L; redefine pred a [= b; reflexivity proof let a be Element of L; thus a"\/"a = a by Th17; end; end; canceled; theorem for L being join-associative (non empty \/-SemiLattStr), a, b, c being Element of L holds a [= b & b [= c implies a [= c proof let L be join-associative (non empty \/-SemiLattStr), a, b, c be Element of L; assume a"\/"b = b & b"\/"c = c; hence a"\/"c = c by Def5; end; theorem Th26: for L being join-commutative (non empty \/-SemiLattStr), a, b being Element of L holds a [= b & b [= a implies a=b proof let L be join-commutative (non empty \/-SemiLattStr), a, b be Element of L; assume a"\/"b = b & b"\/"a =a; hence thesis; end; theorem Th27: for L being meet-absorbing join-absorbing meet-associative (non empty LattStr), a, b, c being Element of L holds a [= b implies a"/\"c [= b"/\"c proof let L be meet-absorbing join-absorbing meet-associative (non empty LattStr), a, b, c be Element of L; assume a [= b; hence (a"/\"c)"\/"(b"/\"c) = ((a"/\"b)"/\"c)"\/"(b"/\"c) by Th21 .= (a"/\"(b"/\"c))"\/"(b"/\"c) by Def7 .= b"/\"c by Def8; end; canceled; theorem for L being Lattice holds (for a,b,c being Element of L holds (a"/\"b)"\/"(b"/\"c)"\/"(c"/\"a) = (a"\/"b)"/\"(b"\/"c)"/\"(c"\/"a)) implies L is distributive proof let L be Lattice; assume A1: for a,b,c being Element of L holds (a"/\"b)"\/"(b"/\"c)"\/"(c"/\"a) = (a"\/"b)"/\"(b"\/"c)"/\"(c"\/"a); A2: now let a,b,c be Element of L; assume A3: c [= a; thus a"/\"(b"\/"c) = (b"\/"c)"/\"(a"/\"(a"\/"b)) by Def9 .= (a"\/"b)"/\"((b"\/"c)"/\"a) by Def7 .= (a"\/"b)"/\"((b"\/"c)"/\"(c"\/"a)) by A3,Def3 .= (a"\/"b)"/\"(b"\/"c)"/\"(c"\/"a) by Def7 .= (a"/\"b)"\/"(b"/\"c)"\/"(c"/\"a) by A1 .= (a"/\"b)"\/"((b"/\"c)"\/"(c"/\"a)) by Def5 .= (a"/\"b)"\/"((b"/\"c)"\/"c) by A3,Th21 .= (a"/\"b)"\/"c by Def8; end; let a,b,c be Element of L; A4: (a"/\"b)"\/"(c"/\"a) [= a proof thus ((a"/\"b)"\/"(c"/\"a))"\/"a = (a"/\"b)"\/"((c"/\"a)"\/"a) by Def5 .= (a"/\"b)"\/"a by Def8 .= a by Def8; end; thus a"/\"(b"\/"c) = (a"/\"(c"\/"a))"/\"(b"\/"c) by Def9 .= a"/\"((c"\/"a)"/\"(b"\/"c)) by Def7 .= (a"/\"(a"\/"b))"/\"((c"\/"a)"/\"(b"\/"c)) by Def9 .= a"/\"((a"\/"b)"/\"((b"\/"c)"/\"(c"\/"a))) by Def7 .= a"/\"((a"\/"b)"/\"(b"\/"c)"/\"(c"\/"a)) by Def7 .= a"/\"((b"/\"c)"\/"(a"/\"b)"\/"(c"/\"a)) by A1 .= a"/\"((b"/\"c)"\/"((a"/\"b)"\/"(c"/\"a))) by Def5 .= (a"/\"(b"/\"c))"\/"((a"/\"b)"\/"(c"/\"a)) by A2,A4 .= (a"/\"b"/\"c)"\/"((a"/\"b)"\/"(c"/\"a)) by Def7 .= ((a"/\"b"/\"c)"\/"(a"/\"b))"\/"(c"/\"a) by Def5 .= (a"/\"b)"\/"(a"/\"c) by Def8; end; reserve L for D_Lattice; reserve a, b, c for Element of L; canceled; theorem Th31: a"\/"(b"/\"c) = (a"\/"b)"/\"(a"\/"c) proof for a,b,c holds a"/\"(b"\/"c) = (a"/\"b)"\/"(a"/\"c) by Def11; hence thesis by Th19; end; theorem Th32: c"/\"a = c"/\"b & c"\/"a = c"\/"b implies a=b proof assume that A1: c"/\"a = c"/\"b and A2: c"\/"a = c"\/"b; thus a = a"/\"( c"\/"a ) by Def9 .= ( b"/\"c )"\/"( b"/\"a ) by A1,A2,Def11 .= b"/\"( c"\/"a ) by Def11 .= b by A2,Def9; end; canceled; theorem (a"\/"b)"/\"(b"\/"c)"/\"(c"\/"a) = (a"/\"b)"\/"(b"/\"c)"\/"(c"/\"a) proof thus (a"\/"b)"/\"(b"\/"c)"/\"(c"\/"a) = (((a"\/"b)"/\"(b"\/"c))"/\"c)"\/"(((a"\/"b)"/\"(b"\/"c))"/\"a) by Def11 .= ((a"\/"b)"/\"((b"\/"c)"/\"c))"\/"(((a"\/"b)"/\"(b"\/"c))"/\"a) by Def7 .= ((a"\/"b)"/\"c)"\/"(a"/\"((a"\/"b)"/\"(b"\/"c))) by Def9 .= ((a"\/"b)"/\"c)"\/"((a"/\"(a"\/"b))"/\"(b"\/"c)) by Def7 .= (c"/\"(a"\/"b))"\/"(a"/\"(b"\/"c)) by Def9 .= ((c"/\"a)"\/"(c"/\"b))"\/"(a"/\"(b"\/"c)) by Def11 .= ((a"/\"b)"\/"(c"/\"a))"\/"((c"/\"a)"\/"(b"/\"c)) by Def11 .= (a"/\"b)"\/"((c"/\"a)"\/"((c"/\"a)"\/"(b"/\"c))) by Def5 .= (a"/\"b)"\/"(((c"/\"a)"\/"(c"/\"a))"\/"(b"/\"c)) by Def5 .= (a"/\"b)"\/"((b"/\"c)"\/"(c"/\"a)) by Th17 .= (a"/\"b)"\/"(b"/\"c)"\/"(c"/\"a) by Def5; end; definition cluster distributive -> modular Lattice; coherence proof let L be Lattice; assume A1: L is distributive; let a,b,c be Element of L; assume a"\/"c = c; hence a"\/"(b"/\"c) = (a"\/"b)"/\"c by A1,Th31; end; end; reserve L for 0_Lattice; reserve a for Element of L; canceled 4; theorem Th39: Bottom L"\/"a = a proof thus Bottom L"\/"a = ( Bottom L"/\"a )"\/"a by Def16 .= a by Def8; end; theorem Bottom L"/\"a = Bottom L by Def16; theorem Th41: Bottom L [= a proof Bottom L [= Bottom L"\/"a by Th22; hence thesis by Th39; end; reserve L for 1_Lattice; reserve a for Element of L; canceled; theorem Th43: Top L"/\"a = a proof thus Top L"/\"a = ( Top L"\/"a )"/\"a by Def17 .= a by Def9; end; theorem Top L"\/"a = Top L by Def17; theorem a [= Top L proof Top L"/\"a [= Top L by Th23; hence thesis by Th43; end; definition let L be non empty LattStr, x be Element of L; assume A1: L is complemented D_Lattice; func x` -> Element of L means :Def21: it is_a_complement_of x; existence by A1,Def19; uniqueness proof let a,b be Element of L such that A2: a is_a_complement_of x and A3: b is_a_complement_of x; A4: a"\/"x = Top L & x"\/"a = Top L & a"/\"x = Bottom L & x"/\"a = Bottom L by A2,Def18; b"\/"x = Top L & b"/\"x = Bottom L & x"\/"b = Top L & x"/\"b = Bottom L by A3,Def18; hence thesis by A1,A4,Th32; end; end; reserve L for B_Lattice; reserve a, b for Element of L; canceled; theorem Th47: a`"/\"a = Bottom L proof a` is_a_complement_of a by Def21; hence thesis by Def18; end; theorem Th48: a`"\/"a = Top L proof a` is_a_complement_of a by Def21; hence thesis by Def18; end; theorem Th49: a`` = a proof a`` is_a_complement_of a` by Def21; then A1: a``"\/"a` = Top L & a``"/\"a` = Bottom L by Def18; a` is_a_complement_of a by Def21; then a"\/"a` =Top L & a "/\"a`= Bottom L by Def18; hence a``= a by A1,Th32; end; theorem Th50: ( a"/\"b )` = a`"\/" b` proof A1: (a`"\/"b`)"\/"(a"/\"b) = a`"\/"(b`"\/"(a"/\"b)) by Def5 .= a`"\/"((b`"\/"a)"/\"(b`"\/"b)) by Th31 .= a`"\/"((b`"\/"a)"/\"Top L) by Th48 .= (b`"\/"a)"\/"a` by Th43 .= b`"\/"(a"\/"a`) by Def5 .= b`"\/"Top L by Th48 .= Top L by Def17; (a`"\/"b`)"/\"(a"/\"b) = ((a`"\/"b`)"/\"a)"/\"b by Def7 .= ((a`"/\"a)"\/"(b`"/\"a))"/\"b by Def11 .= (Bottom L"\/"(b`"/\"a))"/\"b by Th47 .= b"/\"(b`"/\"a) by Th39 .= (b"/\"b`)"/\"a by Def7 .= Bottom L"/\"a by Th47 .= Bottom L by Def16; then a`"\/"b` is_a_complement_of a"/\"b by A1,Def18; hence thesis by Def21; end; theorem ( a"\/"b )` = a`"/\" b` proof thus (a"\/"b)` = (a``"\/"b)` by Th49 .= (a``"\/"b``)` by Th49 .= (a`"/\"b`)`` by Th50 .= a`"/\"b` by Th49; end; theorem Th52: b"/\"a = Bottom L iff b [= a` proof thus b"/\"a = Bottom L implies b [= a` proof assume A1: b"/\"a = Bottom L; b = b"/\"Top L by Th43 .= b"/\"(a"\/"a`) by Th48 .= Bottom L"\/"(b"/\"a`) by A1,Def11 .= b"/\"a` by Th39; then b"\/"a` = a` by Def8; hence b [= a` by Def3; end; thus thesis proof assume b [= a`; then b"/\"a [= a`"/\"a by Th27; then A2: b"/\"a [= Bottom L by Th47; Bottom L [= b"/\"a by Th41; hence b"/\"a = Bottom L by A2,Th26; end; end; theorem a [= b implies b` [= a` proof assume a [= b; then b`"/\"a [= b`"/\"b by Th27; then A1: b`"/\"a [= Bottom L by Th47; Bottom L [= b`"/\"a by Th41; then b `"/\"a = Bottom L by A1,Th26; hence b` [= a` by Th52; end;

Back to top