robbins4.miz
begin
registration
let L be
Lattice;
cluster the LattStr of L ->
Lattice-like;
coherence by
ROBBINS3: 15;
end
theorem ::
ROBBINS4:1
Th1: for K,L be
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 be
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 be
Element of IT st for a be
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 be
Element of IT st for a be
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 ::
ROBBINS4:2
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 ::
ROBBINS4:3
Th3: for L be non
empty
OrthoLattStr holds L is
Ortholattice iff (for a,b,c be
Element of L holds ((a
"\/" b)
"\/" c)
= ((((c
` )
"/\" (b
` ))
` )
"\/" a)) & (for a,b be
Element of L holds a
= (a
"/\" (a
"\/" b))) & for a,b be
Element of L holds a
= (a
"\/" (b
"/\" (b
` )))
proof
let L be non
empty
OrthoLattStr;
thus L is
Ortholattice implies (for a,b,c be
Element of L holds ((a
"\/" b)
"\/" c)
= ((((c
` )
"/\" (b
` ))
` )
"\/" a)) & (for a,b be
Element of L holds a
= (a
"/\" (a
"\/" b))) & for a,b be
Element of L holds a
= (a
"\/" (b
"/\" (b
` )))
proof
assume
A1: L is
Ortholattice;
thus for a,b,c be
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 be
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 be
Element of L holds ((a
"\/" b)
"\/" c)
= ((((c
` )
"/\" (b
` ))
` )
"\/" a);
assume
A3: for a,b be
Element of L holds a
= (a
"/\" (a
"\/" b));
assume
A4: for a,b be
Element of L holds a
= (a
"\/" (b
"/\" (b
` )));
A5: for a be
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 be
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 be
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 be
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 be
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 be
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 ::
ROBBINS4:4
Th4: for L be
involutive
Lattice-like non
empty
OrthoLattStr holds L is
de_Morgan iff for a,b be
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 be
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 be
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
definition
let L be non
empty
OrthoLattStr;
::
ROBBINS4:def1
attr L is
orthomodular means
:
Def1: for x,y be
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 ::
ROBBINS4:5
Th5: for L be
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 ::
ROBBINS4:6
Th6: for L be
orthomodular
meet-absorbing
join-absorbing
join-associative
meet-commutative non
empty
OrthoLattStr, x,y be
Element of L holds (x
"\/" ((x
` )
"/\" (x
"\/" y)))
= (x
"\/" y) by
LATTICES: 5,
Def1;
definition
let L be non
empty
OrthoLattStr;
::
ROBBINS4:def2
attr L is
Orthomodular means
:
Def2: for x,y be
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
definition
::
ROBBINS4:def3
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 be
Element of N st x
<= z & y
<= z & for z9 be
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,
XBOOLE_1: 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,
XBOOLE_1: 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 be
Element of N st z
<= x & z
<= y & for z9 be
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,
CARD_1: 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,
CARD_1: 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,
YELLOW11: 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,
YELLOW11: 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 ::
ROBBINS4:7
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 ::
ROBBINS4:8
Th8: for a be
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
::
ROBBINS4:def4
func
Benzene ->
strict
OrthoLattStr means
:
Def4: the LattStr of it
= (
latt
B_6 ) & for x be
Element of it , y be
Subset of 3 st x
= y holds (the
Compl of it
. x)
= (y
` );
existence
proof
defpred
P[
set,
set] means for y be
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 be
Element of M holds ex y be
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 be
Function of M, M st for x be
Element of M holds
P[x, (f
. x)] from
FUNCT_2:sch 3(
A1);
then
consider C be
UnOp of M such that
A4: for x be
Element of M, y be
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 be
Element of A1, y be
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 be
Element of A2, y be
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 be
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 ::
ROBBINS4:9
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 ::
ROBBINS4:10
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 ::
ROBBINS4:11
Th11: for a be
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 ::
ROBBINS4:12
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 ::
ROBBINS4:13
Th13: for a,b be
Element of
B_6 , x,y be
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 ::
ROBBINS4:14
Th14: for a,b be
Element of
B_6 , x,y be
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 be
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 be
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,
YELLOW_0: 23;
end;
theorem ::
ROBBINS4:15
Th15: for a,b be
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 be
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 be
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,
YELLOW_0: 23;
end;
theorem ::
ROBBINS4:16
Th16: for a,b be
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 be
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 be
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,
YELLOW_0: 23;
end;
theorem ::
ROBBINS4:17
Th17: for a,b be
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 ::
ROBBINS4:18
Th18: for a,b be
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 ::
ROBBINS4:19
Th19: for a,b be
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 ::
ROBBINS4:20
for a,b be
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 ::
ROBBINS4:21
Th21: for a,b be
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 ::
ROBBINS4:22
Th22: for a,b be
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 ::
ROBBINS4:23
Th23: for a be
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,
TARSKI: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,
TARSKI: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,
YELLOW11: 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,
TARSKI:def 2;
end;
theorem ::
ROBBINS4:24
Th24: for a,b be
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 ::
ROBBINS4:25
Th25: for a,x be
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 ::
ROBBINS4:26
Th26: for a,x be
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 ::
ROBBINS4:27
Th27: for a,x be
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 be
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 be
Element of
Benzene holds (B
"\/" a)
= B & (a
"\/" B)
= B by
Th27;
hence thesis;
end;
end
theorem ::
ROBBINS4:28
(
Top
Benzene )
= 3
proof
reconsider x = 3 as
Element of
Benzene by
Th9,
ENUMSET1:def 4;
for a be
Element of
Benzene holds (x
"\/" a)
= x & (a
"\/" x)
= x by
Th27;
hence thesis by
LATTICES:def 17;
end;
theorem ::
ROBBINS4:29
Th29: (
Bottom
Benzene )
=
0
proof
reconsider x =
0 as
Element of
Benzene by
Th9,
ENUMSET1:def 4;
for a be
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 be
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 be
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 be
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 be
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 be
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
definition
let L be
Ortholattice, a,b be
Element of L;
::
ROBBINS4:def5
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 ::
ROBBINS4:30
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;
:: original:
are_orthogonal
redefine
pred a,b
are_orthogonal ;
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 ::
ROBBINS4:31
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
theorem ::
ROBBINS4:32
L is
orthomodular iff for a,b be
Element of L st (b
` )
[= a & (a
"/\" b)
= (
Bottom L) holds a
= (b
` )
proof
thus L is
orthomodular implies for a,b be
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 be
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 ::
ROBBINS4:33
L is
orthomodular iff for a,b be
Element of L st a
_|_ b & (a
"\/" b)
= (
Top L) holds a
= (b
` )
proof
thus L is
orthomodular implies for a,b be
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 be
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 ::
ROBBINS4:34
Th34: L is
orthomodular iff for a,b be
Element of L st b
[= a holds (a
"/\" ((a
` )
"\/" b))
= b
proof
thus L is
orthomodular implies for a,b be
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 be
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 ::
ROBBINS4:35
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 ::
ROBBINS4:36
Th36: L is
orthomodular iff for a,b be
Element of L holds (a
"\/" b)
= (((a
"\/" b)
"/\" a)
"\/" ((a
"\/" b)
"/\" (a
` )))
proof
thus L is
orthomodular implies for a,b be
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 be
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 ::
ROBBINS4:37
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;
::$Notion-Name
theorem ::
ROBBINS4:38
for L be non
empty
OrthoLattStr holds L is
Orthomodular_Lattice iff (for a,b,c be
Element of L holds ((a
"\/" b)
"\/" c)
= ((((c
` )
"/\" (b
` ))
` )
"\/" a)) & (for a,b,c be
Element of L holds (a
"\/" b)
= (((a
"\/" b)
"/\" (a
"\/" c))
"\/" ((a
"\/" b)
"/\" (a
` )))) & for a,b be
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 be
Element of L holds ((a
"\/" b)
"\/" c)
= ((((c
` )
"/\" (b
` ))
` )
"\/" a)) & (for a,b,c be
Element of L holds (a
"\/" b)
= (((a
"\/" b)
"/\" (a
"\/" c))
"\/" ((a
"\/" b)
"/\" (a
` )))) & for a,b be
Element of L holds a
= (a
"\/" (b
"/\" (b
` )))
proof
assume
A1: L is
Orthomodular_Lattice;
hence for a,b,c be
Element of L holds ((a
"\/" b)
"\/" c)
= ((((c
` )
"/\" (b
` ))
` )
"\/" a) by
Th3;
thus for a,b,c be
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,
LATTICES: 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 be
Element of L holds ((a
"\/" b)
"\/" c)
= ((((c
` )
"/\" (b
` ))
` )
"\/" a);
assume
A5: for a,b,c be
Element of L holds (a
"\/" b)
= (((a
"\/" b)
"/\" (a
"\/" c))
"\/" ((a
"\/" b)
"/\" (a
` )));
assume
A6: for a,b be
Element of L holds a
= (a
"\/" (b
"/\" (b
` )));
A7: for a,b be
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 be
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("\/"))
= v0
proof
(v0
"/\" v1)
=
c("\/") by
ROBBINS1:def 23;
hence thesis by
ROBBINS3:def 3;
end;
A2: (v64
"\/"
c(c))
= v64
proof
now
let v64, v1;
(
c(v64)
"\/"
c("\/"))
=
c(v64) by
A1;
hence (v64
"\/"
c(c))
= v64 by
A1;
end;
hence thesis;
end;
A3: (v0
"\/"
c("\/"))
= (v0
"\/" v1)
proof
(
c(v0)
"/\" (v0
"\/" v1))
=
c("\/") by
ROBBINS1:def 23;
hence thesis by
Def2;
end;
A4: (v64
"\/"
c("\/"))
= v64
proof
(
c(v64)
"\/"
c("\/"))
= (
c(v64)
"\/" v1) by
A3;
hence thesis by
A1;
end;
A5: (v64
"\/" v65)
= (v65
"\/" (v64
"\/"
c("\/")))
proof
(v65
"\/"
c("\/"))
= v65 by
A4;
hence thesis by
ROBBINS3:def 1;
end;
A6: (v64
"\/" v65)
= (v65
"\/" (v64
"\/"
c(c)))
proof
(v65
"\/"
c(c))
= 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(c)
"\/" v65)
proof
(
c(c)
"\/" v65)
= v65 by
A8;
hence thesis by
A3;
end;
A12: (
c(c)
"\/"
c("\/"))
= (
c(c)
"\/" v65)
proof
(((v65
` )
` )
` )
= (v65
` ) by
A10;
hence thesis by
A11;
end;
A13: (
c(c)
"\/"
c("\/"))
= (
c(c)
"\/" v65)
proof
(((v65
` )
` )
` )
= (v65
` ) by
A10;
hence thesis by
A12;
end;
A14: (
c(c)
"\/"
c("\/"))
= (
c(c)
"\/" v65)
proof
(((v65
` )
` )
` )
= (v65
` ) by
A10;
hence thesis by
A13;
end;
A15: (
c(c)
"\/"
c("\/"))
= (
c(c)
"\/" v65)
proof
(((v65
` )
` )
` )
= (v65
` ) by
A10;
hence thesis by
A14;
end;
A16: (
c(c)
"\/"
c("\/"))
= v65
proof
(((v65
` )
` )
"\/" v65)
= v65 by
A2;
hence thesis by
A15;
end;
A17: (
c(c)
"\/"
c("\/"))
= ((v0
` )
` )
proof
(((v0
` )
` )
` )
= (v0
` ) by
A10;
hence thesis by
A4;
end;
A18: ((v0
` )
` )
= v0
proof
(
c(c)
"\/"
c("\/"))
= ((v0
` )
` ) by
A17;
hence thesis by
A16;
end;
A19: (v64
"\/"
c("\/"))
= (v64
"\/" (v1
"\/"
c(c)))
proof
(v64
"\/" (v1
"\/"
c(c)))
= (v1
"\/" v64) by
A6;
hence thesis by
A3;
end;
A20: (v64
"\/"
c("\/"))
= (v1
"\/" v64)
proof
(v64
"\/" (v1
"\/" ((v64
` )
` )))
= (v1
"\/" v64) by
A6;
hence thesis by
A19;
end;
A21: (v0
"\/"
c("\/"))
= (v1
"\/" v0)
proof
((v0
` )
` )
= v0 by
A18;
hence thesis by
A20;
end;
A22: (v64
"\/" (v1
"\/"
c(v64)))
= (
c(v64)
"\/" v64)
proof
(
c(v64)
"\/"
c("\/"))
= (v1
"\/"
c(v64)) by
A21;
hence thesis by
A5;
end;
A23: (
c(v0)
"\/"
c("\/"))
= (v0
` )
proof
((v0
` )
` )
= v0 by
A18;
hence thesis by
A4;
end;
A24: ((v0
"\/" v1)
"\/"
c(v0))
= (
c("\/")
"\/" (v0
"\/" v1))
proof
((v0
` )
"\/"
c("\/"))
=
c(v0) by
A23;
hence thesis by
A22;
end;
A25: (v0
"\/" (v1
"\/"
c(v0)))
= (
c("\/")
"\/" (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("\/"))))
= (
c("\/")
"\/" (v0
"\/" v1))
proof
((v0
"\/" v1)
"\/" (v65
"\/"
c("\/")))
= (v0
"\/" (v1
"\/" (v65
"\/"
c("\/")))) by
ROBBINS3:def 1;
hence thesis by
A22;
end;
A27: (v0
"\/" (v1
"\/" (v65
"\/"
c("\/"))))
= (v0
"\/" (v1
"\/"
c(v0)))
proof
(
c("\/")
"\/" (v0
"\/" v1))
= (v0
"\/" (v1
"\/"
c(v0))) by
A25;
hence thesis by
A26;
end;
A28: (
c("\/")
"\/" (v0
"\/" v1))
= (v0
"\/" (v1
"\/" (v65
"\/"
c("\/"))))
proof
((v0
"\/" v1)
"\/" (v65
"\/"
c("\/")))
= (v0
"\/" (v1
"\/" (v65
"\/"
c("\/")))) by
ROBBINS3:def 1;
hence thesis by
A22;
end;
A29: (
c("\/")
"\/" (v0
"\/" v1))
= (v0
"\/" (v1
"\/"
c(v0)))
proof
now
let v65, v1, v0;
(v0
"\/" (v1
"\/" (v65
"\/"
c("\/"))))
= (v0
"\/" (v1
"\/"
c(v0))) by
A27;
hence (
c("\/")
"\/" (v0
"\/" v1))
= (v0
"\/" (v1
"\/"
c(v0))) by
A28;
end;
hence thesis;
end;
A30: (v2
"\/" (v1
"\/"
c(v2)))
= ((v1
"\/" v2)
"\/" (v65
"\/"
c("\/")))
proof
(
c("\/")
"\/" (v2
"\/" v1))
= (v2
"\/" (v1
"\/"
c(v2))) by
A29;
hence thesis by
A22;
end;
A31: (v2
"\/" (v1
"\/" (v2
` )))
= (v1
"\/" (v2
"\/" (v65
"\/"
c("\/"))))
proof
((v1
"\/" v2)
"\/" (v65
"\/"
c("\/")))
= (v1
"\/" (v2
"\/" (v65
"\/"
c("\/")))) 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
"\/"
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 ::
ROBBINS4:39
for L be 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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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;