:: Formalization of Ortholattices via Orthoposets
:: by Adam Grabowski and Markus Moschner
::
:: Received December 28, 2004
:: Copyright (c) 2004-2021 Association of Mizar Users

:: Originally proved by McCune with the help of OTTER

definition

let L be non empty \/-SemiLattStr ;

attr L is join-Associative means :: ROBBINS3:def 1
for x, y, z being Element of L holds x "\/" (y "\/" z) = y "\/" (x "\/" z);

end;

:: deftheorem defines join-Associative ROBBINS3:def 1 :
for L being non empty \/-SemiLattStr holds
( L is join-Associative iff for x, y, z being Element of L holds x "\/" (y "\/" z) = y "\/" (x "\/" z) );

definition

let L be non empty /\-SemiLattStr ;

attr L is meet-Associative means :: ROBBINS3:def 2
for x, y, z being Element of L holds x "/\" (y "/\" z) = y "/\" (x "/\" z);

end;

:: deftheorem defines meet-Associative ROBBINS3:def 2 :
for L being non empty /\-SemiLattStr holds
( L is meet-Associative iff for x, y, z being Element of L holds x "/\" (y "/\" z) = y "/\" (x "/\" z) );

definition

let L be non empty LattStr ;

attr L is meet-Absorbing means :: ROBBINS3:def 3
for x, y being Element of L holds x "\/" (x "/\" y) = x;

end;

:: deftheorem defines meet-Absorbing ROBBINS3:def 3 :
for L being non empty LattStr holds
( L is meet-Absorbing iff for x, y being Element of L holds x "\/" (x "/\" y) = x );

theorem Th1: :: ROBBINS3:1

for L being non empty LattStr st L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing holds
( L is meet-idempotent & L is join-idempotent )

proof end;

theorem Th2: :: ROBBINS3:2

for L being non empty LattStr st L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing holds
( L is meet-commutative & L is join-commutative )

proof end;

theorem Th3: :: ROBBINS3:3

for L being non empty LattStr st L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing holds
L is meet-absorbing

proof end;

theorem Th4: :: ROBBINS3:4

for L being non empty LattStr st L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing holds
( L is meet-associative & L is join-associative )

proof end;

theorem Th5: :: ROBBINS3:5

for L being non empty LattStr holds
( L is Lattice-like iff ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) )

proof end;

registration

cluster non empty Lattice-like -> non empty join-Associative meet-Associative meet-Absorbing for LattStr ;

coherence
for b₁ being non empty LattStr st b₁ is Lattice-like holds
( b₁ is meet-Associative & b₁ is join-Associative & b₁ is meet-Absorbing ) by Th5;

cluster non empty join-absorbing join-Associative meet-Associative meet-Absorbing -> non empty Lattice-like for LattStr ;

coherence
for b₁ being non empty LattStr st b₁ is meet-Associative & b₁ is join-Associative & b₁ is meet-Absorbing & b₁ is join-absorbing holds
b₁ is Lattice-like by Th5;

end;

registration

cluster non empty PartialOrdered OrderInvolutive -> non empty Dneg PartialOrdered for OrthoRelStr ;

coherence
for b₁ being non empty PartialOrdered OrthoRelStr st b₁ is OrderInvolutive holds
b₁ is Dneg

proof end;

end;

theorem Th6: :: ROBBINS3:6

for L being non empty Dneg OrthoRelStr
for x being Element of L holds (x `) ` = x

proof end;

theorem Th7: :: ROBBINS3:7

for O being non empty PartialOrdered OrderInvolutive OrthoRelStr
for x, y being Element of O st x <= y holds
y ` <= x `

proof end;

registration

cluster non empty reflexive transitive antisymmetric with_suprema with_infima strict Dneg PartialOrdered Pure OrderInvolutive for OrthoRelStr ;

existence
ex b₁ being PreOrthoPoset st
( b₁ is with_infima & b₁ is with_suprema & b₁ is strict )

proof end;

end;

notation

let L be non empty \/-SemiLattStr ;
let x, y be Element of L;
synonym x |_| y for x "\/" y;

end;

notation

let L be non empty /\-SemiLattStr ;
let x, y be Element of L;
synonym x |^| y for x "/\" y;

end;

notation

let L be non empty RelStr ;
let x, y be Element of L;
synonym x "|^|" y for x "/\" y;
synonym x "|_|" y for x "\/" y;

end;

definition

attr c₁ is strict ;
struct \/-SemiLattRelStr -> \/-SemiLattStr , RelStr ;
aggr \/-SemiLattRelStr(# carrier, L_join, InternalRel #) -> \/-SemiLattRelStr ;

end;

definition

attr c₁ is strict ;
struct /\-SemiLattRelStr -> /\-SemiLattStr , RelStr ;
aggr /\-SemiLattRelStr(# carrier, L_meet, InternalRel #) -> /\-SemiLattRelStr ;

end;

definition

attr c₁ is strict ;
struct LattRelStr -> /\-SemiLattRelStr , \/-SemiLattRelStr , LattStr ;
aggr LattRelStr(# carrier, L_join, L_meet, InternalRel #) -> LattRelStr ;

end;

definition

func TrivLattRelStr -> LattRelStr equals :: ROBBINS3:def 4
LattRelStr(# {0},op2,op2,(id {0}) #);

coherence
LattRelStr(# {0},op2,op2,(id {0}) #) is LattRelStr ;

end;

:: deftheorem defines TrivLattRelStr ROBBINS3:def 4 :
TrivLattRelStr = LattRelStr(# {0},op2,op2,(id {0}) #);

registration

cluster TrivLattRelStr -> 1 -element ;

coherence
TrivLattRelStr is 1 -element ;

end;

registration

cluster non empty for \/-SemiLattRelStr ;

existence
not for b₁ being \/-SemiLattRelStr holds b₁ is empty

proof end;

cluster non empty for /\-SemiLattRelStr ;

existence
not for b₁ being /\-SemiLattRelStr holds b₁ is empty

proof end;

cluster non empty for LattRelStr ;

existence
not for b₁ being LattRelStr holds b₁ is empty

proof end;

end;

theorem :: ROBBINS3:8

for R being non empty RelStr st the InternalRel of R is_reflexive_in the carrier of R & the InternalRel of R is antisymmetric & the InternalRel of R is transitive holds
( R is reflexive & R is antisymmetric & R is transitive )

proof end;

registration

cluster TrivLattRelStr -> reflexive ;

coherence
TrivLattRelStr is reflexive

proof end;

end;

registration

cluster reflexive transitive antisymmetric with_suprema with_infima for LattRelStr ;

existence
ex b₁ being LattRelStr st
( b₁ is antisymmetric & b₁ is reflexive & b₁ is transitive & b₁ is with_suprema & b₁ is with_infima )

proof end;

end;

registration

cluster TrivLattRelStr -> meet-Absorbing ;

coherence
TrivLattRelStr is meet-Absorbing ;

end;

Lm1: TrivLattRelStr is Lattice-like
;

registration

cluster non empty Lattice-like for LattRelStr ;

existence
ex b₁ being non empty LattRelStr st b₁ is Lattice-like by Lm1;

end;

definition

let L be Lattice;
:: original: LattRel
redefine func LattRel L -> Order of the carrier of L;
coherence
LattRel L is Order of the carrier of L

proof end;

end;

definition

attr c₁ is strict ;
struct OrthoLattRelStr -> LattRelStr , OrthoLattStr , OrthoRelStr ;
aggr OrthoLattRelStr(# carrier, L_join, L_meet, InternalRel, Compl #) -> OrthoLattRelStr ;

end;

definition

func TrivCLRelStr -> OrthoLattRelStr equals :: ROBBINS3:def 5
OrthoLattRelStr(# {0},op2,op2,(id {0}),op1 #);

coherence
OrthoLattRelStr(# {0},op2,op2,(id {0}),op1 #) is OrthoLattRelStr ;

end;

:: deftheorem defines TrivCLRelStr ROBBINS3:def 5 :
TrivCLRelStr = OrthoLattRelStr(# {0},op2,op2,(id {0}),op1 #);

:: Axiomatics for ortholattices is the classical one for lattices extended
:: by the three following:
:: x ^ y = c(c(x) v c(y)). % DM de_Morgan from ROBBINS1
:: c(c(x)) = x. % CC involutive from OPOSET_1, too specific
:: x v c(x) = y v c(y). % ONE

definition

let L be non empty ComplStr ;

attr L is involutive means :Def6: :: ROBBINS3:def 6
for x being Element of L holds (x `) ` = x;

end;

:: deftheorem Def6 defines involutive ROBBINS3:def 6 :
for L being non empty ComplStr holds
( L is involutive iff for x being Element of L holds (x `) ` = x );

definition

let L be non empty ComplLLattStr ;

attr L is with_Top means :Def7: :: ROBBINS3:def 7
for x, y being Element of L holds x |_| (x `) = y |_| (y `);

end;

:: deftheorem Def7 defines with_Top ROBBINS3:def 7 :
for L being non empty ComplLLattStr holds
( L is with_Top iff for x, y being Element of L holds x |_| (x `) = y |_| (y `) );

registration

cluster TrivOrtLat -> involutive with_Top ;

coherence
( TrivOrtLat is involutive & TrivOrtLat is with_Top ) by STRUCT_0:def 10;

end;

registration

cluster TrivCLRelStr -> 1 -element ;

coherence
TrivCLRelStr is 1 -element ;

end;

registration

cluster TrivCLRelStr -> reflexive ;

coherence
TrivCLRelStr is reflexive

proof end;

end;

registration

cluster TrivCLRelStr -> involutive with_Top ;

coherence
( TrivCLRelStr is involutive & TrivCLRelStr is with_Top ) by STRUCT_0:def 10;

end;

registration

cluster non empty trivial V52() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V161() complemented Boolean de_Morgan upper-bounded' lower-bounded' distributive' complemented' join-Associative meet-Associative meet-Absorbing involutive with_Top for OrthoLattStr ;

existence
ex b₁ being 1 -element OrthoLattStr st
( b₁ is involutive & b₁ is with_Top & b₁ is de_Morgan & b₁ is Lattice-like )

proof end;

end;

definition

mode Ortholattice is non empty Lattice-like de_Morgan involutive with_Top OrthoLattStr ;

end;

theorem Th9: :: ROBBINS3:9

for K, L being non empty LattStr st LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is join-commutative holds
L is join-commutative

proof end;

theorem Th10: :: ROBBINS3:10

for K, L being non empty LattStr st LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is meet-commutative holds
L is meet-commutative

proof end;

theorem Th11: :: ROBBINS3:11

for K, L being non empty LattStr st LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is join-associative holds
L is join-associative

proof end;

theorem Th12: :: ROBBINS3:12

for K, L being non empty LattStr st LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is meet-associative holds
L is meet-associative

proof end;

theorem Th13: :: ROBBINS3:13

for K, L being non empty LattStr st LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is join-absorbing holds
L is join-absorbing

proof end;

theorem Th14: :: ROBBINS3:14

for K, L being non empty LattStr st LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is meet-absorbing holds
L is meet-absorbing

proof end;

theorem :: ROBBINS3:15

for K, L being non empty LattStr st LattStr(# the carrier of K, the L_join of K, the L_meet of K #) = LattStr(# the carrier of L, the L_join of L, the L_meet of L #) & K is Lattice-like holds
L is Lattice-like by Th9, Th10, Th11, Th12, Th13, Th14;

theorem :: ROBBINS3:16

for L1, L2 being non empty \/-SemiLattStr st \/-SemiLattStr(# the carrier of L1, the L_join of L1 #) = \/-SemiLattStr(# the carrier of L2, the L_join of L2 #) holds
for a1, b1 being Element of L1
for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 holds
a1 "\/" b1 = a2 "\/" b2 ;

theorem :: ROBBINS3:17

for L1, L2 being non empty /\-SemiLattStr st /\-SemiLattStr(# the carrier of L1, the L_meet of L1 #) = /\-SemiLattStr(# the carrier of L2, the L_meet of L2 #) holds
for a1, b1 being Element of L1
for a2, b2 being Element of L2 st a1 = a2 & b1 = b2 holds
a1 "/\" b1 = a2 "/\" b2 ;

theorem Th18: :: ROBBINS3:18

for K, L being non empty ComplStr
for x being Element of K
for y being Element of L st the Compl of K = the Compl of L & x = y holds
x ` = y `

proof end;

theorem Th19: :: ROBBINS3:19

for K, L being non empty ComplLLattStr st ComplLLattStr(# the carrier of K, the L_join of K, the Compl of K #) = ComplLLattStr(# the carrier of L, the L_join of L, the Compl of L #) & K is with_Top holds
L is with_Top

proof end;

theorem Th20: :: ROBBINS3:20

for K, L being non empty OrthoLattStr st OrthoLattStr(# the carrier of K, the L_join of K, the L_meet of K, the Compl of K #) = OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) & K is de_Morgan holds
L is de_Morgan

proof end;

theorem Th21: :: ROBBINS3:21

for K, L being non empty OrthoLattStr st OrthoLattStr(# the carrier of K, the L_join of K, the L_meet of K, the Compl of K #) = OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) & K is involutive holds
L is involutive

proof end;

definition

let R be RelStr ;

mode RelAugmentation of R -> LattRelStr means :: ROBBINS3:def 8
RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of R, the InternalRel of R #);

existence
ex b₁ being LattRelStr st RelStr(# the carrier of b₁, the InternalRel of b₁ #) = RelStr(# the carrier of R, the InternalRel of R #)

proof end;

end;

:: deftheorem defines RelAugmentation ROBBINS3:def 8 :
for R being RelStr
for b₂ being LattRelStr holds
( b₂ is RelAugmentation of R iff RelStr(# the carrier of b₂, the InternalRel of b₂ #) = RelStr(# the carrier of R, the InternalRel of R #) );

definition

let R be LattStr ;

mode LatAugmentation of R -> LattRelStr means :Def9: :: ROBBINS3:def 9
LattStr(# the carrier of it, the L_join of it, the L_meet of it #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #);

existence
ex b₁ being LattRelStr st LattStr(# the carrier of b₁, the L_join of b₁, the L_meet of b₁ #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #)

proof end;

end;

:: deftheorem Def9 defines LatAugmentation ROBBINS3:def 9 :
for R being LattStr
for b₂ being LattRelStr holds
( b₂ is LatAugmentation of R iff LattStr(# the carrier of b₂, the L_join of b₂, the L_meet of b₂ #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) );

registration

let L be non empty LattStr ;

cluster -> non empty for LatAugmentation of L;

coherence
for b₁ being LatAugmentation of L holds not b₁ is empty

proof end;

end;

registration

let L be non empty meet-associative LattStr ;

cluster -> meet-associative for LatAugmentation of L;

coherence
for b₁ being LatAugmentation of L holds b₁ is meet-associative

proof end;

end;

registration

let L be non empty join-associative LattStr ;

cluster -> join-associative for LatAugmentation of L;

coherence
for b₁ being LatAugmentation of L holds b₁ is join-associative

proof end;

end;

registration

let L be non empty meet-commutative LattStr ;

cluster -> meet-commutative for LatAugmentation of L;

coherence
for b₁ being LatAugmentation of L holds b₁ is meet-commutative

proof end;

end;

registration

let L be non empty join-commutative LattStr ;

cluster -> join-commutative for LatAugmentation of L;

coherence
for b₁ being LatAugmentation of L holds b₁ is join-commutative

proof end;

end;

registration

let L be non empty join-absorbing LattStr ;

cluster -> join-absorbing for LatAugmentation of L;

coherence
for b₁ being LatAugmentation of L holds b₁ is join-absorbing

proof end;

end;

registration

let L be non empty meet-absorbing LattStr ;

cluster -> meet-absorbing for LatAugmentation of L;

coherence
for b₁ being LatAugmentation of L holds b₁ is meet-absorbing

proof end;

end;

definition

let L be non empty \/-SemiLattRelStr ;

attr L is naturally_sup-generated means :Def10: :: ROBBINS3:def 10
for x, y being Element of L holds
( x <= y iff x |_| y = y );

end;

:: deftheorem Def10 defines naturally_sup-generated ROBBINS3:def 10 :
for L being non empty \/-SemiLattRelStr holds
( L is naturally_sup-generated iff for x, y being Element of L holds
( x <= y iff x |_| y = y ) );

definition

let L be non empty /\-SemiLattRelStr ;

attr L is naturally_inf-generated means :: ROBBINS3:def 11
for x, y being Element of L holds
( x <= y iff x |^| y = x );

end;

:: deftheorem defines naturally_inf-generated ROBBINS3:def 11 :
for L being non empty /\-SemiLattRelStr holds
( L is naturally_inf-generated iff for x, y being Element of L holds
( x <= y iff x |^| y = x ) );

registration

let L be Lattice;

cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like join-Associative meet-Associative meet-Absorbing naturally_sup-generated naturally_inf-generated for LatAugmentation of L;

existence
ex b₁ being LatAugmentation of L st
( b₁ is naturally_sup-generated & b₁ is naturally_inf-generated & b₁ is Lattice-like )

proof end;

end;

registration

cluster 1 -element reflexive for LattRelStr ;

existence
ex b₁ being LattRelStr st
( b₁ is 1 -element & b₁ is reflexive )

proof end;

end;

registration

cluster 1 -element reflexive for OrthoLattRelStr ;

existence
ex b₁ being OrthoLattRelStr st
( b₁ is 1 -element & b₁ is reflexive )

proof end;

end;

registration

cluster 1 -element reflexive for OrthoRelStr ;

existence
ex b₁ being OrthoRelStr st
( b₁ is 1 -element & b₁ is reflexive )

proof end;

end;

registration

cluster 1 -element -> 1 -element well-complemented de_Morgan involutive with_Top for OrthoLattStr ;

coherence
for b₁ being 1 -element OrthoLattStr holds
( b₁ is involutive & b₁ is with_Top & b₁ is de_Morgan & b₁ is well-complemented )

proof end;

end;

registration

cluster 1 -element reflexive -> 1 -element reflexive PartialOrdered Pure OrderInvolutive for OrthoRelStr ;

coherence
for b₁ being 1 -element reflexive OrthoRelStr holds
( b₁ is OrderInvolutive & b₁ is Pure & b₁ is PartialOrdered )

proof end;

end;

registration

cluster 1 -element reflexive -> 1 -element reflexive naturally_sup-generated naturally_inf-generated for LattRelStr ;

coherence
for b₁ being 1 -element reflexive LattRelStr holds
( b₁ is naturally_sup-generated & b₁ is naturally_inf-generated )

proof end;

end;

registration

cluster non empty Lattice-like with_suprema with_infima de_Morgan PartialOrdered Pure OrderInvolutive naturally_sup-generated naturally_inf-generated for OrthoLattRelStr ;

existence
ex b₁ being non empty OrthoLattRelStr st
( b₁ is with_infima & b₁ is with_suprema & b₁ is naturally_sup-generated & b₁ is naturally_inf-generated & b₁ is de_Morgan & b₁ is Lattice-like & b₁ is OrderInvolutive & b₁ is Pure & b₁ is PartialOrdered )

proof end;

end;

registration

cluster non empty Lattice-like with_suprema with_infima naturally_sup-generated naturally_inf-generated for LattRelStr ;

existence
ex b₁ being non empty LattRelStr st
( b₁ is with_infima & b₁ is with_suprema & b₁ is naturally_sup-generated & b₁ is naturally_inf-generated & b₁ is Lattice-like )

proof end;

end;

theorem Th22: :: ROBBINS3:22

for L being non empty naturally_sup-generated LattRelStr
for x, y being Element of L holds
( x <= y iff x [= y ) by Def10;

theorem Th23: :: ROBBINS3:23

for L being non empty Lattice-like naturally_sup-generated LattRelStr holds RelStr(# the carrier of L, the InternalRel of L #) = LattPOSet L

proof end;

registration

cluster non empty Lattice-like naturally_sup-generated -> non empty with_suprema with_infima for LattRelStr ;

coherence
for b₁ being non empty LattRelStr st b₁ is naturally_sup-generated & b₁ is Lattice-like holds
( b₁ is with_infima & b₁ is with_suprema )

proof end;

end;

definition

let R be OrthoLattStr ;

mode CLatAugmentation of R -> OrthoLattRelStr means :Def12: :: ROBBINS3:def 12
OrthoLattStr(# the carrier of it, the L_join of it, the L_meet of it, the Compl of it #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #);

existence
ex b₁ being OrthoLattRelStr st OrthoLattStr(# the carrier of b₁, the L_join of b₁, the L_meet of b₁, the Compl of b₁ #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #)

proof end;

end;

:: deftheorem Def12 defines CLatAugmentation ROBBINS3:def 12 :
for R being OrthoLattStr
for b₂ being OrthoLattRelStr holds
( b₂ is CLatAugmentation of R iff OrthoLattStr(# the carrier of b₂, the L_join of b₂, the L_meet of b₂, the Compl of b₂ #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) );

registration

let L be non empty OrthoLattStr ;

cluster -> non empty for CLatAugmentation of L;

coherence
for b₁ being CLatAugmentation of L holds not b₁ is empty

proof end;

end;

registration

let L be non empty meet-associative OrthoLattStr ;

cluster -> meet-associative for CLatAugmentation of L;

coherence
for b₁ being CLatAugmentation of L holds b₁ is meet-associative

proof end;

end;

registration

let L be non empty join-associative OrthoLattStr ;

cluster -> join-associative for CLatAugmentation of L;

coherence
for b₁ being CLatAugmentation of L holds b₁ is join-associative

proof end;

end;

registration

let L be non empty meet-commutative OrthoLattStr ;

cluster -> meet-commutative for CLatAugmentation of L;

coherence
for b₁ being CLatAugmentation of L holds b₁ is meet-commutative

proof end;

end;

registration

let L be non empty join-commutative OrthoLattStr ;

cluster -> join-commutative for CLatAugmentation of L;

coherence
for b₁ being CLatAugmentation of L holds b₁ is join-commutative

proof end;

end;

registration

let L be non empty meet-absorbing OrthoLattStr ;

cluster -> meet-absorbing for CLatAugmentation of L;

coherence
for b₁ being CLatAugmentation of L holds b₁ is meet-absorbing

proof end;

end;

registration

let L be non empty join-absorbing OrthoLattStr ;

cluster -> join-absorbing for CLatAugmentation of L;

coherence
for b₁ being CLatAugmentation of L holds b₁ is join-absorbing

proof end;

end;

registration

let L be non empty with_Top OrthoLattStr ;

cluster -> with_Top for CLatAugmentation of L;

coherence
for b₁ being CLatAugmentation of L holds b₁ is with_Top

proof end;

end;

registration

let L be Ortholattice;

cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like join-Associative meet-Associative meet-Absorbing with_Top naturally_sup-generated naturally_inf-generated for CLatAugmentation of L;

existence
ex b₁ being CLatAugmentation of L st
( b₁ is naturally_sup-generated & b₁ is naturally_inf-generated & b₁ is Lattice-like )

proof end;

end;

registration

cluster non empty Lattice-like well-complemented de_Morgan involutive with_Top naturally_sup-generated for OrthoLattRelStr ;

existence
ex b₁ being non empty OrthoLattRelStr st
( b₁ is involutive & b₁ is with_Top & b₁ is de_Morgan & b₁ is Lattice-like & b₁ is naturally_sup-generated & b₁ is well-complemented )

proof end;

end;

theorem Th24: :: ROBBINS3:24

for L being non empty with_suprema with_infima PartialOrdered OrthoRelStr
for x, y being Element of L st x <= y holds
( y = x "|_|" y & x = x "|^|" y )

proof end;

definition

let L be non empty meet-commutative /\-SemiLattStr ;
let a, b be Element of L;
:: original: |^|
redefine func a |^| b -> M3( the carrier of L);
commutativity
for a, b being Element of L holds a |^| b = b |^| a by LATTICES:def 6;

end;

definition

let L be non empty join-commutative \/-SemiLattStr ;
let a, b be Element of L;
:: original: |_|
redefine func a |_| b -> M3( the carrier of L);
commutativity
for a, b being Element of L holds a |_| b = b |_| a by LATTICES:def 4;

end;

registration

cluster non empty meet-commutative meet-absorbing join-absorbing naturally_sup-generated -> non empty reflexive for LattRelStr ;

coherence
for b₁ being non empty LattRelStr st b₁ is meet-absorbing & b₁ is join-absorbing & b₁ is meet-commutative & b₁ is naturally_sup-generated holds
b₁ is reflexive

proof end;

end;

registration

cluster non empty join-associative naturally_sup-generated -> non empty transitive for LattRelStr ;

coherence
for b₁ being non empty LattRelStr st b₁ is join-associative & b₁ is naturally_sup-generated holds
b₁ is transitive

proof end;

end;

registration

cluster non empty join-commutative naturally_sup-generated -> non empty antisymmetric for LattRelStr ;

coherence
for b₁ being non empty LattRelStr st b₁ is join-commutative & b₁ is naturally_sup-generated holds
b₁ is antisymmetric

proof end;

end;

theorem Th25: :: ROBBINS3:25

for L being non empty Lattice-like with_suprema with_infima naturally_sup-generated OrthoLattRelStr
for x, y being Element of L holds x "|_|" y = x |_| y

proof end;

theorem Th26: :: ROBBINS3:26

for L being non empty Lattice-like with_suprema with_infima naturally_sup-generated OrthoLattRelStr
for x, y being Element of L holds x "|^|" y = x |^| y

proof end;

theorem :: ROBBINS3:27

for L being non empty Lattice-like with_suprema with_infima PartialOrdered OrderInvolutive naturally_sup-generated naturally_inf-generated OrthoLattRelStr holds L is de_Morgan

proof end;

registration

let L be Ortholattice;

cluster -> involutive for CLatAugmentation of L;

coherence
for b₁ being CLatAugmentation of L holds b₁ is involutive

proof end;

end;

registration

let L be Ortholattice;

cluster -> de_Morgan for CLatAugmentation of L;

coherence
for b₁ being CLatAugmentation of L holds b₁ is de_Morgan

proof end;

end;

theorem Th28: :: ROBBINS3:28

for L being non empty OrthoLattRelStr st L is involutive & L is with_Top & L is de_Morgan & L is Lattice-like & L is naturally_sup-generated holds
( L is Orthocomplemented & L is PartialOrdered )

proof end;

theorem :: ROBBINS3:29

for L being Ortholattice
for E being naturally_sup-generated CLatAugmentation of L holds E is Orthocomplemented by Th28;

registration

let L be Ortholattice;

cluster naturally_sup-generated -> Orthocomplemented naturally_sup-generated for CLatAugmentation of L;

coherence
for b₁ being naturally_sup-generated CLatAugmentation of L holds b₁ is Orthocomplemented by Th28;

end;

theorem Th30: :: ROBBINS3:30

for L being non empty OrthoLattStr st L is Boolean & L is well-complemented & L is Lattice-like holds
L is Ortholattice

proof end;

registration

cluster non empty Lattice-like Boolean well-complemented -> non empty de_Morgan involutive with_Top for OrthoLattStr ;

coherence
for b₁ being non empty OrthoLattStr st b₁ is Boolean & b₁ is well-complemented & b₁ is Lattice-like holds
( b₁ is involutive & b₁ is with_Top & b₁ is de_Morgan ) by Th30;

end;