:: Orthomodular Lattices
:: by El\.zbieta M\c{a}dra and Adam Grabowski
::
:: Received June 27, 2008
:: Copyright (c) 2008 Association of Mizar Users
environ
vocabularies BINOP_1, BOOLE, FUNCT_1, SUBSET_1, LATTICES, ROBBINS3, ORDERS_1,
LATTICE3, ROBBINS1, OPOSET_1, FILTER_1, REALSET1, RELAT_2, ROBBINS4,
BHSP_1, SYMSP_1, YELLOW_1, ARYTM, FILTER_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, ENUMSET1, SUBSET_1, BINOP_1, RELAT_1,
FUNCT_1, RELSET_1, PARTFUN1, ORDINAL1, NUMBERS, CARD_1, XXREAL_0,
RELAT_2, FUNCT_2, STRUCT_0, LATTICE3, LATTICES, ORDERS_1, ORDERS_2,
ROBBINS1, OPOSET_1, WAYBEL_1, YELLOW_0, YELLOW_1, ROBBINS3;
constructors BINOP_1, REALSET2, WAYBEL_1, LATTICE3, YELLOW_6, OPOSET_1,
ROBBINS3, YELLOW_1, ORDINAL1, XXREAL_0, XCMPLX_0;
registrations SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, REALSET1,
STRUCT_0, LATTICES, YELLOW_0, YELLOW_1, ROBBINS1, OPOSET_1, SHEFFER1,
ROBBINS3, XBOOLE_0, ORDINAL1;
requirements SUBSET, BOOLE, NUMERALS, ARITHM, REAL;
definitions LATTICES, RELAT_2, TARSKI, ROBBINS3, ROBBINS1, REALSET1, SUBSET_1,
ORDERS_2, LATTICE3, YELLOW_0;
theorems ZFMISC_1, STRUCT_0, LATTICE3, FILTER_1, LATTICES, FUNCT_2, ROBBINS3,
ROBBINS1, FILTER_0, YELLOW11, XBOOLE_1, TARSKI, ENUMSET1, CARD_5,
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 Strict:
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
T0: 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 p' = p, q' = q as Element of L by T0;
hereby assume [p,q] in LattRel K; then
p [= q by FILTER_1:32; then
p "\/" q = q by LATTICES:def 3; then
p' "\/" q' = q' by T0; then
p' [= q' by LATTICES:def 3;
hence [p,q] in LattRel L by FILTER_1:32;
end;
assume [p,q] in LattRel L; then
p' [= q' by FILTER_1:32; then
p' "\/" q' = q' by LATTICES:def 3; then
p "\/" q = q by T0; then
p [= q by LATTICES:def 3;
hence thesis by FILTER_1:32;
end;
hence thesis by T0,RELSET_1:def 3;
end;
registration
cluster trivial -> meet-Absorbing (non empty OrthoLattStr);
coherence;
end;
registration
cluster -> lower-bounded 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
consider x being 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 by LATTICES:18
.= (a`` "\/" a`)` by ROBBINS1:def 23
.= c by ROBBINS3:def 7;
hence thesis;
end;
hence thesis by LATTICES:def 13;
end;
cluster -> upper-bounded 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
consider x being 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 by LATTICES:17
.= c by ROBBINS3:def 7;
hence thesis;
end;
hence thesis by LATTICES:def 14;
end;
end;
reserve L for Ortholattice,
a, b, c for Element of L;
theorem yy:
a "\/" a` = Top L & a "/\" a` = Bottom L
proof
thus a "\/" a` = Top L
proof
A: (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 by LATTICES:17
.= a "\/" a` by ROBBINS3:def 7;
end;
b "\/" (a "\/" a`) = a "\/" a` by A;
hence thesis by A,LATTICES:def 17;
end;
A: (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 by LATTICES:18
.= (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 A,LATTICES:def 16;
end;
theorem 3ort:
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 a: 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 ROBBINS1:def 23,a;
then (c` "/\" b`)` "\/" a=((c "\/" b``)`)` "\/" a by ROBBINS3:def 6,a;
then (c` "/\" b`)` "\/" a=(c "\/" b)`` "\/" a by ROBBINS3:def 6,a;
then (c` "/\" b`)` "\/" a=(c "\/" b) "\/" a by ROBBINS3:def 6,a;
then (c` "/\" b`)` "\/" a=a "\/" (c "\/" b) by a,LATTICES:def 4;
then (c` "/\" b`)` "\/" a=c "\/" (a "\/" b) by ROBBINS3:def 1,a;
hence thesis by a,LATTICES:def 4;
end;
thus (for a, b being Element of L holds a = a "/\" (a "\/" b))
by LATTICES:def 9,a;
let a,b be Element of L;
thus a "\/" (b "/\" b`) = a "\/" (b` "\/" b``)` by ROBBINS1:def 23,a
.= a "\/" (b` "\/" b)` by ROBBINS3:def 6,a
.= a "\/" (b "\/" b`)` by a,LATTICES:def 4
.= a "\/" (a "\/" a`)` by ROBBINS3:def 7,a
.= a "\/" (a`` "\/" a`)` by ROBBINS3:def 6,a
.= a "\/" (a` "/\" a) by ROBBINS1:def 23,a
.= (a` "/\" a)"\/"a by a,LATTICES:def 4
.= a by LATTICES:def 8,a;
end;
assume z1: for a, b, c being Element of L holds
(a "\/" b) "\/" c = (c` "/\" b`)` "\/" a;
assume z2:for a, b being Element of L holds a = a "/\" (a "\/" b);
assume z3:for a, b being Element of L holds a = a "\/" (b "/\" b`);
a: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 z3 .= a by z2;
end;
b: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 z1; then
(a "\/" x) "\/" x = x`` "\/" a by a; then
a "\/" x = x`` "\/" a by z3;
hence thesis by z3;
end;
c: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 b
.= x`` by z3;
end;
d: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 b;
hence thesis by c;
end;
e: 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 z3;
hence thesis by d;
end;
f: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 z1;
hence a "\/" b = (b` "/\" a`)` "\/" x by d .= (b` "/\" a`)` by z3;
end;
k1:L is join-commutative
proof
let a,b be Element of L;
set x = a "/\" a`;
x "\/" b = (b` "/\" x`)` by f;
hence b "\/" a = (b` "/\" x`)` "\/" a by d
.= (a "\/" x) "\/" b by z1
.= a "\/" b by z3;
end;
k2:L is join-associative
proof
let a,b,c be Element of L;
set x = a "/\" a`;
thus (a "\/" b) "\/" c = (c` "/\" b`)` "\/" a by z1
.= (b "\/" c) "\/" a by f
.= a "\/" (b "\/" c) by k1,LATTICES:def 4;
end;
l1:L is involutive
proof
let a be Element of L;
a2:a` = a` "/\" (a` "\/" a) by z2;
a` "\/" a = (a` "/\" a``)` by f;
hence a`` = (a` "/\" a``) "\/" a by f,a2
.= a by d;
end;
l2:L is de_Morgan
proof
let a,b be Element of L;
thus (a` "\/" b`)` = (b` "\/" a`)` by k1, LATTICES:def 4
.= (a`` "/\" b``)`` by f
.= a`` "/\" b`` by l1,ROBBINS3:def 6
.= a`` "/\" b by l1,ROBBINS3:def 6
.= a "/\" b by l1,ROBBINS3:def 6;
end;
l3:L is with_Top
proof
let a,b be Element of L;
(a` "/\" a``)` = (b` "/\" b``)` by e;
then (a` "/\" a``)` = b` "\/" b by f;
then a` "\/" a = b` "\/" b by f;
then a` "\/" a = b "\/" b` by k1, LATTICES:def 4;
hence thesis by k1, LATTICES:def 4;
end;
k3:L is join-absorbing by z2,LATTICES:def 9;
k5: L is meet-associative
proof
let a,b,c be Element of L;
thus a "/\" (b "/\" c) = (a` "\/" (b "/\" c)`)` by ROBBINS1:def 23,l2
.= (a` "\/" (b` "\/" c`)``)` by ROBBINS1:def 23,l2
.= (a` "\/" (b` "\/" c`))` by l1, ROBBINS3:def 6
.= ((a` "\/" b`) "\/" c`)` by k2,LATTICES:def 5
.= ((a` "\/" b`)`` "\/" c`)` by l1, ROBBINS3:def 6
.= ((a "/\" b)` "\/" c`)` by ROBBINS1:def 23,l2
.= (a "/\" b) "/\" c by ROBBINS1:def 23,l2;
end;
L is meet-absorbing
proof
let a,b be Element of L;
thus (a "/\" b) "\/" b = (b` "/\" (a "/\" b)`)` by f
.= (b` "/\" (a` "\/" b`)``)` by ROBBINS1:def 23,l2
.= (b` "/\" (a` "\/" b`))` by ROBBINS3:def 6,l1
.= (b` "/\" (b` "\/" a`))` by LATTICES:def 4,k1
.= b`` by z2
.= b by ROBBINS3:def 6,l1;
end;
hence thesis by l1,l2,l3,k1,k2,k3,k5;
end;
theorem theo:
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:21
.= (a`"\/"b`)`` by a1, ROBBINS1:def 23
.= b`"\/"a` by ROBBINS3:def 6;
then a` "/\" b` = b` by LATTICES:def 9;
hence thesis by LATTICES:21;
end;
assume a: for a,b being Element of L st a [= b holds b` [= a`;
let x,y be Element of L;
b:x` [= (x "/\" y)` by a,LATTICES:23;
c:y` [= (x "/\" y)` by a,LATTICES:23;
x` "\/" y` [= (x "/\" y)` by b,c,FILTER_0:6;
then (x "/\" y)`` [= (x` "\/" y`)` by a;
then A: x "/\" y [= (x` "\/" y`)` by ROBBINS3:def 6;
(x` "\/" y`)` [= x`` by a,LATTICES:22; then
d:(x` "\/" y`)` [= x by ROBBINS3:def 6;
(x` "\/" y`)` [= y`` by a,LATTICES:22;
then e: (x` "\/" y`)` [= y by ROBBINS3:def 6;
(x` "\/" y`)` [= x "/\" y by d,e,FILTER_0:7;
hence thesis by A,LATTICES:26;
end;
begin :: Orthomodularity
definition let L be non empty OrthoLattStr;
attr L is orthomodular means :DefModular:
for x, y being Element of L st
x [= y holds y = x "\/" (x` "/\" y);
end;
registration
cluster trivial orthomodular modular Boolean Ortholattice;
existence
proof
consider L being trivial Ortholattice;
L is orthomodular
proof
let x, y be Element of L;
thus thesis by STRUCT_0:def 10;
end;
hence thesis;
end;
end;
theorem twMod:
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 tw1:
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
proof
let L be orthomodular meet-absorbing join-absorbing join-associative
meet-commutative (non empty OrthoLattStr);
let x, y be Element of L;
x [= x "\/" y by LATTICES:22;
hence thesis by DefModular;
end;
definition let L be non empty OrthoLattStr;
attr L is Orthomodular means :DefMod3:
for x, y being Element of L holds
x "\/" (x` "/\" (x "\/" y)) = x "\/" y;
end;
registration
cluster Orthomodular -> orthomodular
(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 B1: L is Orthomodular;
let x, y be Element of L;
assume x [= y; then
x "\/" y = y by LATTICES:def 3;
hence thesis by B1,DefMod3;
end;
cluster orthomodular -> Orthomodular
(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 L is orthomodular; then
for x, y being Element of L holds
x "\/" (x` "/\" (x "\/" y)) = x "\/" y by tw1;
hence thesis by DefMod3;
end;
end;
registration
cluster modular -> orthomodular Ortholattice;
coherence by twMod;
end;
registration
cluster join-Associative meet-Absorbing de_Morgan orthomodular
Ortholattice;
existence
proof
consider L being trivial 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;
L1: 3 \ 2 misses 2 by XBOOLE_1:79;
L2: 1 c= 2 by NAT_1:40; then
Lem1: 3 \ 2 misses 1 by L1,XBOOLE_1:63;
registration
cluster B_6 -> with_suprema with_infima;
coherence
proof
set Z = {0, 1, 3 \ 1, 2, 3 \ 2, 3};
set N = B_6;
AA: the carrier of N = {0, 1, 3 \ 1, 2, 3 \ 2, 3} by YELLOW_1:1;
A1: N is with_suprema
proof
let x,y be Element of N;
A8: Z = the carrier of N by YELLOW_1:1;
thus ex z being Element of N st x <= z & y <= z &
for z' being Element of N st x <= z' & y <= z' holds z <= z'
proof
per cases by A8,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
A9: 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;
x c= z & y c= z by A9,NAT_1:40;
hence x <= z & y <= z by YELLOW_1:3;
let z' be Element of N;
A10: z' is Element of Z by YELLOW_1:1;
assume x <= z' & y <= z';
then
A11: 3\1 c= z' & 2 c= z' by A9,YELLOW_1:3;
A12: now
assume z' = 3\1;
then not 0 in z' & 0 in 2 by YELLOW11:3,TARSKI:def 2,CARD_1:88;
hence contradiction by A11;
end;
A13: now
assume z' = 2;
then not 2 in z' & 2 in 3\1 by YELLOW11:3,TARSKI:def 2;
hence contradiction by A11;
end;
A14: now
assume z' = 3\2;
then not 1 in z' & 1 in 2
by YELLOW11:4,TARSKI:def 1,TARSKI:def 2,CARD_5:1;
hence contradiction by A11;
end;
A00: z' <> 1 by A11,NAT_1:40;
z' <> 0 by A11;
hence z <= z' by A00,A10,A12,A13,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 A: x = 1 & y = 3\1;
B: 1 c= 3 by NAT_1:40;
1 \/ (3\1) = 1 \/ 3 by XBOOLE_1:39 .= 3 by B,XBOOLE_1:12;
then reconsider z = x \/ y as Element of N
by ENUMSET1:def 4,AA,A;
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 A9: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;
x c= z & y c= z by A9,NAT_1:40;
hence x <= z & y <= z by YELLOW_1:3;
let z' be Element of N;
A10: z' is Element of Z by YELLOW_1:1;
assume x <= z' & y <= z';
then
A11: 3\2 c= z' & 1 c= z' by A9,YELLOW_1:3;
A12: now
assume z' = 3\1;
then not 0 in z' & 0 in 1
by YELLOW11:3,TARSKI:def 1,def 2,CARD_1:87;
hence contradiction by A11;
end;
A13: now
assume z' = 2;
then not 2 in z' & 2 in 3\2 by YELLOW11:4,TARSKI:def 1;
hence contradiction by A11;
end;
A14: now
assume z' = 3\2;
then not 0 in z' & 0 in 1
by YELLOW11:4,TARSKI:def 1,CARD_5:1;
hence contradiction by A11;
end;
A00: now
assume z' = 1;
then not 2 in z' & 2 in 3\2 by YELLOW11:4,CARD_5:1,TARSKI:def 1;
hence contradiction by A11;
end;
z' <> 0 by A11;
hence z <= z' by A00,A10,A12,A13,A14,ENUMSET1:def 4;
end;
suppose F1: x = 1 & y = 3;
1 c= 3 by NAT_1:40;
then reconsider z = x \/ y as Element of N by F1,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 AA: x = 1 & y = 2;
1 c= 2 by NAT_1:40;
then reconsider z = x \/ y as Element of N by AA,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 A: y = 1 & x = 3\1;
B: 1 c= 3 by NAT_1:40;
1 \/ (3\1) = 1 \/ 3 by XBOOLE_1:39 .= 3 by B,XBOOLE_1:12;
then reconsider z = x \/ y as Element of N by A,AA,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 A9: 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;
x c= z & y c= z by A9,NAT_1:40;
hence x <= z & y <= z by YELLOW_1:3;
let z' be Element of N;
A10: z' is Element of Z by YELLOW_1:1;
assume x <= z' & y <= z';
then
A11: 3\2 c= z' & 1 c= z' by A9,YELLOW_1:3;
A12: now
assume z' = 3\1;
then not 0 in z' & 0 in 1
by YELLOW11:3,TARSKI:def 1,def 2,CARD_1:87;
hence contradiction by A11;
end;
A13: now
assume z' = 2;
then not 2 in z' & 2 in 3\2
by YELLOW11:4,TARSKI:def 1;
hence contradiction by A11;
end;
A14: now
assume z' = 3\2;
then not 0 in z' & 0 in 1
by YELLOW11:4,TARSKI:def 1,CARD_5:1;
hence contradiction by A11;
end;
A00: now
assume z' = 1;
then not 2 in z' & 2 in 3\2 by YELLOW11:4,CARD_5:1,TARSKI:def 1;
hence contradiction by A11;
end;
z' <> 0 by A11;
hence z <= z' by A00,A10,A12,A13,A14,ENUMSET1:def 4;
end;
suppose F1:y = 1 & x = 3;
1 c= 3 by NAT_1:40;
then reconsider z = x \/ y as Element of N by F1,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 F1: y = 1 & x = 2;
1 c= 2 by NAT_1:40; then
reconsider z = x \/ y as Element of N by F1,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 XBOOLE_1:12,XBOOLE_1:34,L2;
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
A16: 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;
x c= z & y c= z by A16,NAT_1:40;
hence x <= z & y <= z by YELLOW_1:3;
let z' be Element of N;
A10: z' is Element of Z by YELLOW_1:1;
assume x <= z' & y <= z';
then
A11: 3\1 c= z' & 2 c= z' by A16,YELLOW_1:3;
A12: now
assume z' = 3\1;
then not 0 in z' & 0 in 2 by YELLOW11:3,TARSKI:def 2,CARD_1:88;
hence contradiction by A11;
end;
A13: now
assume z' = 2;
then not 2 in z' & 2 in 3\1 by YELLOW11:3,TARSKI:def 2;
hence contradiction by A11;
end;
A14: now
assume z' = 3\2;
then not 1 in z' & 1 in 2
by YELLOW11:4,TARSKI:def 1,TARSKI:def 2,CARD_5:1;
hence contradiction by A11;
end;
A00: z' <> 1 by A11,NAT_1:40;
z' <> 0 by A11;
hence z <= z' by A00,A10,A12,A13,A14,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
A22: x = 2 & y = 3\2;
A: 2 c= 3 by NAT_1:40;
2 \/ (3\2) = 2 \/ 3 by XBOOLE_1:39 .= 3 by A,XBOOLE_1:12;
then x \/ y in Z by A22,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
A23: x = 2 & y = 3;
2 c= 3 by NAT_1:40;
then reconsider z = x \/ y as Element of N by A23,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 XBOOLE_1:12,XBOOLE_1:34,L2;
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
A24: x = 3\2 & y = 2;
A: 2 c= 3 by NAT_1:40;
2 \/ (3\2) = 2 \/ 3 by XBOOLE_1:39 .= 3 by XBOOLE_1:12,A;
then x \/ y in Z by A24,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
A27: x = 3 & y = 2;
2 c= 3 by NAT_1:40;
then reconsider z = x \/ y as Element of N by A27,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;
A8: Z = the carrier of N by YELLOW_1:1;
thus ex z being Element of N st z <= x & z <= y &
for z' being Element of N st z' <= x & z' <= y holds z' <= z
proof
per cases by A8,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
A9: 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 by XBOOLE_1:2;
hence z <= x & z <= y by YELLOW_1:3;
let z' be Element of N;
A10: z' is Element of Z by YELLOW_1:1;
assume z' <= x & z' <= y;
then
A11: z' c= 3\1 & z' c= 2 by A9,YELLOW_1:3;
A12: now
assume z'= 3\1;
then 2 in z' & not 2 in 2 by YELLOW11:3,TARSKI:def 2;
hence contradiction by A11;
end;
A13: now
assume z'= 2;
then 0 in z' & not 0 in 3\1 by YELLOW11:3,CARD_5:1,TARSKI:def 2;
hence contradiction by A11;
end;
A14: now
assume z'= 3\2;
then 2 in z' & not 2 in 2 by YELLOW11:4,TARSKI:def 1;
hence contradiction by A11;
end;
A00: now
assume z'= 1;
then 0 in z' & not 0 in 3\1
by CARD_1:87,TARSKI:def 1,def 2,YELLOW11:3;
hence contradiction by A11;
end;
now
assume z'= 3;
then 2 in z' & not 2 in 2 by CARD_1:89,ENUMSET1:def 1;
hence contradiction by A11;
end;
hence z' <= z by A00,A10,A12,A13,A14,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 ENUMSET1:def 4,AA;
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 Lem1,XBOOLE_0:def 7;
then reconsider z = x /\ y as Element of N
by ENUMSET1:def 4,AA;
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 F1: x = 1 & y = 3;
1 c= 3 by NAT_1:40;
then reconsider z = x /\ y as Element of N by F1,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 ZFMISC_1:19,CARD_1:87,88;
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 AA,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 XBOOLE_0:def 7,Lem1;
then reconsider z = x /\ y as Element of N
by AA,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 F1:y = 1 & x = 3;
1 c= 3 by NAT_1:40;
then reconsider z = x /\ y as Element of N by F1,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 ZFMISC_1:19,CARD_1:87,88;
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:19;
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
A15: 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 A15;
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
A16: 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 by XBOOLE_1:2;
hence z <= x & z <= y by YELLOW_1:3;
let z' be Element of N;
A17: z' is Element of Z by YELLOW_1:1;
assume z' <= x & z' <= y;
then
A18: z' c= 3\1 & z' c= 2 by A16,YELLOW_1:3;
A19: now
assume z'= 3\1;
then 2 in z' & not 2 in 2 by YELLOW11:3,TARSKI:def 2;
hence contradiction by A18;
end;
A20: now
assume z'= 2;
then 0 in z' & not 0 in 3\1 by YELLOW11:3,CARD_5:1,TARSKI:def 2;
hence contradiction by A18;
end;
A21: now
assume z'= 3\2;
then 2 in z' & not 2 in 2 by YELLOW11:4,TARSKI:def 1;
hence contradiction by A18;
end;
A202: now
assume z'= 3;
then 2 in z' & not 2 in 2 by CARD_1:89,ENUMSET1:def 1;
hence contradiction by A18;
end;
now
assume z'= 1;
then 0 in z' & not 0 in 3\1
by CARD_1:87,TARSKI:def 1,def 2,YELLOW11:3;
hence contradiction by A18;
end;
hence z' <= z by A17,A19,A20,A21,ENUMSET1:def 4,A202;
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
A22: 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 A22,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
A23: x = 2 & y = 3;
2 c= 3 by NAT_1:40;
then reconsider z = x /\ y as Element of N by A23,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,YELLOW11:4,ZFMISC_1:19;
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
A24: 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 A24,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
A25: 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 A25;
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
A26: 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 A26;
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
A27: x = 3 & y = 2;
2 c= 3 by NAT_1:40;
then reconsider z = x /\ y as Element of N by A27,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
A28: 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 A28;
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 A1;
end;
end;
theorem LemBA:
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 CosikX1:
for a being set st
a in the carrier of latt B_6 holds a c= 3
proof
let a be set;
assume a in the carrier of latt B_6; then
a = 0 or a = 1 or a = 3 \ 1 or a = 2 or a = 3 \ 2 or a = 3
by ENUMSET1:def 4,LemBA;
hence thesis by NAT_1:40;
end;
definition
func Benzene -> strict OrthoLattStr means :BenDef:
the LattStr of it = latt B_6 &
for x being Element of the carrier of it,
y being Subset of 3 st x = y holds
(the Compl of it).x = y`;
existence
proof
set N = latt B_6;
set M = the carrier of N;
set A = the L_join of N, B = the L_meet of N;
defpred P[set,set] means
for y being Subset of 3 st $1 = y holds $2 = y`;
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 CosikX1;
A1: 1 c= 3 & 2 c= 3 by NAT_1:40;
now per cases by LemBA,ENUMSET1:def 4;
suppose z = 0;
hence z` in M by ENUMSET1:def 4,LemBA;
end;
suppose z = 1;
hence z` in M by ENUMSET1:def 4,LemBA;
end;
suppose z = 3\1; then
z` = 3 /\ 1 by XBOOLE_1:48 .= 1 by A1,XBOOLE_1:28;
hence z` in M by ENUMSET1:def 4,LemBA;
end;
suppose z = 3\2; then
z` = 3 /\ 2 by XBOOLE_1:48 .= 2 by A1,XBOOLE_1:28;
hence z` in M by ENUMSET1:def 4,LemBA;
end;
suppose z = 2;
hence z` in M by ENUMSET1:def 4,LemBA;
end;
suppose z = 3; then
z` = 0 by XBOOLE_1:37;
hence z` in M by ENUMSET1:def 4,LemBA;
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
T1: for x being Element of M,
y being Subset of 3 st x = y holds C.x = y`;
take IT = OrthoLattStr (#M, A, B, C#);
thus thesis by T1;
end;
uniqueness
proof
let A1, A2 be strict OrthoLattStr such that
A0: the LattStr of A1 = latt B_6 &
for x being Element of the carrier of A1,
y being Subset of 3 st x = y holds
(the Compl of A1).x = y` and
A2: the LattStr of A2 = latt B_6 &
for x being Element of the carrier of A2,
y being Subset of 3 st x = y holds
(the Compl of A2).x = y`;
set M = the carrier of A1;
set f1 = the Compl of A1;
set f2 = the Compl of A2;
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 A0,CosikX1;
thus f1.x = y` by A0 .= f2.x by A2,A0;
end;
hence thesis by A0,A2,FUNCT_2:113;
end;
end;
theorem LemBen:
the carrier of Benzene = { 0, 1, 3 \ 1, 2, 3 \ 2, 3 }
proof
A2: the LattStr of Benzene = the LattStr of latt B_6 by BenDef;
LattPOSet latt B_6 = the RelStr of B_6 by LATTICE3:def 15;
hence thesis by A2,YELLOW_1:1;
end;
theorem LemBen2:
the carrier of Benzene c= bool 3
proof
let a be set;
assume A1: a in the carrier of Benzene; then
reconsider x = a as Element of Benzene;
A2: a = 0 or a = 1 or a = 3 \ 1 or a = 2 or a = 3 \ 2 or a = 3
by ENUMSET1:def 4,LemBen,A1;
0 c= 3 & 1 c= 3 & 2 c= 3 & 3 c= 3 by NAT_1:40;
hence thesis by A2;
end;
theorem CosikX:
for a being set st
a in the carrier of Benzene holds a c= {0,1,2} by LemBen2,CARD_1:89;
registration
cluster Benzene -> non empty;
coherence by LemBen;
cluster Benzene -> Lattice-like;
coherence
proof
the LattStr of Benzene = latt B_6 by BenDef;
hence thesis by ROBBINS3:15;
end;
end;
theorem Strict2:
LattPOSet the LattStr of Benzene = B_6
proof
LattPOSet the LattStr of Benzene = LattPOSet latt B_6 by BenDef;
hence thesis by LATTICE3:def 15;
end;
theorem HiHi:
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
A0: a = x & b = y;
hereby assume a <= b; then
x% <= y% by Strict,A0,Strict2;
hence x [= y by LATTICE3:7;
end;
assume x [= y; then
x% <= y% by LATTICE3:7;
hence thesis by A0,Strict2,Strict;
end;
theorem Ha0:
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;
assume
X0: a = x & b = y;
reconsider xy = x "\/" y as Element of B_6 by YELLOW_1:1,LemBen;
x [= x "\/" y & y [= x "\/" y by LATTICES:22; then
X1: a <= xy & b <= xy by X0,HiHi;
t1: 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 YELLOW_1:1,LemBen;
assume d >= a & d >= b; then
x [= e & y [= e by X0,HiHi; then
x "\/" y [= e by FILTER_0:6;
hence thesis by HiHi;
end;
reconsider xy = x "/\" y as Element of B_6 by YELLOW_1:1,LemBen;
x "/\" y [= x & x "/\" y [= y by LATTICES:23; then
x1: xy <= a & xy <= b by X0,HiHi;
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 YELLOW_1:1,LemBen;
assume d <= a & d <= b; then
e [= x & e [= y by X0,HiHi; then
e [= x "/\" y by FILTER_0:7;
hence thesis by HiHi;
end;
hence thesis by t1,X1,YELLOW_0:23,22,x1;
end;
theorem Ha1:
for a, b being Element of B_6 st a = 3 \ 1 & b = 2 holds
a "\/" b = 3 &
a "/\" b = 0
proof
let a,b be Element of B_6;
Z1: the carrier of B_6 = { 0, 1, 3 \ 1, 2, 3 \ 2, 3 } by YELLOW_1:1;
assume Z: a = 3\1 & b = 2;
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;
a c= t & b c= t by NAT_1:40,Z; then
A0:a <= t & b <= t by YELLOW_1:3;
a1:for d being Element of B_6 st d >= a & d >= b holds t <= d
proof
let z' be Element of B_6;
assume z' >= a & z' >= b; then
A11: 3\1 c= z' & 2 c= z' by Z,YELLOW_1:3;
A12: now
assume z' = 3\1;
then not 0 in z' & 0 in 2 by YELLOW11:3,TARSKI:def 2,CARD_1:88;
hence contradiction by A11;
end;
A13: now
assume z' = 2;
then not 2 in z' & 2 in 3\1 by YELLOW11:3,TARSKI:def 2;
hence contradiction by A11;
end;
A14: now
assume z' = 3\2;
then not 1 in z' & 1 in 2
by YELLOW11:4,TARSKI:def 1,TARSKI:def 2,CARD_5:1;
hence contradiction by A11;
end;
A00: z' <> 1 by A11,NAT_1:40;
z' <> 0 by A11;
hence t <= z' by A00,A12,A13,A14,ENUMSET1:def 4,Z1;
end;
z c= a & z c= b by XBOOLE_1:2; then
Z0:z <= a & z <= b by YELLOW_1:3;
for d being Element of B_6 st a >= d & b >= d holds d <= z
proof
let z' be Element of B_6;
assume a >= z' & b >= z'; then
A11: z' c= 3\1 & z' c= 2 by Z,YELLOW_1:3;
A12: now
assume z' = 3\1;
then 2 in z' & not 2 in 2 by YELLOW11:3,TARSKI:def 2;
hence contradiction by A11;
end;
A13: now
assume z' = 2;
then 0 in z' & not 0 in 3\1 by YELLOW11:3,CARD_5:1,TARSKI:def 2;
hence contradiction by A11;
end;
A14: now
assume z' = 3\2;
then 2 in z' & not 2 in 2 by YELLOW11:4,TARSKI:def 1;
hence contradiction by A11;
end;
A00: now
assume z' = 1;
then 0 in z' & not 0 in 3\1
by CARD_1:87,TARSKI:def 1,def 2,YELLOW11:3;
hence contradiction by A11;
end;
now
assume z'= 3;
then 2 in z' & not 2 in 2 by CARD_1:89,ENUMSET1:def 1;
hence contradiction by A11;
end;
hence z' <= z by A00,A12,A13,A14,ENUMSET1:def 4,Z1;
end;
hence thesis by a1,Z0,A0,YELLOW_0:23,YELLOW_0:22;
end;
theorem Ha11:
for a, b being Element of B_6 st a = 3 \ 2 & b = 1 holds
a "\/" b = 3 &
a "/\" b = 0
proof
let a,b be Element of B_6;
Z1: the carrier of B_6 = { 0, 1, 3 \ 1, 2, 3 \ 2, 3 } by YELLOW_1:1;
assume Z: a = 3\2 & b = 1;
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;
a c= t & b c= t by NAT_1:40,Z; then
A0:a <= t & b <= t by YELLOW_1:3;
a1:for d being Element of B_6 st d >= a & d >= b holds t <= d
proof
let z' be Element of B_6;
assume z' >= a & z' >= b; then
A11: 3\2 c= z' & 1 c= z' by Z,YELLOW_1:3;
A12: now
assume z' = 3\2;
then not 0 in z' & 0 in 1 by YELLOW11:4,TARSKI:def 1,CARD_1:87;
hence contradiction by A11;
end;
A13: now
assume z' = 2;
then not 2 in z' & 2 in 3\2 by YELLOW11:4,TARSKI:def 1;
hence contradiction by A11;
end;
A14: now
assume z' = 3\1;
then not 0 in z' & 0 in 1
by YELLOW11:3,TARSKI:def 1,TARSKI:def 2,CARD_5:1;
hence contradiction by A11;
end;
A00: now
assume z'= 1; then
2 in 3\2 & not 2 in z' by YELLOW11:4,TARSKI:def 1,CARD_5:1;
hence contradiction by A11;
end;
z' <> 0 by A11;
hence t <= z' by A00,A12,A13,A14,ENUMSET1:def 4,Z1;
end;
z c= a & z c= b by XBOOLE_1:2; then
Z0:z <= a & z <= b by YELLOW_1:3;
for d being Element of B_6 st a >= d & b >= d holds d <= z
proof
let z' be Element of B_6;
assume a >= z' & b >= z'; then
A11: z' c= 3\2 & z' c= 1 by Z,YELLOW_1:3;
A12: now
assume z'= 3\1;
then 2 in z' & not 2 in 1 by YELLOW11:3,TARSKI:def 2,CARD_5:1;
hence contradiction by A11;
end;
A13: now
assume z'= 2;
then 0 in z' & not 0 in 3\2 by YELLOW11:4,CARD_5:1,TARSKI:def 2,def 1;
hence contradiction by A11;
end;
A14: now
assume z'= 3\2;
then 2 in z' & not 2 in 1 by YELLOW11:4,TARSKI:def 1,CARD_5:1;
hence contradiction by A11;
end;
A00: now
assume z'= 1;
then 0 in z' & not 0 in 3\2
by CARD_1:87,TARSKI:def 1,YELLOW11:4;
hence contradiction by A11;
end;
now
assume z'= 3;
then 2 in z' & not 2 in 1
by CARD_1:89,ENUMSET1:def 1,CARD_5:1,TARSKI:def 1;
hence contradiction by A11;
end;
hence z' <= z by A00,A12,A13,A14,ENUMSET1:def 4,Z1;
end;
hence thesis by a1,Z0,A0,YELLOW_0:23,YELLOW_0:22;
end;
theorem Hax:
for a, b being Element of B_6 st a = 3 \ 1 & b = 1 holds
a "\/" b = 3 &
a "/\" b = 0
proof
let x,y be Element of B_6;
Z1: the carrier of B_6 = { 0, 1, 3 \ 1, 2, 3 \ 2, 3 } by YELLOW_1:1;
assume Z: x = 3\1 & y = 1;
x misses y by Z,XBOOLE_1:79; then
P: x /\ y = 0 by XBOOLE_0:def 7;
B: 1 c= 3 by NAT_1:40;
C: 1 \/ (3\1) = 1 \/ 3 by XBOOLE_1:39 .= 3 by B,XBOOLE_1:12;
reconsider z = 3 as Element of B_6 by ENUMSET1:def 4,Z1;
now
x c= z & y c= z by Z,NAT_1:40;
hence x <= z & y <= z by YELLOW_1:3;
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 C,Z,YELLOW_1:3;
end;
hence x "\/" y = 3 by YELLOW_0:22;
reconsider z = 0 as Element of B_6 by ENUMSET1:def 4,Z1;
now
z c= x & z c= y by XBOOLE_1:2;
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 P;
end;
hence thesis by YELLOW_0:23;
end;
theorem Hax2:
for a, b being Element of B_6 st a = 3 \ 2 & b = 2 holds
a "\/" b = 3 &
a "/\" b = 0
proof
let x,y be Element of B_6;
Z1: the carrier of B_6 = { 0, 1, 3 \ 1, 2, 3 \ 2, 3 } by YELLOW_1:1;
assume Z: x = 3\2 & y = 2;
x misses y by Z,XBOOLE_1:79; then
P: x /\ y = 0 by XBOOLE_0:def 7;
B: 2 c= 3 by NAT_1:40;
C: 2 \/ (3\2) = 2 \/ 3 by XBOOLE_1:39 .= 3 by B,XBOOLE_1:12;
reconsider z = 3 as Element of B_6 by ENUMSET1:def 4,Z1;
now
x c= z & y c= z by Z,NAT_1:40;
hence x <= z & y <= z by YELLOW_1:3;
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 YELLOW_1:3,C,Z;
end;
hence x "\/" y = 3 by YELLOW_0:22;
reconsider z = 0 as Element of B_6 by ENUMSET1:def 4,Z1;
now
z c= x & z c= y by XBOOLE_1:2;
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 P;
end;
hence thesis by YELLOW_0:23;
end;
theorem Haczyk1:
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 A: 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 A,Ha1;
hence thesis by Ha0;
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 A: 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 & aa "/\" bb = 0 by A,Ha11;
hence thesis by Ha0;
end;
theorem Haczyk3:
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 A: 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 A,Hax;
hence thesis by Ha0;
end;
theorem Haczyk4:
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 A: 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 A,Hax2;
hence thesis by Ha0;
end;
theorem twU:
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
let a be Element of Benzene;
set B = Benzene;
set X = bool the carrier of B;
B4: 1 in 3 by YELLOW11:1,ENUMSET1:def 1;
B8: 0 in 3 by YELLOW11:1,ENUMSET1:def 1;
a in the carrier of B; then
reconsider c = a as Subset of 3 by LemBen2;
V0: a` = c` by BenDef; then
A2: 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 ZFMISC_1:142,YELLOW11:1;
V1: a` c= c` by BenDef;
thus a = 0 implies a` = 3 by V0;
thus a = 3 implies a` = 0
proof
assume AA:a = 3;
not 0 in c` by XBOOLE_0:def 4,AA; then
b2: not 0 in a` by BenDef;
1 in c by AA,ENUMSET1:def 1,YELLOW11:1;then
c2: not 1 in a` by V1,XBOOLE_0:def 4;
2 in c by AA,ENUMSET1:def 1,YELLOW11:1; then
not 2 in a` by V1,XBOOLE_0:def 4;
hence thesis by TARSKI:def 2,b2,c2,TARSKI:def 1,ENUMSET1:def 1,A2;
end;
thus a = 1 implies a` = 3 \ 1 by V0;
thus a = 3\1 implies a` = 1
proof
assume aa:a = 3\1; then
bb: 1 in c & 2 in c by TARSKI:def 2,YELLOW11:3; then
cc: not 1 in a` by V1,XBOOLE_0:def 4;
ee: not 2 in a` by V1,XBOOLE_0:def 4,bb;
not 0 in c by aa,TARSKI:def 2,YELLOW11:3;
hence thesis by CARD_5:1,TARSKI:def 2,cc,ee,TARSKI:def 1,A2,
ENUMSET1:def 1,V0,XBOOLE_0:def 4,B8;
end;
thus a = 2 implies a` = 3\2 by V0;
assume h1: a = 3\2; then
2 in c by TARSKI:def 1,YELLOW11:4; then
B3: not 2 in a` by V1,XBOOLE_0:def 4;
not 1 in c by h1,TARSKI:def 1,YELLOW11:4; then
B1: 1 in a` by V0,XBOOLE_0:def 4,B4;
not 0 in c by h1,TARSKI:def 1,YELLOW11:4; then
0 in a` by V0,XBOOLE_0:def 4,B8;
hence thesis by CARD_5:1,TARSKI:def 1,B1,A2,
ENUMSET1:def 1,B3,TARSKI:def 2;
end;
theorem Inkl:
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 YELLOW_1:1,LemBen;
hereby assume a [= b; then
x <= y by HiHi;
hence a c= b by YELLOW_1:3;
end;
assume a c= b; then
x <= y by YELLOW_1:3;
hence thesis by HiHi;
end;
theorem KL1:
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 by XBOOLE_1:2; then
a [= x by Inkl;
hence thesis by LATTICES:21;
end;
theorem Bot2:
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 by XBOOLE_1:2; then
a [= x by Inkl;
hence thesis by LATTICES:def 3;
end;
theorem Bot1:
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 CosikX,YELLOW11:1; then
x [= a by Inkl;
hence thesis by LATTICES:def 3;
end;
registration
cluster Benzene -> lower-bounded;
coherence
proof
reconsider B = 0 as Element of Benzene by LemBen,ENUMSET1:def 4;
take B;
for a being Element of Benzene holds
B "/\" a = B & a "/\" B = B by KL1;
hence thesis;
end;
cluster Benzene -> upper-bounded;
coherence
proof
reconsider B = 3 as Element of Benzene by LemBen,ENUMSET1:def 4;
take B;
for a being Element of Benzene holds
B "\/" a = B & a "\/" B = B by Bot1;
hence thesis;
end;
end;
theorem
Top Benzene = 3
proof
reconsider x = 3 as Element of Benzene by LemBen,ENUMSET1:def 4;
for a being Element of Benzene holds
x "\/" a = x & a "\/" x = x by Bot1;
hence thesis by LATTICES:def 17;
end;
theorem Stan0:
Bottom Benzene = 0
proof
reconsider x = 0 as Element of Benzene by LemBen,ENUMSET1:def 4;
for a being Element of Benzene holds
x "/\" a = x & a "/\" x = x by KL1;
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 ENUMSET1:def 4,LemBen;
suppose x:a = 0;then
a` = 3 by twU;
hence thesis by x,twU;
end;
suppose x:a = 1;then
a` = 3\1 by twU;
hence thesis by x,twU;
end;
suppose x:a = 3\1;then
a` = 1 by twU;
hence thesis by x,twU;
end;
suppose x:a = 2;then
a` = 3\2 by twU;
hence thesis by x,twU;
end;
suppose x:a = 3\2;then
a` = 2 by twU;
hence thesis by x,twU;
end;
suppose x:a = 3;then
a` = 0 by twU;
hence thesis by x,twU;
end;
end;
hence I:B is involutive by ROBBINS3:def 6;
B: for a being Element of B holds a "\/" a` = 3
proof
let a be Element of B;
per cases by ENUMSET1:def 4,LemBen;
suppose x:a = 0;then
a` = 3 by twU;
hence thesis by x,Bot2;
end;
suppose x:a = 1; then
a` = 3\1 by twU;
hence thesis by x,Haczyk3;
end;
suppose x:a = 3\1; then
a` = 1 by twU;
hence thesis by x,Haczyk3;
end;
suppose x:a = 2;then
a` = 3\2 by twU;
hence thesis by x,Haczyk4;
end;
suppose x:a = 3\2;then
a` = 2 by twU;
hence thesis by x,Haczyk4;
end;
suppose a = 3;
hence thesis by Bot1;
end;
end;
thus B is with_Top
proof
let a,b be Element of B;
a "\/" a` = 3 by B;
hence thesis by B;
end;
thus B is de_Morgan
proof
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 CosikX;
reconsider x, y as Subset of 3 by CARD_1:89;
A1: a` = x` by BenDef;
A2: b` = y` by BenDef;
assume a [= b; then
x c= y by Inkl; then
y` c= x` by SUBSET_1:31;
hence thesis by A1,A2,Inkl;
end;
hence thesis by theo,I;
end;
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 x = 1; set y = 2;
reconsider x, y as Element of Benzene by LemBen,ENUMSET1:def 4;
d: x` = 3\1 by twU;
f: for z being set holds z in 1 implies z in 2
proof
let z be set;
assume z in 1;
then z = 0 by TARSKI:def 1,CARD_5:1;
hence thesis by CARD_1:88,TARSKI:def 2;
end;
1 c= 2 by f,TARSKI:def 3;then
a: x [= y by Inkl;
x "\/" (x` "/\" y) = x
proof
x` "/\" y = 0 by Haczyk1,d;
hence thesis by LATTICES:39,Stan0;
end;
hence thesis by a;
end;
hence thesis by DefModular;
end;
end;
begin :: Orthogonality
definition let L be Ortholattice, a,b be Element of L;
pred a, b are_orthogonal means :orthogonal:
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` by orthogonal;
then a "/\" a` = a by LATTICES:21;
hence thesis by yy;
end;
assume a = Bottom L;
then a "/\" a` = a by yy;
then a [= a` by LATTICES:21;
hence thesis by orthogonal;
end;
definition let L be Ortholattice; let a, b be Element of L;
redefine pred a,b are_orthogonal;
symmetry
proof
let a, b be Element of L;
assume a _|_ b;then
a [= b` by orthogonal;
then b`` [= a` by theo;
then b [= a` by ROBBINS3:def 6;
hence thesis by orthogonal;
end;
end;
theorem
a _|_ b & a _|_ c implies a _|_ (b "/\" c) & a _|_ (b "\/" c)
proof
assume a: a _|_ b;
assume b: a _|_ c;
c:a [= b` by orthogonal,a;
d:a [= c` by orthogonal,b;
b`[= b` "\/" c` by LATTICES:22;then
a [= b` "\/" c` by c, LATTICES:25;then
a [= (b` "\/" c`)`` by ROBBINS3:def 6; then
a [= (b "/\" c)` by ROBBINS1:def 23;
hence a _|_ (b "/\" c) by orthogonal;
a "/\" c` [= b` "/\" c` by c,LATTICES:27;then
a [= b` "/\" c` by d,LATTICES:21;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 a _|_ (b "\/" c) by orthogonal;
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 z1: L is orthomodular;
let x,y be Element of L;
assume z2: y` [= x;
assume z3: x "/\" y = Bottom L;
thus x = y` "\/" (y`` "/\" x) by z1,z2,DefModular
.= y` "\/" (y "/\" x) by ROBBINS3:def 6
.= y` by LATTICES:39,z3;
end;
assume z: 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 a: (x"\/"(x`"/\"y))``[=y by ROBBINS3:def 6;
b: (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 yy;
(x "\/" (x` "/\" y))`` = y by a,b,z;
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 z1: L is orthomodular;
let x,y be Element of L;
assume z2: x _|_ y;
assume z3: x "\/" y = Top L;
x [= y` by z2,orthogonal;
hence y` = x "\/" (x` "/\" y`) by z1,DefModular
.= 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 yy,z3
.= x "\/" (x`"/\"x) by ROBBINS1:def 23
.= x by LATTICES:def 8;
end;
assume z: 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 a: x "\/" (x` "/\" y) [= y`` by ROBBINS3:def 6;
b: 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 yy;
x "\/" (x` "/\" y) _|_ y` by a,orthogonal; then
x "\/" (x` "/\" y) = y`` by b,z;
hence thesis by ROBBINS3:def 6;
end;
theorem twDual:
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 z1:L is orthomodular;
let a,b be Element of L;
assume b [= a;
then a` [= b` by theo;
then b` = a` "\/" (a`` "/\" b`) by DefModular,z1
.= 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 z1: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 theo; then
b` = a`"/\"(a``"\/"b`) by z1
.= 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)
proof
assume a:L is orthomodular;
let a,b;
a "/\" b [= a by LATTICES:23;
hence thesis by twDual,a;
end;
assume z1: 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 z2: b [= a;
hence b = a "/\" b by LATTICES:21
.= a "/\" (a` "\/" (a "/\" b)) by z1
.= a "/\" (a` "\/" b) by LATTICES:21,z2;
end;
hence thesis by twDual;
end;
theorem dziw:
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 z:L is orthomodular;
let a,b be Element of L;
a "\/" b = a "\/" ((a "\/" b) "/\" a`) by tw1,z;
hence thesis by LATTICES:def 9;
end;
assume z1:for a,b being Element of L holds
a "\/" b = ((a "\/" b) "/\" a) "\/" ((a "\/" b) "/\" a`);
let x,y be Element of L;
assume z2: x [= y;
hence y = x "\/" y by LATTICES:def 3
.= ((x "\/" y) "/\" x) "\/" ((x "\/" y) "/\" x`) by z1
.= (y "/\" x) "\/" ((x "\/" y) "/\" x`) by z2,LATTICES:def 3
.= (y "/\" x) "\/" (y "/\" x`) by z2,LATTICES:def 3
.= x "\/" (x` "/\" y) by LATTICES:21,z2;
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 z1: L is orthomodular;
let a,b;
assume z2: a [= b;
b: (a"/\"b)[=(a"\/"b) by FILTER_0:3,LATTICES:23;
c: (a"/\"b)[=(b"\/"a`) by LATTICES:23,FILTER_0:3;
e: (b"/\"a`)[=(b"\/"a`) by FILTER_0:3,LATTICES:23;
f: (b"/\"a`)[=(a"\/"b) by FILTER_0:3,LATTICES:23;
g: (a"/\"b)"\/" (b"/\"a`)[=(a"\/"b) by FILTER_0:6,b,f;
(a"/\"b)"\/" (b"/\"a`)[=(b"\/"a`) by FILTER_0:6,c,e;then
B: (a"/\"b)"\/" (b"/\"a`)[=(a"\/"b)"/\"(b"\/"a`) by FILTER_0:7,g;
h: a "\/"b = ((a"\/"b)"/\"a)"\/"((a"\/"b)"/\"a`) by z1,dziw
.= (b"/\"a)"\/"((a"\/"b)"/\"a`) by z2,LATTICES:def 3
.= (b"/\"a)"\/"(b"/\"a`) by z2,LATTICES:def 3;
(a"\/"b)"/\"(b"\/"a`)[= a"\/"b by LATTICES:23;
hence thesis by B,LATTICES:26,h;
end;
assume z1:for a,b st a[=b holds
(a "\/" b) "/\" (b "\/" a`) = (a "/\" b) "\/" (b "/\" a`);
let a,b;
assume z2: a [= b;
then (a "\/" b) "/\" (b "\/" a`) = (a "/\" b) "\/" (b "/\" a`) by z1
.= a "\/" (a` "/\" b) by LATTICES:21,z2;
hence a "\/" (a` "/\" b) = b "/\" (b "\/" a`) by LATTICES:def 3,z2
.= b by LATTICES:def 9;
end;
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 a:L is Orthomodular_Lattice;
thus (for a, b, c being Element of L holds
(a "\/" b) "\/" c = (c` "/\" b`)` "\/" a) by 3ort,a;
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: a "\/"b [= ((a"\/"b)"/\"(a"\/"c))"\/"((a"\/"b)"/\"a`)
proof
c:a"\/"b=((a"\/"b)"/\"a)"\/"((a"\/"b)"/\"a`) by a,dziw;
a"/\"(a"\/"b)[=(a"\/"c)"/\"(a"\/"b) by LATTICES:27,a,LATTICES:22;then
(a"\/"b)"/\"a[=(a"\/"c)"/\"(a"\/"b) by a,LATTICES:def 6;then
(a"\/"b)"/\"a[= (a"\/"b)"/\"(a"\/"c) by a,LATTICES:def 6;then
((a"\/"b)"/\"a`)"\/"((a"\/"b)"/\"a)[=
((a"\/"b)"/\"a`)"\/"((a"\/"b)"/\"(a"\/"c)) by a,FILTER_0:1;then
((a"\/"b)"/\"a)"\/"((a"\/"b)"/\"a`)[=
((a"\/"b)"/\"a`)"\/"((a"\/"b)"/\"(a"\/"c))by a,LATTICES:def 4;
hence thesis by c,a,LATTICES:def 4;
end;
((a"\/"b)"/\"(a"\/"c))"\/"((a"\/"b)"/\"a`) [= a "\/"b
proof
b:(a"\/"b)"/\"a` [= a "\/"b by LATTICES:23,a;
(a"\/"b)"/\"(a"\/"c) [= a "\/"b by LATTICES:23,a;
hence thesis by FILTER_0:6,b,a;
end;
hence thesis by A,LATTICES:26,a;
end;
thus for a, b being Element of L holds a = a "\/" (b "/\" b`) by 3ort,a;
end;
assume z1:(for a, b, c being Element of L holds
(a "\/" b) "\/" c = (c` "/\" b`)` "\/" a);
assume z2: (for a, b,c being Element of L holds
a "\/" b = ((a"\/"b)"/\"(a"\/"c))"\/"((a"\/"b)"/\"a`));
assume z3:(for a, b being Element of L holds a = a "\/" (b "/\" b`));
A: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 z3
.= ((a"\/"b)"/\"(a"\/"c))"\/"((a"\/"b)"/\"a`) by z2
.= (a"/\"(a"\/"c))"\/"((a"\/"b)"/\"a`) by z3
.= (a"/\"(a"\/"c))"\/"(a"/\"a`) by z3
.= a"/\"(a"\/"c) by z3;
end;
B:L is Ortholattice by z1,z3,A,3ort;
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 z2;
hence thesis by z3;
end;
hence thesis by dziw,B;
end;
reserve L for join-Associative meet-Absorbing de_Morgan orthomodular
Lattice-like (non empty OrthoLattStr);
reserve v0,v1,v2,v63,v64,v65,v66 for Element of L;
registration
cluster -> with_Top (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
A7: (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 DefMod3;
end;
A8: 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;
A11: v64 "\/" c(c(v64)) = v64
proof
now let v64,v1;
(c(v64) "\/" c((c(c(v64)) "\/" c(v1)))) = c(v64) by A8;
hence (v64 "\/" c(c(v64))) = v64 by A8;
end;
hence thesis;
end;
A15: v64 "\/" v65 = v65 "\/" (v64 "\/" c(c(v65)))
proof
v65 "\/" c(c(v65)) = v65 by A11;
hence thesis by ROBBINS3:def 1;
end;
A20: v64 "\/" c((c(v64) "\/" v1)) = v64
proof
(c(v64) "\/" c((c(c(c(v64))) "\/" c((c(v64) "\/" v1))))) =
(c(v64) "\/" v1) by A7;
hence thesis by A8;
end;
A24: v64 "\/" v65 = (v65 "\/" (v64 "\/" c((c(v65) "\/" v1))))
proof
v65 "\/" c((c(v65) "\/" v1)) = v65 by A20;
hence thesis by ROBBINS3:def 1;
end;
A33: (v64 "\/" c((c(c(v64)) "\/" c((v1 "\/" v64)))))
= (v64 "\/" (v1 "\/" c(c(v64))))
proof
(v64 "\/" (v1 "\/" c(c(v64)))) = (v1 "\/" v64) by A15;
hence thesis by A7;
end;
A35: (v64 "\/" c((c(c(v64)) "\/" c((v1 "\/" v64))))) = v1 "\/" v64
proof
v64 "\/" (v1 "\/" v64``) = v1 "\/" v64 by A15;
hence thesis by A33;
end;
A50: v64 "\/" v64`` = v64```` "\/" v64
proof
v64```` "\/" v64`` = v64`` by A11;
hence thesis by A15;
end;
A52: v64 = v64```` "\/" v64
proof
v64 "\/" v64`` = v64 by A11;
hence thesis by A50;
end;
A62: v65``` "\/" v65` = v65```
proof
v65```` "\/" v65 = v65 by A52;
hence thesis by A20;
end;
A64: v65` = v65```
proof
v65``` "\/" v65` = v65` by A11;
hence thesis by A62;
end;
A69: (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 A52;
hence thesis by A7;
end;
A71: (c(c(v65)) "\/" c((c(c(c(c(c(c(v65)))))) "\/" c(v65))))
= (c(c(c(c(v65)))) "\/" v65)
proof
v65``` = v65` by A64;
hence thesis by A69;
end;
A73: (c(c(v65)) "\/" c((c(c(c(c(v65)))) "\/" c(v65))))
= c(c(c(c(v65)))) "\/" v65
proof
v65``` = v65` by A64;
hence thesis by A71;
end;
A75: (c(c(v65)) "\/" c((c(c(v65)) "\/" c(v65))))
= c(c(c(c(v65)))) "\/" v65
proof
v65``` = v65` by A64;
hence thesis by A73;
end;
A77: (c(c(v65)) "\/" c((c(c(v65)) "\/" c(v65)))) = (c(c(v65)) "\/" v65)
proof
v65``` = v65` by A64;
hence thesis by A75;
end;
A79: (c(c(v65)) "\/" c((c(c(v65)) "\/" c(v65)))) = v65
proof
v65`` "\/" v65 = v65 by A11;
hence thesis by A77;
end;
A82: (c(c(v0)) "\/" c((v65 "\/" c(v0)))) = v0``
proof
v0``` = v0` by A64;
hence thesis by A20;
end;
A85: v0`` = v0
proof
(c(c(v0)) "\/" c((c(c(v0)) "\/" c(v0)))) = v0`` by A82;
hence thesis by A79;
end;
A87: (v0 "\/" c((v0 "\/" c((v1 "\/" v0))))) = v1 "\/" v0
proof
v0`` = v0 by A85;
hence thesis by A35;
end;
A89: (c(v0) "\/" c((v0 "\/" v65))) = v0`
proof
v0`` = v0 by A85;
hence thesis by A20;
end;
A148: (v64 "\/" (v1 "\/" c(v64))) = (c(v64) "\/" v64)
proof
(c(v64) "\/" c((c(v64) "\/" c((v1 "\/" c(v64))))))=(v1 "\/" c(v64))
by A87;
hence thesis by A24;
end;
A152: ((v0 "\/" v1) "\/" c(v0))=(c((v0 "\/" v1)) "\/" (v0 "\/" v1))
proof
(v0` "\/" c((v0 "\/" v1)))=c(v0) by A89;
hence thesis by A148;
end;
A154: (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 A152;
end;
A158: (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 A148;
end;
A159: (v0 "\/" (v1 "\/" (v65 "\/" c((v0 "\/" v1)))))
=(v0 "\/" (v1 "\/" c(v0)))
proof
(c((v0 "\/" v1)) "\/" (v0 "\/" v1))=(v0 "\/" (v1 "\/" c(v0))) by A154;
hence thesis by A158;
end;
A164: (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 A148;
end;
A166: (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 A159;
hence (c((v1 "\/" v0)) "\/" (v0 "\/" v1))=(v0 "\/" (v1 "\/" c(v0)))
by A164;
end;
hence thesis;
end;
A172: (v2 "\/" (v1 "\/" c(v2))) =
((v1 "\/" v2) "\/" (v65 "\/" c((v1 "\/" v2))))
proof
(c((v1 "\/" v2)) "\/" (v2 "\/" v1))=(v2 "\/" (v1 "\/" c(v2))) by A166;
hence thesis by A148;
end;
A174: (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 A172;
end;
A176: v2 "\/" (v1 "\/" v2`) = v1 "\/" (v2 "\/" v1`)
proof
now let v65,v2,v1;
(v1 "\/" (v2 "\/" (v65 "\/" c((v1 "\/" v2))))) =
(v1 "\/" (v2 "\/" c(v1))) by A159;
hence v2 "\/" (v1 "\/" c(v2)) = v1 "\/" (v2 "\/" c(v1)) by A174;
end;
hence thesis;
end;
A183: v0 "\/" v0` = v1 "\/" (v0 "\/" v1`)
proof
v0 "\/" (v1 "\/" v0`) = v0 "\/" v0` by A148;
hence thesis by A176;
end;
let v1,v0;
v1 "\/" (v0 "\/" v1`) = v1 "\/" v1` by A148;
hence thesis by A183;
end;
hence thesis by ROBBINS3:def 7;
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 z1: L is join-Associative;
assume z2: L is meet-Absorbing;
assume z3: L is de_Morgan;
assume z4: L is Orthomodular;
a: 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 z2,ROBBINS3:def 3
.= x "\/" (x` "\/" y`)` by z3,ROBBINS1:def 23;
end;
b: for x being Element of L holds x = x "\/" x``
proof
let x be Element of L;
thus x = x "\/" (x` "\/" (x`` "\/" x``)`)` by a
.= x "\/" (x` "\/" (x` "/\" x`))` by z3,ROBBINS1:def 23
.= x "\/" x`` by z2,ROBBINS3:def 3;
end;
c: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 z4,DefMod3
.= x "\/" (x`` "\/" (x "\/" y)`)` by z3,ROBBINS1:def 23;
end;
d: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 c
.= x by a;
end;
e: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 b;
hence thesis by z1,ROBBINS3:def 1;
end;
f: 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 e
.= x by d;
end;
g: for x being Element of L holds x` "\/" x` = x`
proof
let x be Element of L;
thus x` = x` "\/" (x "\/" x``)` by f
.= x` "\/" x` by b;
end;
h:for x being Element of L holds x`` "\/" x = x
proof
let x be Element of L;
x`` "\/" x = x "\/" (x`` "\/" x``) by e
.= x "\/" x`` by g;
hence thesis by b;
end;
i:for x being Element of L holds x```` "\/" x = x
proof
let x be Element of L;
x```` "\/" x = x "\/" (x```` "\/" x``) by e
.= x "\/" x`` by h;
hence thesis by b;
end;
j: for x being Element of L holds x``` = x`
proof
let x be Element of L;
x``` = x``` "\/" (x```` "\/" x)` by d
.= x``` "\/" x` by i;
hence thesis by h;
end;
k:for x being Element of L holds x`` "\/" (x`` "\/" x`)` = x
proof
let x be Element of L;
x = x```` "\/" x by i
.= x```` "\/" (x`````` "\/" (x```` "\/" x)`)` by c
.= x```` "\/" (x`````` "\/" x`)` by i
.= x`` "\/" (x`````` "\/" x`)` by j
.= x`` "\/" (x```` "\/" x`)` by j;
hence thesis by j;
end;
l: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 f;
hence thesis by j;
end;
m:for x being Element of L holds x`` = x
proof
let x be Element of L;
thus x = x`` "\/" (x`` "\/" x`)` by k
.= x`` by l;
end;
l3: L is join-absorbing
proof
let a,b be Element of L;
a "/\" (a "\/" b) = (a` "\/" (a "\/" b)`)` by z3,ROBBINS1:def 23
.= (a` "\/" (a`` "\/" b)`)` by m
.= a`` by d
.= a by m;
hence thesis;
end;
l1: L is meet-Associative
proof
let a,b,c be Element of L;
thus a "/\" (b "/\" c) = a "/\" (b` "\/" c`)` by z3,ROBBINS1:def 23
.= (a` "\/" (b` "\/" c`)``)` by z3,ROBBINS1:def 23
.= (a` "\/" (b` "\/" c`))` by m
.= (b` "\/" (a` "\/" c`))` by z1,ROBBINS3:def 1
.= (b` "\/" (a` "\/" c`)``)` by m
.= (b` "\/" (a "/\" c)`)` by z3,ROBBINS1:def 23
.= b "/\" (a "/\" c) by z3,ROBBINS1:def 23;
end;
reconsider L' = L as Lattice-like (non empty OrthoLattStr)
by z2,l1,z1,l3;
reconsider L' as join-Associative meet-Absorbing de_Morgan Orthomodular
Lattice-like (non empty OrthoLattStr) by z3,z4;
L' is with_Top;
hence L is Orthomodular_Lattice by m,ROBBINS3:def 6;
end;