:: Orthomodular Lattices
:: by El\.zbieta M\c{a}dra and Adam Grabowski
::
:: Received June 27, 2008
:: Copyright (c) 2008-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, LATTICES, LATTICE3, SUBSET_1, FILTER_1, PBOOLE, EQREL_1,
ZFMISC_1, ROBBINS3, XBOOLE_0, ROBBINS1, OPOSET_1, ORDERS_2, YELLOW_1,
CARD_1, RELAT_2, TARSKI, STRUCT_0, XXREAL_0, FILTER_0, FUNCT_1, BINOP_1,
RVSUM_1, SYMSP_1, ROBBINS4;
notations TARSKI, XBOOLE_0, ZFMISC_1, ENUMSET1, SUBSET_1, BINOP_1, FUNCT_1,
ORDINAL1, CARD_1, NUMBERS, FUNCT_2, STRUCT_0, LATTICE3, LATTICES,
ORDERS_2, ROBBINS1, YELLOW_1, ROBBINS3;
constructors BINOP_1, REALSET2, LATTICE3, ROBBINS3, YELLOW_1, RELSET_1;
registrations SUBSET_1, RELAT_1, STRUCT_0, LATTICES, YELLOW_1, ROBBINS1,
SHEFFER1, ROBBINS3, XBOOLE_0, ORDINAL1;
requirements SUBSET, BOOLE, NUMERALS, REAL;
definitions LATTICES, TARSKI, ROBBINS3, ROBBINS1, LATTICE3;
equalities LATTICES, ROBBINS1, SUBSET_1, LATTICE3, ORDINAL1;
expansions LATTICES, TARSKI, ROBBINS3, ROBBINS1;
theorems ZFMISC_1, STRUCT_0, LATTICE3, FILTER_1, LATTICES, FUNCT_2, ROBBINS3,
ROBBINS1, FILTER_0, YELLOW11, XBOOLE_1, TARSKI, ENUMSET1, XBOOLE_0,
SUBSET_1, YELLOW_1, CARD_1, NAT_1, RELSET_1, YELLOW_0;
schemes FUNCT_2;
begin :: Preliminaries
registration
let L be Lattice;
cluster the LattStr of L -> Lattice-like;
coherence by ROBBINS3:15;
end;
theorem Th1:
for K,L being Lattice st the LattStr of K = the LattStr of L
holds LattPOSet K = LattPOSet L
proof
let K, L be Lattice;
assume
A1: the LattStr of K = the LattStr of L;
for p, q being Element of K holds [p,q] in LattRel K iff [p,q] in LattRel L
proof
let p,q be Element of K;
reconsider p9 = p, q9 = q as Element of L by A1;
hereby
assume [p,q] in LattRel K;
then p [= q by FILTER_1:31;
then p "\/" q = q;
then p9 "\/" q9 = q9 by A1;
then p9 [= q9;
hence [p,q] in LattRel L by FILTER_1:31;
end;
assume [p,q] in LattRel L;
then p9 [= q9 by FILTER_1:31;
then p9 "\/" q9 = q9;
then p "\/" q = q by A1;
then p [= q;
hence thesis by FILTER_1:31;
end;
hence thesis by A1,RELSET_1:def 2;
end;
registration
cluster -> meet-Absorbing for 1-element OrthoLattStr;
coherence;
end;
registration
cluster -> lower-bounded for Ortholattice;
coherence
proof
let IT be Ortholattice;
ex c being Element of IT st for a being Element of IT holds c "/\" a =
c & a "/\" c = c
proof
set x = the Element of IT;
take c = (x`` "\/" x`)`;
let a be Element of IT;
thus c "/\" a = (a`` "\/" a`)` "/\" a by ROBBINS3:def 7
.= (a` "/\" a) "/\" a by ROBBINS1:def 23
.= a` "/\" (a "/\" a) by LATTICES:def 7
.= a` "/\" a
.= (a`` "\/" a`)` by ROBBINS1:def 23
.= c by ROBBINS3:def 7;
hence thesis;
end;
hence thesis;
end;
cluster -> upper-bounded for Ortholattice;
coherence
proof
let IT be Ortholattice;
ex c being Element of IT st for a being Element of IT holds c "\/" a =
c & a "\/" c = c
proof
set x = the Element of IT;
take c = x` "\/" x;
let a be Element of IT;
c "\/" a = (a` "\/" a) "\/" a by ROBBINS3:def 7
.= a` "\/" (a "\/" a) by LATTICES:def 5
.= a` "\/" a
.= c by ROBBINS3:def 7;
hence thesis;
end;
hence thesis;
end;
end;
reserve L for Ortholattice,
a, b, c for Element of L;
theorem Th2:
a "\/" a` = Top L & a "/\" a` = Bottom L
proof
A1: (a "\/" a`) "\/" b = a "\/" a`
proof
thus (a "\/" a`) "\/" b = (b "\/" b`) "\/" b by ROBBINS3:def 7
.= b` "\/" (b "\/" b) by LATTICES:def 5
.= b` "\/" b
.= a "\/" a` by ROBBINS3:def 7;
end;
then b "\/" (a "\/" a`) = a "\/" a`;
hence a "\/" a` = Top L by A1,LATTICES:def 17;
A2: (a "/\" a`) "/\" b = a "/\" a`
proof
thus (a "/\" a`) "/\" b = (a` "\/" a``)` "/\" b by ROBBINS1:def 23
.= (b` "\/" b``)` "/\" b by ROBBINS3:def 7
.= (b "/\" b`) "/\" b by ROBBINS1:def 23
.= b` "/\" (b "/\" b) by LATTICES:def 7
.= b` "/\" b
.= (b`` "\/" b`)` by ROBBINS1:def 23
.= (a`` "\/" a`)` by ROBBINS3:def 7
.= a "/\" a` by ROBBINS1:def 23;
end;
then b "/\" (a "/\" a`) = a "/\" a`;
hence thesis by A2,LATTICES:def 16;
end;
theorem Th3:
for L being non empty OrthoLattStr holds L is Ortholattice iff (
for a, b, c being Element of L holds (a "\/" b) "\/" c = (c` "/\" b`)` "\/" a)
& (for a, b being Element of L holds a = a "/\" (a "\/" b)) & for a, b being
Element of L holds a = a "\/" (b "/\" b`)
proof
let L be non empty OrthoLattStr;
thus L is Ortholattice implies (for a, b, c being Element of L holds (a "\/"
b) "\/" c = (c` "/\" b`)` "\/" a) & (for a, b being Element of L holds a = a
"/\" (a "\/" b)) & for a, b being Element of L holds a = a "\/" (b "/\" b`)
proof
assume
A1: L is Ortholattice;
thus for a, b, c being Element of L holds (a "\/" b) "\/" c = (c` "/\" b`)
` "\/" a
proof
let a,b,c be Element of L;
(c` "/\" b`)` "\/" a=((c`` "\/" b``)`)` "\/" a by A1,ROBBINS1:def 23;
then (c` "/\" b`)` "\/" a=((c "\/" b``)`)` "\/" a by A1,ROBBINS3:def 6;
then (c` "/\" b`)` "\/" a=(c "\/" b)`` "\/" a by A1,ROBBINS3:def 6;
then (c` "/\" b`)` "\/" a=(c "\/" b) "\/" a by A1,ROBBINS3:def 6;
then (c` "/\" b`)` "\/" a=a "\/" (c "\/" b) by A1,LATTICES:def 4;
then (c` "/\" b`)` "\/" a=c "\/" (a "\/" b) by A1,ROBBINS3:def 1;
hence thesis by A1,LATTICES:def 4;
end;
thus for a, b being Element of L holds a = a "/\" (a "\/" b) by A1,
LATTICES:def 9;
let a,b be Element of L;
thus a "\/" (b "/\" b`) = a "\/" (b` "\/" b``)` by A1,ROBBINS1:def 23
.= a "\/" (b` "\/" b)` by A1,ROBBINS3:def 6
.= a "\/" (b "\/" b`)` by A1,LATTICES:def 4
.= a "\/" (a "\/" a`)` by A1,ROBBINS3:def 7
.= a "\/" (a`` "\/" a`)` by A1,ROBBINS3:def 6
.= a "\/" (a` "/\" a) by A1,ROBBINS1:def 23
.= (a` "/\" a)"\/"a by A1,LATTICES:def 4
.= a by A1,LATTICES:def 8;
end;
assume
A2: for a, b, c being Element of L holds (a "\/" b) "\/" c = (c` "/\" b`
)` "\/" a;
assume
A3: for a, b being Element of L holds a = a "/\" (a "\/" b);
assume
A4: for a, b being Element of L holds a = a "\/" (b "/\" b`);
A5: for a being Element of L holds a "/\" a = a
proof
let a be Element of L;
thus a "/\" a = a "/\" (a "\/" (a "/\" a`)) by A4
.= a by A3;
end;
A6: for a,b being Element of L holds a = (b "/\" b`)`` "\/" a
proof
let a,b be Element of L;
set x = b "/\" b`;
(a "\/" x) "\/" x = (x` "/\" x`)` "\/" a by A2;
then (a "\/" x) "\/" x = x`` "\/" a by A5;
then a "\/" x = x`` "\/" a by A4;
hence thesis by A4;
end;
A7: for a being Element of L holds a "/\" a` = (a "/\" a`)``
proof
let a be Element of L;
set x = a "/\" a`;
thus x = x`` "\/" x by A6
.= x`` by A4;
end;
A8: for a,b being Element of L holds a = (b "/\" b`) "\/" a
proof
let a,b be Element of L;
a = (b "/\" b`)`` "\/" a by A6;
hence thesis by A7;
end;
A9: for a,b being Element of L holds a "\/" b = (b` "/\" a`)`
proof
let a,b be Element of L;
set x = a "/\" a`;
(x "\/" a) "\/" b = (b` "/\" a`)` "\/" x by A2;
hence a "\/" b = (b` "/\" a`)` "\/" x by A8
.= (b` "/\" a`)` by A4;
end;
A10: L is involutive
proof
let a be Element of L;
a` = a` "/\" (a` "\/" a) & a` "\/" a = (a` "/\" a``)` by A3,A9;
hence a`` = (a` "/\" a``) "\/" a by A9
.= a by A8;
end;
A11: L is join-commutative
proof
let a,b be Element of L;
set x = a "/\" a`;
x "\/" b = (b` "/\" x`)` by A9;
hence b "\/" a = (b` "/\" x`)` "\/" a by A8
.= (a "\/" x) "\/" b by A2
.= a "\/" b by A4;
end;
A12: L is de_Morgan
proof
let a,b be Element of L;
thus (a` "\/" b`)` = (b` "\/" a`)` by A11
.= (a`` "/\" b``)`` by A9
.= a`` "/\" b`` by A10
.= a`` "/\" b by A10
.= a "/\" b by A10;
end;
A13: L is meet-absorbing
proof
let a,b be Element of L;
thus (a "/\" b) "\/" b = (b` "/\" (a "/\" b)`)` by A9
.= (b` "/\" (a` "\/" b`)``)` by A12
.= (b` "/\" (a` "\/" b`))` by A10
.= (b` "/\" (b` "\/" a`))` by A11
.= b`` by A3
.= b by A10;
end;
A14: L is join-associative
proof
let a,b,c be Element of L;
thus (a "\/" b) "\/" c = (c` "/\" b`)` "\/" a by A2
.= (b "\/" c) "\/" a by A9
.= a "\/" (b "\/" c) by A11;
end;
A15: L is meet-associative
proof
let a,b,c be Element of L;
thus a "/\" (b "/\" c) = (a` "\/" (b "/\" c)`)` by A12
.= (a` "\/" (b` "\/" c`)``)` by A12
.= (a` "\/" (b` "\/" c`))` by A10
.= ((a` "\/" b`) "\/" c`)` by A14
.= ((a` "\/" b`)`` "\/" c`)` by A10
.= ((a "/\" b)` "\/" c`)` by A12
.= (a "/\" b) "/\" c by A12;
end;
A16: for a,b being Element of L holds a "/\" a` = b "/\" b`
proof
let a,b be Element of L;
a "/\" a` = (a "/\" a`) "\/" (b "/\" b`) by A4;
hence thesis by A8;
end;
A17: L is with_Top
proof
let a,b be Element of L;
(a` "/\" a``)` = (b` "/\" b``)` by A16;
then (a` "/\" a``)` = b` "\/" b by A9;
then a` "\/" a = b` "\/" b by A9;
then a` "\/" a = b "\/" b` by A11;
hence thesis by A11;
end;
L is join-absorbing by A3;
hence thesis by A11,A14,A10,A12,A17,A15,A13;
end;
theorem Th4:
for L being involutive Lattice-like non empty OrthoLattStr
holds L is de_Morgan iff for a,b being Element of L st a [= b holds b` [= a`
proof
let L be involutive Lattice-like non empty OrthoLattStr;
thus L is de_Morgan implies for a,b being Element of L st a [= b holds b` [=
a`
proof
assume
A1: L is de_Morgan;
let a,b be Element of L;
assume a [= b;
then a` = (a"/\"b)` by LATTICES:4
.= (a`"\/"b`)`` by A1
.= b`"\/"a` by ROBBINS3:def 6;
then a` "/\" b` = b` by LATTICES:def 9;
hence thesis by LATTICES:4;
end;
assume
A2: for a,b being Element of L st a [= b holds b` [= a`;
let x,y be Element of L;
(x` "\/" y`)` [= y`` by A2,LATTICES:5;
then
A3: (x` "\/" y`)` [= y by ROBBINS3:def 6;
x` [= (x "/\" y)` & y` [= (x "/\" y)` by A2,LATTICES:6;
then x` "\/" y` [= (x "/\" y)` by FILTER_0:6;
then (x "/\" y)`` [= (x` "\/" y`)` by A2;
then
A4: x "/\" y [= (x` "\/" y`)` by ROBBINS3:def 6;
(x` "\/" y`)` [= x`` by A2,LATTICES:5;
then (x` "\/" y`)` [= x by ROBBINS3:def 6;
then (x` "\/" y`)` [= x "/\" y by A3,FILTER_0:7;
hence thesis by A4,LATTICES:8;
end;
begin :: Orthomodularity
definition
let L be non empty OrthoLattStr;
attr L is orthomodular means
:Def1:
for x, y being Element of L st x [= y holds y = x "\/" (x` "/\" y);
end;
registration
cluster trivial orthomodular modular Boolean for Ortholattice;
existence
proof
set L = the 1-element Ortholattice;
L is orthomodular
by STRUCT_0:def 10;
hence thesis;
end;
end;
theorem Th5:
for L being modular Ortholattice holds L is orthomodular
proof
let L be modular Ortholattice;
let x, y be Element of L;
assume x [= y;
then x "\/" (x` "/\" y) = (x "\/" x`) "/\" y by LATTICES:def 12;
then x "\/" (x` "/\" y) = (y "\/" y`) "/\" y by ROBBINS3:def 7;
hence thesis by LATTICES:def 9;
end;
definition
mode Orthomodular_Lattice is orthomodular Ortholattice;
end;
theorem Th6:
for L being orthomodular meet-absorbing join-absorbing
join-associative meet-commutative non empty OrthoLattStr, x, y being Element
of L holds x "\/" (x` "/\" (x "\/" y)) = x "\/" y
by LATTICES:5,Def1;
definition
let L be non empty OrthoLattStr;
attr L is Orthomodular means
:Def2:
for x, y being Element of L holds x "\/" (x` "/\" (x "\/" y)) = x "\/" y;
end;
registration
cluster Orthomodular -> orthomodular for meet-absorbing join-absorbing
join-associative meet-commutative non empty OrthoLattStr;
coherence
proof
let L be meet-absorbing join-absorbing join-associative meet-commutative
non empty OrthoLattStr;
assume
A1: L is Orthomodular;
let x, y be Element of L;
assume x [= y;
then x "\/" y = y;
hence thesis by A1;
end;
cluster orthomodular -> Orthomodular for meet-absorbing join-absorbing
join-associative meet-commutative non empty OrthoLattStr;
coherence
by Th6;
end;
registration
cluster modular -> orthomodular for Ortholattice;
coherence by Th5;
end;
registration
cluster join-Associative meet-Absorbing de_Morgan orthomodular for
Ortholattice;
existence
proof
set L = the 1-element Ortholattice;
take L;
thus thesis;
end;
end;
begin :: Examples: The Benzene Ring
definition
func B_6 -> RelStr equals
InclPoset { 0, 1, 3 \ 1, 2, 3 \ 2, 3 };
coherence;
end;
registration
cluster B_6 -> non empty;
coherence;
cluster B_6 -> reflexive transitive antisymmetric;
coherence;
end;
Lm1: 3 \ 2 misses 2 by XBOOLE_1:79;
Lm2: Segm 1 c= Segm 2 by NAT_1:39;
then
Lm3: 3 \ 2 misses 1 by Lm1,XBOOLE_1:63;
registration
cluster B_6 -> with_suprema with_infima;
coherence
proof
set N = B_6;
set Z = {0, 1, 3 \ 1, 2, 3 \ 2, 3};
A1: the carrier of N = {0, 1, 3 \ 1, 2, 3 \ 2, 3} by YELLOW_1:1;
A2: N is with_suprema
proof
let x,y be Element of N;
A3: Z = the carrier of N by YELLOW_1:1;
thus ex z being Element of N st x <= z & y <= z & for z9 being Element
of N st x <= z9 & y <= z9 holds z <= z9
proof
per cases by A3,ENUMSET1:def 4;
suppose
x = 0 & y = 0;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by YELLOW_1:3;
end;
suppose
x = 0 & y = 3\1;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by YELLOW_1:3;
end;
suppose
x = 0 & y = 2;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by YELLOW_1:3;
end;
suppose
x = 0 & y = 3\2;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by YELLOW_1:3;
end;
suppose
x = 0 & y = 3;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by YELLOW_1:3;
end;
suppose
x = 3\1 & y = 0;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by YELLOW_1:3;
end;
suppose
x = 3\1 & y = 3\1;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by YELLOW_1:3;
end;
suppose
A4: x = 3\1 & y = 2;
3 in Z by ENUMSET1:def 4;
then reconsider z = 3 as Element of N by YELLOW_1:1;
take z;
Segm 2 c= Segm 3 by NAT_1:39;
hence x <= z & y <= z by A4,YELLOW_1:3;
let z9 be Element of N;
assume that
A5: x <= z9 and
A6: y <= z9;
A7: z9 is Element of Z by YELLOW_1:1;
A8: 3\1 c= z9 by A4,A5,YELLOW_1:3;
A9: now
assume z9 = 2;
then
A10: not 2 in z9;
2 in 3\1 by TARSKI:def 2,YELLOW11:3;
hence contradiction by A8,A10;
end;
A11: Segm 2 c= z9 by A4,A6,YELLOW_1:3;
A12: now
A13: 0 in 2 by CARD_1:50,TARSKI:def 2;
assume z9 = 3\1;
hence contradiction by A11,A13,TARSKI:def 2,YELLOW11:3;
end;
A14: now
A15: Segm 1 in Segm 2 by CARD_1:50,TARSKI:def 2;
assume z9 = 3\2;
hence contradiction by A11,A15,TARSKI:def 1,YELLOW11:4;
end;
1 in 2 & 0 in 2 by TARSKI:def 2,CARD_1:50;
then 1 in z9 & 0 in z9 by A11;
then z9 <> 1 & z9 <> 0;
hence thesis by A7,A12,A9,A14,ENUMSET1:def 4;
end;
suppose
x = 1 & y = 0;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by YELLOW_1:3;
end;
suppose
x = 1 & y = 1;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by YELLOW_1:3;
end;
suppose
A16: x = 1 & y = 3\1;
A17: Segm 1 c= Segm 3 by NAT_1:39;
1 \/ (3\1) = 1 \/ 3 by XBOOLE_1:39
.= 3 by A17,XBOOLE_1:12;
then reconsider z = x \/ y as Element of N by A1,A16,ENUMSET1:def 4;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by YELLOW_1:3;
end;
suppose
A18: x = 1 & y = 3\2;
3 in Z by ENUMSET1:def 4;
then reconsider z = 3 as Element of N by YELLOW_1:1;
take z;
Segm 1 c= Segm 3 by NAT_1:39;
hence x <= z & y <= z by A18,YELLOW_1:3;
let z9 be Element of N;
assume that
A19: x <= z9 and
A20: y <= z9;
A21: 3\2 c= z9 by A18,A20,YELLOW_1:3;
A22: now
A23: 2 in 3\2 by TARSKI:def 1,YELLOW11:4;
assume z9 = 1;
hence contradiction by A21,A23,CARD_1:49,TARSKI:def 1;
end;
A24: now
assume z9 = 2;
then
A25: not 2 in z9;
2 in 3\2 by TARSKI:def 1,YELLOW11:4;
hence contradiction by A21,A25;
end;
A26: 1 c= z9 by A18,A19,YELLOW_1:3;
A27: now
A28: 0 in 1 by CARD_1:49,TARSKI:def 1;
assume z9 = 3\1;
hence contradiction by A26,A28,TARSKI:def 2,YELLOW11:3;
end;
A29: now
A30: 0 in 1 by CARD_1:49,TARSKI:def 1;
assume z9 = 3\2;
hence contradiction by A26,A30,TARSKI:def 1,YELLOW11:4;
end;
z9 is Element of Z & z9 <> 0 by A26,YELLOW_1:1;
hence thesis by A27,A24,A29,A22,ENUMSET1:def 4;
end;
suppose
A31: x = 1 & y = 3;
Segm 1 c= Segm 3 by NAT_1:39;
then reconsider z = x \/ y as Element of N by A31,XBOOLE_1:12;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by YELLOW_1:3;
end;
suppose
A32: x = 1 & y = 2;
Segm 1 c= Segm 2 by NAT_1:39;
then reconsider z = x \/ y as Element of N by A32,XBOOLE_1:12;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by YELLOW_1:3;
end;
suppose
y = 1 & x = 0;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by YELLOW_1:3;
end;
suppose
y = 1 & x = 1;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by YELLOW_1:3;
end;
suppose
A33: y = 1 & x = 3\1;
A34: Segm 1 c= Segm 3 by NAT_1:39;
1 \/ (3\1) = 1 \/ 3 by XBOOLE_1:39
.= 3 by A34,XBOOLE_1:12;
then reconsider z = x \/ y as Element of N by A1,A33,ENUMSET1:def 4;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by YELLOW_1:3;
end;
suppose
A35: y = 1 & x = 3\2;
3 in Z by ENUMSET1:def 4;
then reconsider z = 3 as Element of N by YELLOW_1:1;
take z;
Segm 1 c= Segm 3 by NAT_1:39;
hence x <= z & y <= z by A35,YELLOW_1:3;
let z9 be Element of N;
assume that
A36: x <= z9 and
A37: y <= z9;
A38: 3\2 c= z9 by A35,A36,YELLOW_1:3;
A39: now
A40: 2 in 3\2 by TARSKI:def 1,YELLOW11:4;
assume z9 = 1;
hence contradiction by A38,A40,CARD_1:49,TARSKI:def 1;
end;
A41: now
assume z9 = 2;
then
A42: not 2 in z9;
2 in 3\2 by TARSKI:def 1,YELLOW11:4;
hence contradiction by A38,A42;
end;
A43: 1 c= z9 by A35,A37,YELLOW_1:3;
A44: now
A45: 0 in 1 by CARD_1:49,TARSKI:def 1;
assume z9 = 3\1;
hence contradiction by A43,A45,TARSKI:def 2,YELLOW11:3;
end;
A46: now
A47: 0 in 1 by CARD_1:49,TARSKI:def 1;
assume z9 = 3\2;
hence contradiction by A43,A47,TARSKI:def 1,YELLOW11:4;
end;
z9 is Element of Z & z9 <> 0 by A43,YELLOW_1:1;
hence thesis by A44,A41,A46,A39,ENUMSET1:def 4;
end;
suppose
A48: y = 1 & x = 3;
Segm 1 c= Segm 3 by NAT_1:39;
then reconsider z = x \/ y as Element of N by A48,XBOOLE_1:12;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by YELLOW_1:3;
end;
suppose
A49: y = 1 & x = 2;
Segm 1 c= Segm 2 by NAT_1:39;
then reconsider z = x \/ y as Element of N by A49,XBOOLE_1:12;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by YELLOW_1:3;
end;
suppose
x = 3\1 & y = 3\2;
then reconsider z = x \/ y as Element of N by Lm2,XBOOLE_1:12,34;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by YELLOW_1:3;
end;
suppose
x = 3\1 & y = 3;
then reconsider z = x \/ y as Element of N by XBOOLE_1:12;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by YELLOW_1:3;
end;
suppose
x = 2 & y = 0;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by YELLOW_1:3;
end;
suppose
A50: x = 2 & y = 3\1;
3 in Z by ENUMSET1:def 4;
then reconsider z = 3 as Element of N by YELLOW_1:1;
take z;
Segm 2 c= Segm 3 by NAT_1:39;
hence x <= z & y <= z by A50,YELLOW_1:3;
let z9 be Element of N;
assume that
A51: x <= z9 and
A52: y <= z9;
A53: z9 is Element of Z by YELLOW_1:1;
A54: 3\1 c= z9 by A50,A52,YELLOW_1:3;
A55: now
assume z9 = 2;
then
A56: not 2 in z9;
2 in 3\1 by TARSKI:def 2,YELLOW11:3;
hence contradiction by A54,A56;
end;
A57: 2 c= z9 by A50,A51,YELLOW_1:3;
A58: now
A59: 0 in 2 by CARD_1:50,TARSKI:def 2;
assume z9 = 3\1;
hence contradiction by A57,A59,TARSKI:def 2,YELLOW11:3;
end;
A60: now
A61: 1 in 2 by CARD_1:50,TARSKI:def 2;
assume z9 = 3\2;
hence contradiction by A57,A61,TARSKI:def 1,YELLOW11:4;
end;
1 in 2 & 0 in 2 by CARD_1:50,TARSKI:def 2;
then 1 in z9 & 0 in z9 by A57;
then z9 <> 1 & z9 <> 0;
hence thesis by A53,A58,A55,A60,ENUMSET1:def 4;
end;
suppose
x = 2 & y = 2;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by YELLOW_1:3;
end;
suppose
A62: x = 2 & y = 3\2;
A63: Segm 2 c= Segm 3 by NAT_1:39;
2 \/ (3\2) = 2 \/ 3 by XBOOLE_1:39
.= 3 by A63,XBOOLE_1:12;
then x \/ y in Z by A62,ENUMSET1:def 4;
then reconsider z = x \/ y as Element of N by YELLOW_1:1;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by YELLOW_1:3;
end;
suppose
A64: x = 2 & y = 3;
Segm 2 c= Segm 3 by NAT_1:39;
then reconsider z = x \/ y as Element of N by A64,XBOOLE_1:12;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by YELLOW_1:3;
end;
suppose
x = 3\2 & y = 0;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by YELLOW_1:3;
end;
suppose
x = 3\2 & y = 3\1;
then reconsider z = x \/ y as Element of N by Lm2,XBOOLE_1:12,34;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by YELLOW_1:3;
end;
suppose
A65: x = 3\2 & y = 2;
A66: Segm 2 c= Segm 3 by NAT_1:39;
2 \/ (3\2) = 2 \/ 3 by XBOOLE_1:39
.= 3 by A66,XBOOLE_1:12;
then x \/ y in Z by A65,ENUMSET1:def 4;
then reconsider z = x \/ y as Element of N by YELLOW_1:1;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by YELLOW_1:3;
end;
suppose
x = 3\2 & y = 3\2;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by YELLOW_1:3;
end;
suppose
x = 3\2 & y = 3;
then reconsider z = x \/ y as Element of N by XBOOLE_1:12;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by YELLOW_1:3;
end;
suppose
x = 3 & y = 0;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by YELLOW_1:3;
end;
suppose
x = 3 & y = 3\1;
then reconsider z = x \/ y as Element of N by XBOOLE_1:12;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by YELLOW_1:3;
end;
suppose
A67: x = 3 & y = 2;
Segm 2 c= Segm 3 by NAT_1:39;
then reconsider z = x \/ y as Element of N by A67,XBOOLE_1:12;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by YELLOW_1:3;
end;
suppose
x = 3 & y = 3\2;
then reconsider z = x \/ y as Element of N by XBOOLE_1:12;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by YELLOW_1:3;
end;
suppose
x = 3 & y = 3;
then reconsider z = x \/ y as Element of N;
take z;
x c= z & y c= z by XBOOLE_1:7;
hence x <= z & y <= z by YELLOW_1:3;
let w be Element of N;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence thesis by YELLOW_1:3;
end;
end;
end;
N is with_infima
proof
let x,y be Element of N;
A68: Z = the carrier of N by YELLOW_1:1;
thus ex z being Element of N st z <= x & z <= y & for z9 being Element
of N st z9 <= x & z9 <= y holds z9 <= z
proof
per cases by A68,ENUMSET1:def 4;
suppose
x = 0 & y = 0;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
x = 0 & y = 3\1;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
x = 0 & y = 2;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
x = 0 & y = 3\2;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
x = 0 & y = 3;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
x = 3\1 & y = 0;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
x = 3\1 & y = 3\1;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
A69: x = 3\1 & y = 2;
0 in Z by ENUMSET1:def 4;
then reconsider z = 0 as Element of N by YELLOW_1:1;
take z;
z c= x & z c= y;
hence z <= x & z <= y by YELLOW_1:3;
let z9 be Element of N;
assume that
A70: z9 <= x and
A71: z9 <= y;
A72: z9 c= 3\1 by A69,A70,YELLOW_1:3;
A73: now
assume z9= 2;
then 0 in z9 by CARD_1:50,TARSKI:def 2;
hence contradiction by A72,TARSKI:def 2,YELLOW11:3;
end;
A74: z9 c= 2 by A69,A71,YELLOW_1:3;
A75: now
assume z9= 3\1;
then
A76: 2 in z9 by TARSKI:def 2,YELLOW11:3;
not 2 in 2;
hence contradiction by A74,A76;
end;
A77: now
assume z9= 3;
then
A78: 2 in z9 by CARD_1:51,ENUMSET1:def 1;
not 2 in 2;
hence contradiction by A74,A78;
end;
A79: now
assume z9= 3\2;
then
A80: 2 in z9 by TARSKI:def 1,YELLOW11:4;
not 2 in 2;
hence contradiction by A74,A80;
end;
A81: now
assume z9= 1;
then 0 in z9 by CARD_1:49,TARSKI:def 1;
hence contradiction by A72,TARSKI:def 2,YELLOW11:3;
end;
z9 is Element of Z by YELLOW_1:1;
hence thesis by A75,A73,A79,A81,A77,ENUMSET1:def 4;
end;
suppose
x = 1 & y = 0;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
x = 1 & y = 1;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
x = 1 & y = 3\1;
then x misses y by XBOOLE_1:79;
then x /\ y = 0 by XBOOLE_0:def 7;
then reconsider z = x /\ y as Element of N by A1,ENUMSET1:def 4;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
x = 1 & y = 3\2;
then x /\ y = 0 by Lm3,XBOOLE_0:def 7;
then reconsider z = x /\ y as Element of N by A1,ENUMSET1:def 4;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
A82: x = 1 & y = 3;
Segm 1 c= Segm 3 by NAT_1:39;
then reconsider z = x /\ y as Element of N by A82,XBOOLE_1:28;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
x = 1 & y = 2;
then reconsider z = x /\ y as Element of N by CARD_1:49,50
,ZFMISC_1:13;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
y = 1 & x = 0;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
y = 1 & x = 1;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
y = 1 & x = 3\1;
then x misses y by XBOOLE_1:79;
then x /\ y = 0 by XBOOLE_0:def 7;
then reconsider z = x /\ y as Element of N by A1,ENUMSET1:def 4;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
y = 1 & x = 3\2;
then x /\ y = {} by Lm3,XBOOLE_0:def 7;
then reconsider z = x /\ y as Element of N by A1,ENUMSET1:def 4;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
A83: y = 1 & x = 3;
Segm 1 c= Segm 3 by NAT_1:39;
then reconsider z = x /\ y as Element of N by A83,XBOOLE_1:28;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
y = 1 & x = 2;
then reconsider z = x /\ y as Element of N by CARD_1:49,50
,ZFMISC_1:13;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
x = 3\1 & y = 3\2;
then reconsider z = x /\ y as Element of N by YELLOW11:3,4
,ZFMISC_1:13;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
A84: x = 3\1 & y = 3;
(3\1) /\ 3 = (3 /\ 3) \ 1 by XBOOLE_1:49
.= 3\1;
then reconsider z = x /\ y as Element of N by A84;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
x = 2 & y = 0;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
A85: x = 2 & y = 3\1;
0 in Z by ENUMSET1:def 4;
then reconsider z = 0 as Element of N by YELLOW_1:1;
take z;
z c= x & z c= y;
hence z <= x & z <= y by YELLOW_1:3;
let z9 be Element of N;
assume that
A86: z9 <= x and
A87: z9 <= y;
A88: z9 c= 3\1 by A85,A87,YELLOW_1:3;
A89: now
assume z9= 2;
then 0 in z9 by CARD_1:50,TARSKI:def 2;
hence contradiction by A88,TARSKI:def 2,YELLOW11:3;
end;
A90: z9 c= 2 by A85,A86,YELLOW_1:3;
A91: now
assume z9= 3\1;
then
A92: 2 in z9 by TARSKI:def 2,YELLOW11:3;
not 2 in 2;
hence contradiction by A90,A92;
end;
A93: now
assume z9= 3;
then
A94: 2 in z9 by CARD_1:51,ENUMSET1:def 1;
not 2 in 2;
hence contradiction by A90,A94;
end;
A95: now
assume z9= 3\2;
then
A96: 2 in z9 by TARSKI:def 1,YELLOW11:4;
not 2 in 2;
hence contradiction by A90,A96;
end;
A97: now
assume z9= 1;
then 0 in z9 by CARD_1:49,TARSKI:def 1;
hence contradiction by A88,TARSKI:def 2,YELLOW11:3;
end;
z9 is Element of Z by YELLOW_1:1;
hence thesis by A91,A89,A95,A93,A97,ENUMSET1:def 4;
end;
suppose
x = 2 & y = 2;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
A98: x = 2 & y = 3\2;
2 misses (3\2) by XBOOLE_1:79;
then 2 /\ (3\2) = 0 by XBOOLE_0:def 7;
then x /\ y in Z by A98,ENUMSET1:def 4;
then reconsider z = x /\ y as Element of N by YELLOW_1:1;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
A99: x = 2 & y = 3;
Segm 2 c= Segm 3 by NAT_1:39;
then reconsider z = x /\ y as Element of N by A99,XBOOLE_1:28;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
x = 3\2 & y = 0;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
x = 3\2 & y = 3\1;
then reconsider z = x /\ y as Element of N by YELLOW11:3,4
,ZFMISC_1:13;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
A100: x = 3\2 & y = 2;
2 misses (3\2) by XBOOLE_1:79;
then 2 /\ (3\2) = 0 by XBOOLE_0:def 7;
then x /\ y in Z by A100,ENUMSET1:def 4;
then reconsider z = x /\ y as Element of N by YELLOW_1:1;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
x = 3\2 & y = 3\2;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
A101: x = 3\2 & y = 3;
(3\2) /\ 3 = (3 /\ 3) \2 by XBOOLE_1:49
.= 3\2;
then reconsider z = x /\ y as Element of N by A101;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
x = 3 & y = 0;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
A102: x = 3 & y = 3\1;
(3\1) /\ 3 = (3 /\ 3) \ 1 by XBOOLE_1:49
.= 3\1;
then reconsider z = x /\ y as Element of N by A102;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
A103: x = 3 & y = 2;
Segm 2 c= Segm 3 by NAT_1:39;
then reconsider z = x /\ y as Element of N by A103,XBOOLE_1:28;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
A104: x = 3 & y = 3\2;
(3\2) /\ 3 = (3 /\ 3) \2 by XBOOLE_1:49
.= 3\2;
then reconsider z = x /\ y as Element of N by A104;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
suppose
x = 3 & y = 3;
then reconsider z = x /\ y as Element of N;
take z;
z c= x & z c= y by XBOOLE_1:17;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of N;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence thesis by YELLOW_1:3;
end;
end;
end;
hence thesis by A2;
end;
end;
theorem Th7:
the carrier of latt B_6 = { 0, 1, 3 \ 1, 2, 3 \ 2, 3 }
proof
the RelStr of B_6 = LattPOSet latt B_6 by LATTICE3:def 15;
hence thesis by YELLOW_1:1;
end;
theorem Th8:
for a being set st a in the carrier of latt B_6 holds a c= Segm 3
proof
let a be set;
assume a in the carrier of latt B_6;
then a = 0 or a = Segm 1 or a = 3 \ 1 or a = Segm 2 or a = 3 \ 2 or a = 3
by Th7,ENUMSET1:def 4;
hence thesis by NAT_1:39;
end;
definition
func Benzene -> strict OrthoLattStr means
:Def4:
the LattStr of it = latt
B_6 & for x being Element of it, y being Subset of 3 st x = y
holds (the Compl of it).x = y`;
existence
proof
defpred P[set,set] means for y being Subset of 3 st $1 = y holds $2 = y`;
set N = latt B_6;
set M = the carrier of N;
set A = the L_join of N, B = the L_meet of N;
A1: for x being Element of M ex y being Element of M st P[x,y]
proof
let x be Element of M;
reconsider z = x as Subset of 3 by Th8;
A2: Segm 2 c= Segm 3 by NAT_1:39;
A3: Segm 1 c= Segm 3 by NAT_1:39;
now
per cases by Th7,ENUMSET1:def 4;
suppose
z = 0;
hence z` in M by Th7,ENUMSET1:def 4;
end;
suppose
z = 1;
hence z` in M by Th7,ENUMSET1:def 4;
end;
suppose
z = 3\1;
then z` = 3 /\ 1 by XBOOLE_1:48
.= 1 by A3,XBOOLE_1:28;
hence z` in M by Th7,ENUMSET1:def 4;
end;
suppose
z = 3\2;
then z` = 3 /\ 2 by XBOOLE_1:48
.= 2 by A2,XBOOLE_1:28;
hence z` in M by Th7,ENUMSET1:def 4;
end;
suppose
z = 2;
hence z` in M by Th7,ENUMSET1:def 4;
end;
suppose
z = 3;
then z` = 0 by XBOOLE_1:37;
hence z` in M by Th7,ENUMSET1:def 4;
end;
end;
then reconsider y = z` as Element of M;
take y;
thus thesis;
end;
ex f being Function of M,M st for x being Element of M holds P[x,f.x]
from FUNCT_2:sch 3(A1);
then consider C being UnOp of M such that
A4: for x being Element of M, y being Subset of 3 st x = y holds C.x = y`;
take OrthoLattStr (#M, A, B, C#);
thus thesis by A4;
end;
uniqueness
proof
let A1, A2 be strict OrthoLattStr such that
A5: the LattStr of A1 = latt B_6 and
A6: for x being Element of A1, y being Subset of 3 st
x = y holds (the Compl of A1).x = y` and
A7: the LattStr of A2 = latt B_6 and
A8: for x being Element of A2, y being Subset of 3 st
x = y holds (the Compl of A2).x = y`;
set f2 = the Compl of A2;
set f1 = the Compl of A1;
set M = the carrier of A1;
for x being Element of M holds f1.x = f2.x
proof
let x be Element of M;
reconsider y = x as Subset of 3 by A5,Th8;
thus f1.x = y` by A6
.= f2.x by A5,A7,A8;
end;
hence thesis by A5,A7,FUNCT_2:63;
end;
end;
theorem Th9:
the carrier of Benzene = { 0, 1, 3 \ 1, 2, 3 \ 2, 3 }
proof
the LattStr of Benzene = the LattStr of latt B_6 & LattPOSet latt B_6 =
the RelStr of B_6 by Def4,LATTICE3:def 15;
hence thesis by YELLOW_1:1;
end;
theorem Th10:
the carrier of Benzene c= bool 3
proof
let a be object;
A1: 0 c= 3 & Segm 1 c= Segm 3 by NAT_1:39;
assume
A2: a in the carrier of Benzene;
A3: Segm 2 c= Segm 3 & 3 c= 3 by NAT_1:39;
a = 0 or a = 1 or a = 3 \ 1 or a = 2 or a = 3 \ 2 or a = 3 by A2,Th9,
ENUMSET1:def 4;
hence thesis by A1,A3;
end;
theorem Th11:
for a being set st a in the carrier of Benzene holds a c= {0,1,2
} by Th10,CARD_1:51;
registration
cluster Benzene -> non empty;
coherence by Th9;
cluster Benzene -> Lattice-like;
coherence
proof
the LattStr of Benzene = latt B_6 by Def4;
hence thesis by ROBBINS3:15;
end;
end;
theorem Th12:
LattPOSet the LattStr of Benzene = B_6
proof
LattPOSet the LattStr of Benzene = LattPOSet latt B_6 by Def4;
hence thesis by LATTICE3:def 15;
end;
theorem Th13:
for a, b being Element of B_6, x, y being Element of Benzene st
a = x & b = y holds a <= b iff x [= y
proof
let a, b be Element of B_6, x, y be Element of Benzene;
assume
A1: a = x & b = y;
hereby
assume a <= b;
then x% <= y% by A1,Th1,Th12;
hence x [= y by LATTICE3:7;
end;
assume x [= y;
then x% <= y% by LATTICE3:7;
hence thesis by A1,Th1,Th12;
end;
theorem Th14:
for a, b being Element of B_6, x, y being Element of Benzene st
a = x & b = y holds a "\/" b = x "\/" y & a "/\" b = x "/\" y
proof
let a, b be Element of B_6, x, y be Element of Benzene;
reconsider xy = x "\/" y as Element of B_6 by Th9,YELLOW_1:1;
assume that
A1: a = x and
A2: b = y;
x [= x "\/" y by LATTICES:5;
then
A3: a <= xy by A1,Th13;
A4: for d being Element of B_6 st d >= a & d >= b holds xy <= d
proof
let d be Element of B_6;
reconsider e = d as Element of Benzene by Th9,YELLOW_1:1;
assume d >= a & d >= b;
then x [= e & y [= e by A1,A2,Th13;
then x "\/" y [= e by FILTER_0:6;
hence thesis by Th13;
end;
y [= x "\/" y by LATTICES:5;
then
A5: b <= xy by A2,Th13;
reconsider xy = x "/\" y as Element of B_6 by Th9,YELLOW_1:1;
x "/\" y [= y by LATTICES:6;
then
A6: xy <= b by A2,Th13;
A7: for d being Element of B_6 st d <= a & d <= b holds xy >= d
proof
let d be Element of B_6;
reconsider e = d as Element of Benzene by Th9,YELLOW_1:1;
assume d <= a & d <= b;
then e [= x & e [= y by A1,A2,Th13;
then e [= x "/\" y by FILTER_0:7;
hence thesis by Th13;
end;
x "/\" y [= x by LATTICES:6;
then xy <= a by A1,Th13;
hence thesis by A3,A5,A4,A6,A7,YELLOW_0:22,23;
end;
theorem Th15:
for a, b being Element of B_6 st a = 3 \ 1 & b = 2 holds a "\/"
b = 3 & a "/\" b = 0
proof
3 in { 0, 1, 3 \ 1, 2, 3 \ 2, 3 } & 0 in { 0, 1, 3 \ 1, 2, 3 \ 2, 3 } by
ENUMSET1:def 4;
then reconsider t = 3, z = 0 as Element of B_6 by YELLOW_1:1;
let a,b be Element of B_6;
assume that
A1: a = 3\1 and
A2: b = 2;
Segm 2 c= Segm 3 by NAT_1:39;
then
A3: b <= t by YELLOW_1:3,A2;
A4: the carrier of B_6 = { 0, 1, 3 \ 1, 2, 3 \ 2, 3 } by YELLOW_1:1;
A5: for d being Element of B_6 st d >= a & d >= b holds t <= d
proof
let z9 be Element of B_6;
assume that
A6: z9 >= a and
A7: z9 >= b;
A8: Segm 2 c= z9 by A2,A7,YELLOW_1:3;
A9: now
A10: 0 in 2 by CARD_1:50,TARSKI:def 2;
assume z9 = 3\1;
hence contradiction by A8,A10,TARSKI:def 2,YELLOW11:3;
end;
A11: 3\1 c= z9 by A1,A6,YELLOW_1:3;
A12: now
assume z9 = 2;
then
A13: not 2 in z9;
2 in 3\1 by TARSKI:def 2,YELLOW11:3;
hence contradiction by A11,A13;
end;
A14: now
A15: 1 in 2 by CARD_1:50,TARSKI:def 2;
assume z9 = 3\2;
hence contradiction by A8,A15,TARSKI:def 1,YELLOW11:4;
end;
1 in 2 & 0 in 2 by TARSKI:def 2,CARD_1:50;
then 1 in z9 & 0 in z9 by A8;
then z9 <> 1 & z9 <> 0;
hence thesis by A4,A9,A12,A14,ENUMSET1:def 4;
end;
A16: for d being Element of B_6 st a >= d & b >= d holds d <= z
proof
let z9 be Element of B_6;
assume that
A17: a >= z9 and
A18: b >= z9;
A19: z9 c= 3\1 by A1,A17,YELLOW_1:3;
A20: now
assume z9 = 1;
then 0 in z9 by CARD_1:49,TARSKI:def 1;
hence contradiction by A19,TARSKI:def 2,YELLOW11:3;
end;
A21: z9 c= 2 by A2,A18,YELLOW_1:3;
A22: now
assume z9 = 3\1;
then
A23: 2 in z9 by TARSKI:def 2,YELLOW11:3;
not 2 in 2;
hence contradiction by A21,A23;
end;
A24: now
assume z9= 3;
then
A25: 2 in z9 by CARD_1:51,ENUMSET1:def 1;
not 2 in 2;
hence contradiction by A21,A25;
end;
A26: now
assume z9 = 3\2;
then
A27: 2 in z9 by TARSKI:def 1,YELLOW11:4;
not 2 in 2;
hence contradiction by A21,A27;
end;
now
assume z9 = 2;
then 0 in z9 by CARD_1:50,TARSKI:def 2;
hence contradiction by A19,TARSKI:def 2,YELLOW11:3;
end;
hence thesis by A4,A22,A26,A20,A24,ENUMSET1:def 4;
end;
z c= b;
then
A28: z <= b by YELLOW_1:3;
z c= a;
then
A29: z <= a by YELLOW_1:3;
a <= t by A1,YELLOW_1:3;
hence thesis by A3,A5,A29,A28,A16,YELLOW_0:22,23;
end;
theorem Th16:
for a, b being Element of B_6 st a = 3 \ 2 & b = 1 holds a "\/"
b = 3 & a "/\" b = 0
proof
3 in { 0, 1, 3 \ 1, 2, 3 \ 2, 3 } & 0 in { 0, 1, 3 \ 1, 2, 3 \ 2, 3 } by
ENUMSET1:def 4;
then reconsider t = 3, z = 0 as Element of B_6 by YELLOW_1:1;
let a,b be Element of B_6;
assume that
A1: a = 3\2 and
A2: b = 1;
Segm 1 c= Segm 3 by NAT_1:39;
then
A3: b <= t by YELLOW_1:3,A2;
A4: the carrier of B_6 = { 0, 1, 3 \ 1, 2, 3 \ 2, 3 } by YELLOW_1:1;
A5: for d being Element of B_6 st d >= a & d >= b holds t <= d
proof
let z9 be Element of B_6;
assume that
A6: z9 >= a and
A7: z9 >= b;
A8: 3\2 c= z9 by A1,A6,YELLOW_1:3;
A9: now
A10: 2 in 3\2 by TARSKI:def 1,YELLOW11:4;
assume z9= 1;
hence contradiction by A8,A10,CARD_1:49,TARSKI:def 1;
end;
A11: now
assume z9 = 2;
then
A12: not 2 in z9;
2 in 3\2 by TARSKI:def 1,YELLOW11:4;
hence contradiction by A8,A12;
end;
A13: 1 c= z9 by A2,A7,YELLOW_1:3;
A14: now
A15: 0 in 1 by CARD_1:49,TARSKI:def 1;
assume z9 = 3\2;
hence contradiction by A13,A15,TARSKI:def 1,YELLOW11:4;
end;
A16: now
A17: 0 in 1 by CARD_1:49,TARSKI:def 1;
assume z9 = 3\1;
hence contradiction by A13,A17,TARSKI:def 2,YELLOW11:3;
end;
z9 <> 0 by A13;
hence thesis by A4,A14,A11,A16,A9,ENUMSET1:def 4;
end;
A18: for d being Element of B_6 st a >= d & b >= d holds d <= z
proof
let z9 be Element of B_6;
assume that
A19: a >= z9 and
A20: b >= z9;
A21: z9 c= 3\2 by A1,A19,YELLOW_1:3;
A22: now
assume z9= 1;
then 0 in z9 by CARD_1:49,TARSKI:def 1;
hence contradiction by A21,TARSKI:def 1,YELLOW11:4;
end;
A23: z9 c= 1 by A2,A20,YELLOW_1:3;
A24: now
assume z9= 3\2;
then 2 in z9 by TARSKI:def 1,YELLOW11:4;
hence contradiction by A23,CARD_1:49,TARSKI:def 1;
end;
A25: now
assume z9= 3\1;
then
A26: 2 in z9 by TARSKI:def 2,YELLOW11:3;
not 2 in 1 by CARD_1:50,TARSKI:def 2;
hence contradiction by A23,A26;
end;
A27: now
assume z9= 3;
then 2 in z9 by CARD_1:51,ENUMSET1:def 1;
hence contradiction by A23,CARD_1:49,TARSKI:def 1;
end;
now
assume z9= 2;
then 0 in z9 by CARD_1:50,TARSKI:def 2;
hence contradiction by A21,TARSKI:def 1,YELLOW11:4;
end;
hence thesis by A4,A25,A24,A22,A27,ENUMSET1:def 4;
end;
z c= b;
then
A28: z <= b by YELLOW_1:3;
z c= a;
then
A29: z <= a by YELLOW_1:3;
a <= t by A1,YELLOW_1:3;
hence thesis by A3,A5,A29,A28,A18,YELLOW_0:22,23;
end;
theorem Th17:
for a, b being Element of B_6 st a = 3 \ 1 & b = 1 holds a "\/"
b = 3 & a "/\" b = 0
proof
A1: the carrier of B_6 = { 0, 1, 3 \ 1, 2, 3 \ 2, 3 } by YELLOW_1:1;
then reconsider z = 3 as Element of B_6 by ENUMSET1:def 4;
A2: Segm 1 c= Segm 3 by NAT_1:39;
let x,y be Element of B_6;
assume that
A3: x = 3\1 and
A4: y = 1;
A5: 1 \/ (3\1) = 1 \/ 3 by XBOOLE_1:39
.= 3 by A2,XBOOLE_1:12;
now
thus x <= z & y <= z by A3,YELLOW_1:3,A2,A4;
let w be Element of B_6;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence z <= w by A3,A4,A5,YELLOW_1:3;
end;
hence x "\/" y = 3 by YELLOW_0:22;
reconsider z = 0 as Element of B_6 by A1,ENUMSET1:def 4;
x misses y by A3,A4,XBOOLE_1:79;
then
A6: x /\ y = 0 by XBOOLE_0:def 7;
now
z c= x & z c= y;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of B_6;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence w <= z by A6;
end;
hence thesis by YELLOW_0:23;
end;
theorem Th18:
for a, b being Element of B_6 st a = 3 \ 2 & b = 2 holds a "\/"
b = 3 & a "/\" b = 0
proof
A1: the carrier of B_6 = { 0, 1, 3 \ 1, 2, 3 \ 2, 3 } by YELLOW_1:1;
then reconsider z = 3 as Element of B_6 by ENUMSET1:def 4;
A2: Segm 2 c= Segm 3 by NAT_1:39;
let x,y be Element of B_6;
assume that
A3: x = 3\2 and
A4: y = 2;
A5: 2 \/ (3\2) = 2 \/ 3 by XBOOLE_1:39
.= 3 by A2,XBOOLE_1:12;
now
thus x <= z & y <= z by A3,YELLOW_1:3,A2,A4;
let w be Element of B_6;
assume x <= w & y <= w;
then x c= w & y c= w by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence z <= w by A3,A4,A5,YELLOW_1:3;
end;
hence x "\/" y = 3 by YELLOW_0:22;
reconsider z = 0 as Element of B_6 by A1,ENUMSET1:def 4;
x misses y by A3,A4,XBOOLE_1:79;
then
A6: x /\ y = 0 by XBOOLE_0:def 7;
now
z c= x & z c= y;
hence z <= x & z <= y by YELLOW_1:3;
let w be Element of B_6;
assume w <= x & w <= y;
then w c= x & w c= y by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence w <= z by A6;
end;
hence thesis by YELLOW_0:23;
end;
theorem Th19:
for a, b being Element of Benzene st a = 3 \ 1 & b = 2 holds a
"\/" b = 3 & a "/\" b = 0
proof
let a,b be Element of Benzene;
assume
A1: a = 3\1 & b = 2;
then
a in { 0, 1, 3 \ 1, 2, 3 \ 2, 3 } & b in { 0, 1, 3 \ 1, 2, 3 \ 2, 3 } by
ENUMSET1:def 4;
then reconsider aa = a, bb = b as Element of B_6 by YELLOW_1:1;
aa "\/" bb = 3 & aa "/\" bb = 0 by A1,Th15;
hence thesis by Th14;
end;
theorem
for a, b being Element of Benzene st a = 3 \ 2 & b = 1 holds a "\/" b = 3
proof
let a,b be Element of Benzene;
assume
A1: a = 3 \ 2 & b = 1;
then
a in { 0, 1, 3 \ 1, 2, 3 \ 2, 3 } & b in { 0, 1, 3 \ 1, 2, 3 \ 2, 3 } by
ENUMSET1:def 4;
then reconsider aa = a, bb = b as Element of B_6 by YELLOW_1:1;
aa "\/" bb = 3 by A1,Th16;
hence thesis by Th14;
end;
theorem Th21:
for a, b being Element of Benzene st a = 3 \ 1 & b = 1 holds a "\/" b = 3
proof
let a,b be Element of Benzene;
assume
A1: a = 3\1 & b = 1;
then
a in { 0, 1, 3 \ 1, 2, 3 \ 2, 3 } & b in { 0, 1, 3 \ 1, 2, 3 \ 2, 3 } by
ENUMSET1:def 4;
then reconsider aa = a, bb = b as Element of B_6 by YELLOW_1:1;
aa "\/" bb = 3 by A1,Th17;
hence thesis by Th14;
end;
theorem Th22:
for a, b being Element of Benzene st a = 3 \ 2 & b = 2 holds a "\/" b = 3
proof
let a,b be Element of Benzene;
assume
A1: a = 3\2 & b = 2;
then
a in { 0, 1, 3 \ 1, 2, 3 \ 2, 3 } & b in { 0, 1, 3 \ 1, 2, 3 \ 2, 3 } by
ENUMSET1:def 4;
then reconsider aa = a, bb = b as Element of B_6 by YELLOW_1:1;
aa "\/" bb = 3 by A1,Th18;
hence thesis by Th14;
end;
theorem Th23:
for a being Element of Benzene holds (a = 0 implies a` = 3) & (a
= 3 implies a` = 0) & (a = 1 implies a` = 3\1) & (a = 3\1 implies a` = 1) & (a
= 2 implies a` = 3\2) & (a = 3\2 implies a` = 2)
proof
set B = Benzene;
let a be Element of Benzene;
reconsider c = a as Subset of 3 by Th10;
A1: a` c= c` by Def4;
A2: a` = c` by Def4;
hence a = 0 implies a` = 3;
A3: a` = {} or a` = {0} or a` = {1} or a` = {2} or a` = {0,1} or a` = {1,2}
or a` = {0,2} or a` = {0,1,2} by A2,YELLOW11:1,ZFMISC_1:118;
thus a = 3 implies a` = 0
proof
assume
A4: a = 3;
then 1 in c by ENUMSET1:def 1,YELLOW11:1;
then
A5: not 1 in a` by A1,XBOOLE_0:def 5;
2 in c by A4,ENUMSET1:def 1,YELLOW11:1;
then
A6: not 2 in a` by A1,XBOOLE_0:def 5;
not 0 in c` by A4,XBOOLE_0:def 5;
then not 0 in a` by Def4;
hence thesis by A3,A5,A6,ENUMSET1:def 1,TARSKI:def 1,def 2;
end;
thus a = 1 implies a` = 3 \ 1 by A2;
A7: 0 in 3 by ENUMSET1:def 1,YELLOW11:1;
thus a = 3\1 implies a` = 1
proof
assume
A8: a = 3\1;
then 1 in c by TARSKI:def 2,YELLOW11:3;
then
A9: not 1 in a` by A1,XBOOLE_0:def 5;
2 in c by A8,TARSKI:def 2,YELLOW11:3;
then
A10: not 2 in a` by A1,XBOOLE_0:def 5;
not 0 in c by A8,TARSKI:def 2,YELLOW11:3;
hence thesis by A7,A2,A3,A9,A10,CARD_1:49,ENUMSET1:def 1,TARSKI:def 1,def 2
,XBOOLE_0:def 5;
end;
thus a = 2 implies a` = 3\2 by A2;
assume
A11: a = 3\2;
then 2 in c by TARSKI:def 1,YELLOW11:4;
then
A12: not 2 in a` by A1,XBOOLE_0:def 5;
1 in 3 & not 1 in c by A11,ENUMSET1:def 1,TARSKI:def 1,YELLOW11:1,4;
then
A13: 1 in a` by A2,XBOOLE_0:def 5;
not 0 in c by A11,TARSKI:def 1,YELLOW11:4;
then 0 in a` by A7,A2,XBOOLE_0:def 5;
hence thesis by A3,A12,A13,CARD_1:50,ENUMSET1:def 1,TARSKI:def 1,def 2;
end;
theorem Th24:
for a, b being Element of Benzene holds a [= b iff a c= b
proof
let a, b be Element of Benzene;
reconsider x = a, y = b as Element of B_6 by Th9,YELLOW_1:1;
hereby
assume a [= b;
then x <= y by Th13;
hence a c= b by YELLOW_1:3;
end;
assume a c= b;
then x <= y by YELLOW_1:3;
hence thesis by Th13;
end;
theorem Th25:
for a, x being Element of Benzene st a = 0 holds a "/\" x = a
proof
let a, x be Element of Benzene;
assume a = 0;
then a c= x;
then a [= x by Th24;
hence thesis by LATTICES:4;
end;
theorem Th26:
for a, x being Element of Benzene st a = 0 holds a "\/" x = x
proof
let a, x be Element of Benzene;
assume a = 0;
then a c= x;
then a [= x by Th24;
hence thesis;
end;
theorem Th27:
for a, x being Element of Benzene st a = 3 holds a "\/" x = a
proof
let a, x be Element of Benzene;
assume a = 3;
then x c= a by Th11,YELLOW11:1;
then x [= a by Th24;
hence thesis;
end;
registration
cluster Benzene -> lower-bounded;
coherence
proof
reconsider B = 0 as Element of Benzene by Th9,ENUMSET1:def 4;
take B;
for a being Element of Benzene holds B "/\" a = B & a "/\" B = B by Th25;
hence thesis;
end;
cluster Benzene -> upper-bounded;
coherence
proof
reconsider B = 3 as Element of Benzene by Th9,ENUMSET1:def 4;
take B;
for a being Element of Benzene holds B "\/" a = B & a "\/" B = B by Th27;
hence thesis;
end;
end;
theorem
Top Benzene = 3
proof
reconsider x = 3 as Element of Benzene by Th9,ENUMSET1:def 4;
for a being Element of Benzene holds x "\/" a = x & a "\/" x = x by Th27;
hence thesis by LATTICES:def 17;
end;
theorem Th29:
Bottom Benzene = 0
proof
reconsider x = 0 as Element of Benzene by Th9,ENUMSET1:def 4;
for a being Element of Benzene holds x "/\" a = x & a "/\" x = x by Th25;
hence thesis by LATTICES:def 16;
end;
registration
cluster Benzene -> involutive with_Top de_Morgan;
coherence
proof
set B = Benzene;
for a being Element of B holds a`` = a
proof
let a be Element of B;
per cases by Th9,ENUMSET1:def 4;
suppose
A1: a = 0;
then a` = 3 by Th23;
hence thesis by A1,Th23;
end;
suppose
A2: a = 1;
then a` = 3\1 by Th23;
hence thesis by A2,Th23;
end;
suppose
A3: a = 3\1;
then a` = 1 by Th23;
hence thesis by A3,Th23;
end;
suppose
A4: a = 2;
then a` = 3\2 by Th23;
hence thesis by A4,Th23;
end;
suppose
A5: a = 3\2;
then a` = 2 by Th23;
hence thesis by A5,Th23;
end;
suppose
A6: a = 3;
then a` = 0 by Th23;
hence thesis by A6,Th23;
end;
end;
hence
A7: B is involutive;
A8: for a being Element of B holds a "\/" a` = 3
proof
let a be Element of B;
per cases by Th9,ENUMSET1:def 4;
suppose
A9: a = 0;
then a` = 3 by Th23;
hence thesis by A9,Th26;
end;
suppose
A10: a = 1;
then a` = 3\1 by Th23;
hence thesis by A10,Th21;
end;
suppose
A11: a = 3\1;
then a` = 1 by Th23;
hence thesis by A11,Th21;
end;
suppose
A12: a = 2;
then a` = 3\2 by Th23;
hence thesis by A12,Th22;
end;
suppose
A13: a = 3\2;
then a` = 2 by Th23;
hence thesis by A13,Th22;
end;
suppose
a = 3;
hence thesis by Th27;
end;
end;
thus B is with_Top
proof
let a,b be Element of B;
a "\/" a` = 3 by A8;
hence thesis by A8;
end;
for a,b being Element of B holds a [= b implies b` [= a`
proof
let a,b be Element of B;
reconsider x = a, y = b as Subset of {0,1,2} by Th11;
reconsider x, y as Subset of 3 by CARD_1:51;
assume a [= b;
then x c= y by Th24;
then
A14: y` c= x` by SUBSET_1:12;
a` = x` & b` = y` by Def4;
hence thesis by A14,Th24;
end;
hence B is de_Morgan by A7,Th4;
end;
cluster Benzene -> non orthomodular;
coherence
proof
not for x, y being Element of Benzene st x [= y holds y = x "\/" (x`
"/\" y)
proof
set y = 2;
set x = 1;
reconsider x, y as Element of Benzene by Th9,ENUMSET1:def 4;
for z being object holds z in 1 implies z in 2
proof
let z be object;
assume z in 1;
then z = 0 by CARD_1:49,TARSKI:def 1;
hence thesis by CARD_1:50,TARSKI:def 2;
end;
then 1 c= 2;
then
A15: x [= y by Th24;
x` = 3\1 by Th23;
then x` "/\" y = 0 by Th19;
then x "\/" (x` "/\" y) = x by Th29;
hence thesis by A15;
end;
hence thesis;
end;
end;
begin :: Orthogonality
definition
let L be Ortholattice, a,b be Element of L;
pred a, b are_orthogonal means
a [= b`;
end;
notation
let L be Ortholattice, a,b be Element of L;
synonym a _|_ b for a, b are_orthogonal;
end;
theorem
a _|_ a iff a = Bottom L
proof
thus a _|_ a implies a = Bottom L
proof
assume a_|_a;
then a [= a`;
then a "/\" a` = a by LATTICES:4;
hence thesis by Th2;
end;
assume a = Bottom L;
then a "/\" a` = a;
then a [= a` by LATTICES:4;
hence thesis;
end;
definition
let L be Ortholattice;
let a, b be Element of L;
redefine pred a,b are_orthogonal; :: redefines are_orthogonal (ROBBINS4, definition)
symmetry
proof
let a, b be Element of L;
assume a _|_ b;
then a [= b`;
then b`` [= a` by Th4;
then b [= a` by ROBBINS3:def 6;
hence thesis;
end;
end;
theorem
a _|_ b & a _|_ c implies a _|_ (b "/\" c) & a _|_ (b "\/" c)
proof
assume a _|_ b;
then
A1: a [= b`;
then
A2: a "/\" c` [= b` "/\" c` by LATTICES:9;
assume
A3: a _|_ c;
b`[= b` "\/" c` by LATTICES:5;
then a [= b` "\/" c` by A1,LATTICES:7;
then a [= (b` "\/" c`)`` by ROBBINS3:def 6;
then a [= (b "/\" c)` by ROBBINS1:def 23;
hence a _|_ (b "/\" c);
a [= c` by A3;
then a [= b` "/\" c` by A2,LATTICES:4;
then a [= (b`` "\/" c``)` by ROBBINS1:def 23;
then a [= (b "\/" c``)` by ROBBINS3:def 6;
then a [= (b "\/" c)` by ROBBINS3:def 6;
hence thesis;
end;
begin :: Orthomodularity Conditions
theorem
L is orthomodular iff for a,b being Element of L st b` [= a & a "/\" b
= Bottom L holds a = b`
proof
thus L is orthomodular implies for a,b being Element of L st b` [= a & a
"/\" b = Bottom L holds a = b`
proof
assume
A1: L is orthomodular;
let x,y be Element of L;
assume
A2: y` [= x;
assume
A3: x "/\" y = Bottom L;
thus x = y` "\/" (y`` "/\" x) by A1,A2
.= y` "\/" (y "/\" x) by ROBBINS3:def 6
.= y` by A3;
end;
assume
A4: for a,b being Element of L st b` [= a & a "/\" b = Bottom L holds a = b`;
let x,y be Element of L;
assume x [= y;
then x "\/" (x` "/\" y) [= y "\/" (x` "/\" y) by FILTER_0:1;
then x "\/" (x` "/\" y) [= y by LATTICES:def 8;
then
A5: (x"\/"(x`"/\"y))``[=y by ROBBINS3:def 6;
(x"\/"(x`"/\"y))`"/\"y=y"/\"(x``"\/"(x`"/\"y))` by ROBBINS3:def 6
.= y"/\"(x``"\/"(x`"/\"y)``)` by ROBBINS3:def 6
.= y"/\"(x`"/\"(x`"/\"y)`) by ROBBINS1:def 23
.= y"/\"(x`"/\"(x``"\/"y`)``) by ROBBINS1:def 23
.= y"/\"(x`"/\"(x``"\/"y`)) by ROBBINS3:def 6
.= y"/\"(x`"/\"(x"\/"y`)) by ROBBINS3:def 6
.= (y"/\"x`)"/\"(x"\/"y`) by LATTICES:def 7
.= (y`"\/"x``)`"/\"(x"\/"y`) by ROBBINS1:def 23
.= (x"\/"y`)` "/\" (x "\/" y`) by ROBBINS3:def 6
.= Bottom L by Th2;
then (x "\/" (x` "/\" y))`` = y by A4,A5;
hence thesis by ROBBINS3:def 6;
end;
theorem
L is orthomodular iff for a,b being Element of L st a _|_ b & a "\/" b
= Top L holds a = b`
proof
thus L is orthomodular implies for a,b being Element of L st a _|_ b & a
"\/" b = Top L holds a = b`
proof
assume
A1: L is orthomodular;
let x,y be Element of L;
assume x _|_ y;
then
A2: x [= y`;
assume
A3: x "\/" y = Top L;
thus y` = x "\/" (x` "/\" y`) by A1,A2
.= x "\/" (x`` "\/" y``)` by ROBBINS1:def 23
.= x "\/" (x "\/" y``)` by ROBBINS3:def 6
.= x "\/" (x "\/" y)` by ROBBINS3:def 6
.= x "\/" (x``"\/"x`)` by A3,Th2
.= x "\/" (x`"/\"x) by ROBBINS1:def 23
.= x by LATTICES:def 8;
end;
assume
A4: for a,b being Element of L st a _|_ b & a "\/" b = Top L holds a = b `;
let x,y be Element of L;
assume x [= y;
then x "\/" (x` "/\" y) [= y "\/" (x` "/\" y) by FILTER_0:1;
then x "\/" (x` "/\" y) [= y by LATTICES:def 8;
then x "\/" (x` "/\" y) [= y`` by ROBBINS3:def 6;
then
A5: x "\/" (x` "/\" y) _|_ y`;
y` "\/" (x "\/" (x` "/\" y)) = (y` "\/" x) "\/" (x` "/\" y) by LATTICES:def 5
.= (y` "\/" x``) "\/" (x` "/\" y) by ROBBINS3:def 6
.= (y` "\/" x``)`` "\/" (x` "/\" y) by ROBBINS3:def 6
.= (y "/\" x`)` "\/" (x` "/\" y) by ROBBINS1:def 23
.= Top L by Th2;
then x "\/" (x` "/\" y) = y`` by A4,A5;
hence thesis by ROBBINS3:def 6;
end;
theorem Th34:
L is orthomodular iff for a,b being Element of L st b [= a holds
a "/\" (a` "\/" b) = b
proof
thus L is orthomodular implies for a,b being Element of L st b [= a holds a
"/\" (a` "\/" b) = b
proof
assume
A1: L is orthomodular;
let a,b be Element of L;
assume b [= a;
then a` [= b` by Th4;
then b` = a` "\/" (a`` "/\" b`) by A1
.= a` "\/" (a "/\" b`) by ROBBINS3:def 6
.= a` "\/" (a` "\/" b``)` by ROBBINS1:def 23
.= a` "\/" (a` "\/" b)` by ROBBINS3:def 6
.= (a` "\/" (a` "\/" b)`)`` by ROBBINS3:def 6
.= (a "/\" (a` "\/" b))` by ROBBINS1:def 23;
then b``= (a "/\" (a` "\/" b)) by ROBBINS3:def 6;
hence thesis by ROBBINS3:def 6;
end;
assume
A2: for a,b being Element of L st b [= a holds a "/\" (a` "\/" b) = b;
let a,b be Element of L;
assume a [= b;
then b` [= a` by Th4;
then b` = a`"/\"(a``"\/"b`) by A2
.= a`"/\"(a``"\/"b`)`` by ROBBINS3:def 6
.= a` "/\" (a` "/\" b)` by ROBBINS1:def 23
.= (a`` "\/"(a` "/\" b)``)` by ROBBINS1:def 23
.= (a "\/" (a` "/\" b)``)` by ROBBINS3:def 6
.= (a "\/" (a` "/\" b))` by ROBBINS3:def 6;
then b`` = (a "\/" (a` "/\" b)) by ROBBINS3:def 6;
hence b = a "\/" (a` "/\" b) by ROBBINS3:def 6;
end;
theorem
L is orthomodular iff for a,b holds a "/\" (a` "\/" (a "/\" b)) = a "/\" b
proof
thus L is orthomodular implies for a,b holds a "/\" (a` "\/" (a "/\" b)) = a
"/\" b
by LATTICES:6,Th34;
assume
A1: for a,b holds a "/\" (a` "\/" (a "/\" b)) = a "/\" b;
for a,b holds b [= a implies a "/\" (a` "\/" b) = b
proof
let a,b;
assume
A2: b [= a;
hence b = a "/\" b by LATTICES:4
.= a "/\" (a` "\/" (a "/\" b)) by A1
.= a "/\" (a` "\/" b) by A2,LATTICES:4;
end;
hence thesis by Th34;
end;
theorem Th36:
L is orthomodular iff for a,b being Element of L holds a "\/" b
= ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" a`)
proof
thus L is orthomodular implies for a,b being Element of L holds a "\/" b = (
(a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" a`)
proof
assume
A1: L is orthomodular;
let a,b be Element of L;
a "\/" b = a "\/" ((a "\/" b) "/\" a`) by A1,Th6;
hence thesis by LATTICES:def 9;
end;
assume
A2: for a,b being Element of L holds a "\/" b = ((a "\/" b) "/\" a) "\/"
((a "\/" b) "/\" a`);
let x,y be Element of L;
assume
A3: x [= y;
hence y = x "\/" y
.= ((x "\/" y) "/\" x) "\/" ((x "\/" y) "/\" x`) by A2
.= (y "/\" x) "\/" ((x "\/" y) "/\" x`) by A3
.= (y "/\" x) "\/" (y "/\" x`) by A3
.= x "\/" (x` "/\" y) by A3,LATTICES:4;
end;
theorem
L is orthomodular iff for a,b st a [= b holds (a "\/" b) "/\" (b "\/"
a`) = (a "/\" b) "\/" (b "/\" a`)
proof
thus L is orthomodular implies for a,b st a [= b holds (a "\/" b) "/\" (b
"\/" a`) = (a "/\" b) "\/" (b "/\" a`)
proof
assume
A1: L is orthomodular;
let a,b;
assume
A2: a [= b;
(a"/\"b)[=(a"\/"b) & (b"/\"a`)[=(a"\/"b) by FILTER_0:3,LATTICES:6;
then
A3: (a"/\"b)"\/" (b"/\"a`)[=(a"\/"b) by FILTER_0:6;
(a"/\"b)[=(b"\/"a`) & (b"/\"a`)[=(b"\/"a`) by FILTER_0:3,LATTICES:6;
then (a"/\"b)"\/" (b"/\"a`)[=(b"\/"a`) by FILTER_0:6;
then
A4: (a"/\"b)"\/" (b"/\"a`)[=(a"\/"b)"/\"(b"\/"a`) by A3,FILTER_0:7;
A5: (a"\/"b)"/\"(b"\/"a`)[= a"\/"b by LATTICES:6;
a "\/"b = ((a"\/"b)"/\"a)"\/"((a"\/"b)"/\"a`) by A1,Th36
.= (b"/\"a)"\/"((a"\/"b)"/\"a`) by A2
.= (b"/\"a)"\/"(b"/\"a`) by A2;
hence thesis by A4,A5,LATTICES:8;
end;
assume
A6: for a,b st a[=b holds (a "\/" b) "/\" (b "\/" a`) = (a "/\" b) "\/"
(b "/\" a`);
let a,b;
assume
A7: a [= b;
then (a "\/" b) "/\" (b "\/" a`) = (a "/\" b) "\/" (b "/\" a`) by A6
.= a "\/" (a` "/\" b) by A7,LATTICES:4;
hence a "\/" (a` "/\" b) = b "/\" (b "\/" a`) by A7
.= b by LATTICES:def 9;
end;
::$N The short(est) axiomatization of orthomodular ortholattices
theorem
for L being non empty OrthoLattStr holds L is Orthomodular_Lattice iff
(for a, b, c being Element of L holds (a "\/" b) "\/" c = (c` "/\" b`)` "\/" a)
& (for a, b,c being Element of L holds a "\/" b = ((a "\/" b) "/\" (a "\/" c))
"\/" ((a "\/" b) "/\" a`)) & for a, b being Element of L holds a = a "\/" (b
"/\" b`)
proof
let L be non empty OrthoLattStr;
thus L is Orthomodular_Lattice implies (for a, b, c being Element of L holds
(a "\/" b) "\/" c = (c` "/\" b`)` "\/" a) & (for a, b,c being Element of L
holds a "\/" b = ((a "\/" b) "/\" (a "\/" c)) "\/" ((a "\/" b) "/\" a`)) & for
a, b being Element of L holds a = a "\/" (b "/\" b`)
proof
assume
A1: L is Orthomodular_Lattice;
hence
for a, b, c being Element of L holds (a "\/" b) "\/" c = (c` "/\" b`)
` "\/" a by Th3;
thus for a, b,c being Element of L holds a "\/" b = ((a "\/" b) "/\" (a
"\/" c)) "\/" ((a "\/" b) "/\" a`)
proof
let a,b,c be Element of L;
(a"\/"b)"/\"a` [= a "\/"b & (a"\/"b)"/\"(a"\/"c) [= a "\/"b by A1,
LATTICES:6;
then
A2: ((a"\/"b)"/\"(a"\/"c))"\/"((a"\/"b)"/\"a`) [= a "\/"b by A1,FILTER_0:6;
a"/\"(a"\/"b)[=(a"\/"c)"/\"(a"\/"b) by A1,LATTICES:5,9;
then (a"\/"b)"/\"a[=(a"\/"c)"/\"(a"\/"b) by A1,LATTICES:def 6;
then (a"\/"b)"/\"a[= (a"\/"b)"/\"(a"\/"c) by A1,LATTICES:def 6;
then
((a"\/"b)"/\"a`)"\/"((a"\/"b)"/\"a)[= ((a"\/"b)"/\"a`)"\/"((a"\/"b)
"/\"(a"\/"c)) by A1,FILTER_0:1;
then
A3: ((a"\/"b)"/\"a)"\/"((a"\/"b)"/\"a`)[= ((a"\/"b)"/\"a`)"\/"((a"\/"b)
"/\"(a"\/"c))by A1,LATTICES:def 4;
a"\/"b=((a"\/"b)"/\"a)"\/"((a"\/"b)"/\"a`) by A1,Th36;
then a "\/"b [= ((a"\/"b)"/\"(a"\/"c))"\/"((a"\/"b)"/\"a`) by A1,A3,
LATTICES:def 4;
hence thesis by A1,A2,LATTICES:8;
end;
thus thesis by A1,Th3;
end;
assume
A4: for a, b, c being Element of L holds (a "\/" b) "\/" c = (c` "/\" b
`)` "\/" a;
assume
A5: for a, b,c being Element of L holds a "\/" b = ((a"\/"b)"/\"(a"\/"c
))"\/"((a"\/"b)"/\"a`);
assume
A6: for a, b being Element of L holds a = a "\/" (b "/\" b`);
A7: for a,b being Element of L holds a "\/" b = ((a "\/" b) "/\" a) "\/" ((
a "\/" b) "/\" a`)
proof
let a,b be Element of L;
set c = a "/\" a`;
a "\/" b = ((a "\/" b) "/\" (a "\/" c)) "\/" ((a "\/" b) "/\" a`) by A5;
hence thesis by A6;
end;
for a, c being Element of L holds a = a "/\" (a"\/"c)
proof
let a,c be Element of L;
set b = a "/\" a`;
thus a = a "\/" b by A6
.= ((a"\/"b)"/\"(a"\/"c))"\/"((a"\/"b)"/\"a`) by A5
.= (a"/\"(a"\/"c))"\/"((a"\/"b)"/\"a`) by A6
.= (a"/\"(a"\/"c))"\/"(a"/\"a`) by A6
.= a"/\"(a"\/"c) by A6;
end;
then L is Ortholattice by A4,A6,Th3;
hence thesis by A7,Th36;
end;
reserve L for join-Associative meet-Absorbing de_Morgan orthomodular
Lattice-like non empty OrthoLattStr;
reserve v0,v1,v2,v64,v65 for Element of L;
registration
cluster -> with_Top for
join-Associative meet-Absorbing de_Morgan orthomodular
Lattice-like non empty OrthoLattStr;
coherence
proof
let L;
deffunc c(Element of L) = $1`;
for x,y be Element of L holds x "\/" c(x) = y "\/" c(y)
proof
A1: v0 "\/" c((c(v0) "\/" c(v1))) = v0
proof
(v0 "/\" v1)=c((c(v0) "\/" c(v1))) by ROBBINS1:def 23;
hence thesis by ROBBINS3:def 3;
end;
A2: v64 "\/" c(c(v64)) = v64
proof
now
let v64,v1;
(c(v64) "\/" c((c(c(v64)) "\/" c(v1)))) = c(v64) by A1;
hence (v64 "\/" c(c(v64))) = v64 by A1;
end;
hence thesis;
end;
A3: (v0 "\/" c((c(c(v0)) "\/" c((v0 "\/" v1))))) = v0 "\/" v1
proof
(c(v0) "/\" (v0 "\/" v1))=c((c(c(v0)) "\/" c((v0 "\/" v1)))) by
ROBBINS1:def 23;
hence thesis by Def2;
end;
A4: v64 "\/" c((c(v64) "\/" v1)) = v64
proof
(c(v64) "\/" c((c(c(c(v64))) "\/" c((c(v64) "\/" v1))))) = (c(v64
) "\/" v1) by A3;
hence thesis by A1;
end;
A5: v64 "\/" v65 = (v65 "\/" (v64 "\/" c((c(v65) "\/" v1))))
proof
v65 "\/" c((c(v65) "\/" v1)) = v65 by A4;
hence thesis by ROBBINS3:def 1;
end;
A6: v64 "\/" v65 = v65 "\/" (v64 "\/" c(c(v65)))
proof
v65 "\/" c(c(v65)) = v65 by A2;
hence thesis by ROBBINS3:def 1;
end;
A7: v64 "\/" v64`` = v64```` "\/" v64
proof
v64```` "\/" v64`` = v64`` by A2;
hence thesis by A6;
end;
A8: v64 = v64```` "\/" v64
proof
v64 "\/" v64`` = v64 by A2;
hence thesis by A7;
end;
A9: v65``` "\/" v65` = v65```
proof
v65```` "\/" v65 = v65 by A8;
hence thesis by A4;
end;
A10: v65` = v65```
proof
v65``` "\/" v65` = v65` by A2;
hence thesis by A9;
end;
A11: (c(c(c(c(v65)))) "\/" c((c(c(c(c(c(c(v65)))))) "\/" c(v65))))=(c(c(
c(c(v65)))) "\/" v65)
proof
(c(c(c(c(v65)))) "\/" v65) = v65 by A8;
hence thesis by A3;
end;
A12: (c(c(v65)) "\/" c((c(c(c(c(c(c(v65)))))) "\/" c(v65)))) = (c(c(c(c(
v65)))) "\/" v65)
proof
v65``` = v65` by A10;
hence thesis by A11;
end;
A13: (c(c(v65)) "\/" c((c(c(c(c(v65)))) "\/" c(v65)))) = c(c(c(c(v65))))
"\/" v65
proof
v65``` = v65` by A10;
hence thesis by A12;
end;
A14: (c(c(v65)) "\/" c((c(c(v65)) "\/" c(v65)))) = c(c(c(c(v65)))) "\/" v65
proof
v65``` = v65` by A10;
hence thesis by A13;
end;
A15: (c(c(v65)) "\/" c((c(c(v65)) "\/" c(v65)))) = (c(c(v65)) "\/" v65)
proof
v65``` = v65` by A10;
hence thesis by A14;
end;
A16: (c(c(v65)) "\/" c((c(c(v65)) "\/" c(v65)))) = v65
proof
v65`` "\/" v65 = v65 by A2;
hence thesis by A15;
end;
A17: (c(c(v0)) "\/" c((v65 "\/" c(v0)))) = v0``
proof
v0``` = v0` by A10;
hence thesis by A4;
end;
A18: v0`` = v0
proof
(c(c(v0)) "\/" c((c(c(v0)) "\/" c(v0)))) = v0`` by A17;
hence thesis by A16;
end;
A19: (v64 "\/" c((c(c(v64)) "\/" c((v1 "\/" v64))))) = (v64 "\/" (v1
"\/" c(c(v64))))
proof
(v64 "\/" (v1 "\/" c(c(v64)))) = (v1 "\/" v64) by A6;
hence thesis by A3;
end;
A20: (v64 "\/" c((c(c(v64)) "\/" c((v1 "\/" v64))))) = v1 "\/" v64
proof
v64 "\/" (v1 "\/" v64``) = v1 "\/" v64 by A6;
hence thesis by A19;
end;
A21: (v0 "\/" c((v0 "\/" c((v1 "\/" v0))))) = v1 "\/" v0
proof
v0`` = v0 by A18;
hence thesis by A20;
end;
A22: (v64 "\/" (v1 "\/" c(v64))) = (c(v64) "\/" v64)
proof
(c(v64) "\/" c((c(v64) "\/" c((v1 "\/" c(v64))))))=(v1 "\/" c(v64
)) by A21;
hence thesis by A5;
end;
A23: (c(v0) "\/" c((v0 "\/" v65))) = v0`
proof
v0`` = v0 by A18;
hence thesis by A4;
end;
A24: ((v0 "\/" v1) "\/" c(v0))=(c((v0 "\/" v1)) "\/" (v0 "\/" v1))
proof
(v0` "\/" c((v0 "\/" v1)))=c(v0) by A23;
hence thesis by A22;
end;
A25: (v0 "\/" (v1 "\/" c(v0))) = (c((v0 "\/" v1)) "\/" (v0 "\/" v1))
proof
((v0 "\/" v1) "\/" c(v0)) = (v0 "\/" (v1 "\/" c(v0))) by ROBBINS3:def 1
;
hence thesis by A24;
end;
A26: (v0 "\/" (v1 "\/" (v65 "\/" c((v0 "\/" v1))))) = (c((v0 "\/" v1))
"\/" (v0 "\/" v1))
proof
((v0 "\/" v1) "\/" (v65 "\/" c((v0 "\/" v1)))) = (v0 "\/" (v1
"\/" (v65 "\/" c((v0 "\/" v1))))) by ROBBINS3:def 1;
hence thesis by A22;
end;
A27: (v0 "\/" (v1 "\/" (v65 "\/" c((v0 "\/" v1))))) =(v0 "\/" (v1 "\/" c
(v0)))
proof
(c((v0 "\/" v1)) "\/" (v0 "\/" v1))=(v0 "\/" (v1 "\/" c(v0))) by A25;
hence thesis by A26;
end;
A28: (c((v1 "\/" v0)) "\/" (v0 "\/" v1)) = (v0 "\/" (v1 "\/" (v65 "\/" c
((v0 "\/" v1)))))
proof
((v0 "\/" v1) "\/" (v65 "\/" c((v0 "\/" v1)))) = (v0 "\/" (v1
"\/" (v65 "\/" c((v0 "\/" v1))))) by ROBBINS3:def 1;
hence thesis by A22;
end;
A29: (c((v1 "\/" v0)) "\/" (v0 "\/" v1)) = (v0 "\/" (v1 "\/" c(v0)))
proof
now
let v65,v1,v0;
(v0 "\/" (v1 "\/" (v65 "\/" c((v0 "\/" v1))))) = (v0 "\/" (v1
"\/" c(v0))) by A27;
hence (c((v1 "\/" v0)) "\/" (v0 "\/" v1))=(v0 "\/" (v1 "\/" c(v0)))
by A28;
end;
hence thesis;
end;
A30: (v2 "\/" (v1 "\/" c(v2))) = ((v1 "\/" v2) "\/" (v65 "\/" c((v1 "\/"
v2))))
proof
(c((v1 "\/" v2)) "\/" (v2 "\/" v1))=(v2 "\/" (v1 "\/" c(v2))) by A29;
hence thesis by A22;
end;
A31: (v2 "\/" (v1 "\/" v2`)) = v1 "\/" (v2 "\/" (v65 "\/" c((v1 "\/" v2) )))
proof
((v1 "\/" v2) "\/" (v65 "\/" c((v1 "\/" v2)))) = (v1 "\/" (v2
"\/" (v65 "\/" c((v1 "\/" v2))))) by ROBBINS3:def 1;
hence thesis by A30;
end;
A32: v2 "\/" (v1 "\/" v2`) = v1 "\/" (v2 "\/" v1`)
proof
now
let v65,v2,v1;
(v1 "\/" (v2 "\/" (v65 "\/" c((v1 "\/" v2))))) = (v1 "\/" (v2
"\/" c(v1))) by A27;
hence v2 "\/" (v1 "\/" c(v2)) = v1 "\/" (v2 "\/" c(v1)) by A31;
end;
hence thesis;
end;
A33: v0 "\/" v0` = v1 "\/" (v0 "\/" v1`)
proof
v0 "\/" (v1 "\/" v0`) = v0 "\/" v0` by A22;
hence thesis by A32;
end;
let v1,v0;
v1 "\/" (v0 "\/" v1`) = v1 "\/" v1` by A22;
hence thesis by A33;
end;
hence thesis;
end;
end;
theorem
for L being non empty OrthoLattStr holds L is Orthomodular_Lattice iff
L is join-Associative meet-Absorbing de_Morgan Orthomodular
proof
let L be non empty OrthoLattStr;
thus L is Orthomodular_Lattice implies L is join-Associative meet-Absorbing
de_Morgan Orthomodular;
assume
A1: L is join-Associative;
assume
A2: L is meet-Absorbing;
assume
A3: L is de_Morgan;
A4: for x,y being Element of L holds x = x "\/" (x` "\/" y`)`
proof
let x,y be Element of L;
thus x = x "\/" (x "/\" y) by A2
.= x "\/" (x` "\/" y`)` by A3;
end;
A5: for x being Element of L holds x = x "\/" x``
proof
let x be Element of L;
thus x = x "\/" (x` "\/" (x`` "\/" x``)`)` by A4
.= x "\/" (x` "\/" (x` "/\" x`))` by A3
.= x "\/" x`` by A2;
end;
assume
A6: L is Orthomodular;
A7: for x,y being Element of L holds x "\/" y = x "\/"(x``"\/" (x "\/" y)`)`
proof
let x,y be Element of L;
thus x "\/" y = x "\/" (x` "/\" (x "\/" y)) by A6
.= x "\/" (x`` "\/" (x "\/" y)`)` by A3;
end;
A8: for x,y being Element of L holds x "\/" (x` "\/" y)` = x
proof
let x,y be Element of L;
thus x "\/" (x` "\/" y)` = x "\/" (x` "\/" (x``` "\/" (x` "\/" y)`)`)` by
A7
.= x by A4;
end;
A9: for x,y being Element of L holds x "\/" (y "\/" x``) = y "\/" x
proof
let x,y be Element of L;
y "\/" x = y "\/" (x "\/" x``) by A5;
hence thesis by A1;
end;
A10: for x,y being Element of L holds x "\/" (y "\/" x`)` = x
proof
let x,y be Element of L;
thus x "\/" (y "\/" x`)` = x "\/" (x` "\/" (y "\/" x```))` by A9
.= x by A8;
end;
A11: for x being Element of L holds x` "\/" x` = x`
proof
let x be Element of L;
thus x` = x` "\/" (x "\/" x``)` by A10
.= x` "\/" x` by A5;
end;
A12: for x being Element of L holds x`` "\/" x = x
proof
let x be Element of L;
x`` "\/" x = x "\/" (x`` "\/" x``) by A9
.= x "\/" x`` by A11;
hence thesis by A5;
end;
A13: for x being Element of L holds x```` "\/" x = x
proof
let x be Element of L;
x```` "\/" x = x "\/" (x```` "\/" x``) by A9
.= x "\/" x`` by A12;
hence thesis by A5;
end;
A14: for x being Element of L holds x``` = x`
proof
let x be Element of L;
x``` = x``` "\/" (x```` "\/" x)` by A8
.= x``` "\/" x` by A13;
hence thesis by A12;
end;
A15: for x,y being Element of L holds x`` "\/" (y "\/" x`)` = x``
proof
let x,y be Element of L;
x`` = x`` "\/" (y "\/" x```)` by A10;
hence thesis by A14;
end;
A16: for x being Element of L holds x`` "\/" (x`` "\/" x`)` = x
proof
let x be Element of L;
x = x```` "\/" x by A13
.= x```` "\/" (x`````` "\/" (x```` "\/" x)`)` by A7
.= x```` "\/" (x`````` "\/" x`)` by A13
.= x`` "\/" (x`````` "\/" x`)` by A14
.= x`` "\/" (x```` "\/" x`)` by A14;
hence thesis by A14;
end;
A17: for x being Element of L holds x`` = x
proof
let x be Element of L;
thus x = x`` "\/" (x`` "\/" x`)` by A16
.= x`` by A15;
end;
A18: L is join-absorbing
proof
let a,b be Element of L;
a "/\" (a "\/" b) = (a` "\/" (a "\/" b)`)` by A3
.= (a` "\/" (a`` "\/" b)`)` by A17
.= a`` by A8
.= a by A17;
hence thesis;
end;
L is meet-Associative
proof
let a,b,c be Element of L;
thus a "/\" (b "/\" c) = a "/\" (b` "\/" c`)` by A3
.= (a` "\/" (b` "\/" c`)``)` by A3
.= (a` "\/" (b` "\/" c`))` by A17
.= (b` "\/" (a` "\/" c`))` by A1
.= (b` "\/" (a` "\/" c`)``)` by A17
.= (b` "\/" (a "/\" c)`)` by A3
.= b "/\" (a "/\" c) by A3;
end;
then reconsider L9 = L as Lattice-like non empty OrthoLattStr by A1,A2,A18;
reconsider L9 as join-Associative meet-Absorbing de_Morgan Orthomodular
Lattice-like non empty OrthoLattStr by A3,A6;
L9 is with_Top;
hence thesis by A17,ROBBINS3:def 6;
end;