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


begin

definition
let L be non empty \/-SemiLattStr ;
attr L is join-Associative means :Def1: :: ROBBINS3:def 1
 for x, y, z being Element of L holds x "\/" (y "\/" z) = y "\/" (x "\/" z);
end;

:: deftheorem Def1 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 :Def2: :: ROBBINS3:def 2
 for x, y, z being Element of L holds x "/\" (y "/\" z) = y "/\" (x "/\" z);
end;

:: deftheorem Def2 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 :Def3: :: ROBBINS3:def 3
 for x, y being Element of L holds x "\/" (x "/\" y) = x;
end;

:: deftheorem Def3 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 LattStr ;
coherence
for b1 being non empty LattStr st b1 is Lattice-like holds
( b1 is meet-Associative & b1 is join-Associative & b1 is meet-Absorbing ) by Th5;
cluster non empty join-absorbing join-Associative meet-Associative meet-Absorbing -> non empty Lattice-like LattStr ;
coherence
for b1 being non empty LattStr st b1 is meet-Associative & b1 is join-Associative & b1 is meet-Absorbing & b1 is join-absorbing holds
b1 is Lattice-like by Th5;
end;

begin

registration
cluster non empty PartialOrdered OrderInvolutive -> non empty Dneg PartialOrdered OrthoRelStr ;
coherence
for b1 being non empty PartialOrdered OrthoRelStr st b1 is OrderInvolutive holds
b1 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 OrthoRelStr ;
existence
ex b1 being PreOrthoPoset st
( b1 is with_infima & b1 is with_suprema & b1 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;

begin

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

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

definition
attr c1 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(# 1,op2,op2,(id 1) #);
coherence
LattRelStr(# 1,op2,op2,(id 1) #) is LattRelStr ;
end;

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

registration
cluster TrivLattRelStr -> non empty trivial ;
coherence
( not TrivLattRelStr is empty & TrivLattRelStr is trivial ) by CARD_1:87;
end;

registration
cluster non empty \/-SemiLattRelStr ;
existence
not for b1 being \/-SemiLattRelStr holds b1 is empty
proof end;
cluster non empty /\-SemiLattRelStr ;
existence
not for b1 being /\-SemiLattRelStr holds b1 is empty
proof end;
cluster non empty LattRelStr ;
existence
not for b1 being LattRelStr holds b1 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 LattRelStr ;
existence
ex b1 being LattRelStr st
( b1 is antisymmetric & b1 is reflexive & b1 is transitive & b1 is with_suprema & b1 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 LattRelStr ;
existence
ex b1 being non empty LattRelStr st b1 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;

begin

definition
attr c1 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(# 1,op2,op2,(id 1),op1 #);
coherence
OrthoLattRelStr(# 1,op2,op2,(id 1),op1 #) is OrthoLattRelStr ;
end;

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

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 )
proof end;
end;

registration
cluster TrivCLRelStr -> non empty trivial ;
coherence
( not TrivCLRelStr is empty & TrivCLRelStr is trivial ) by CARD_1:87;
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 )
proof end;
end;

registration
cluster non empty Lattice-like de_Morgan involutive with_Top OrthoLattStr ;
existence
ex b1 being non empty OrthoLattStr st
( b1 is involutive & b1 is with_Top & b1 is de_Morgan & b1 is Lattice-like )
proof end;
end;

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

begin

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
proof end;

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;

begin

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 b1 being LattRelStr st RelStr(# the carrier of b1, the InternalRel of b1 #) = RelStr(# the carrier of R, the InternalRel of R #)
proof end;
end;

:: deftheorem defines RelAugmentation ROBBINS3:def 8 :
for R being RelStr
for b2 being LattRelStr holds
( b2 is RelAugmentation of R iff RelStr(# the carrier of b2, the InternalRel of b2 #) = 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 b1 being LattRelStr st LattStr(# the carrier of b1, the L_join of b1, the L_meet of b1 #) = 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 b2 being LattRelStr holds
( b2 is LatAugmentation of R iff LattStr(# the carrier of b2, the L_join of b2, the L_meet of b2 #) = 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 LatAugmentation of L;
coherence
for b1 being LatAugmentation of L holds not b1 is empty
proof end;
end;

registration
let L be non empty meet-associative LattStr ;
cluster -> meet-associative LatAugmentation of L;
coherence
for b1 being LatAugmentation of L holds b1 is meet-associative
proof end;
end;

registration
let L be non empty join-associative LattStr ;
cluster -> join-associative LatAugmentation of L;
coherence
for b1 being LatAugmentation of L holds b1 is join-associative
proof end;
end;

registration
let L be non empty meet-commutative LattStr ;
cluster -> meet-commutative LatAugmentation of L;
coherence
for b1 being LatAugmentation of L holds b1 is meet-commutative
proof end;
end;

registration
let L be non empty join-commutative LattStr ;
cluster -> join-commutative LatAugmentation of L;
coherence
for b1 being LatAugmentation of L holds b1 is join-commutative
proof end;
end;

registration
let L be non empty join-absorbing LattStr ;
cluster -> join-absorbing LatAugmentation of L;
coherence
for b1 being LatAugmentation of L holds b1 is join-absorbing
proof end;
end;

registration
let L be non empty meet-absorbing LattStr ;
cluster -> meet-absorbing LatAugmentation of L;
coherence
for b1 being LatAugmentation of L holds b1 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 :Def11: :: ROBBINS3:def 11
 for x, y being Element of L holds
( x <= y iff x |^| y = x );
end;

:: deftheorem Def11 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 LatAugmentation of L;
existence
ex b1 being LatAugmentation of L st
( b1 is naturally_sup-generated & b1 is naturally_inf-generated & b1 is Lattice-like )
proof end;
end;

registration
cluster non empty trivial reflexive LattRelStr ;
existence
ex b1 being LattRelStr st
( b1 is trivial & not b1 is empty & b1 is reflexive )
proof end;
end;

registration
cluster non empty trivial reflexive OrthoLattRelStr ;
existence
ex b1 being OrthoLattRelStr st
( b1 is trivial & not b1 is empty & b1 is reflexive )
proof end;
end;

registration
cluster non empty trivial reflexive OrthoRelStr ;
existence
ex b1 being OrthoRelStr st
( b1 is trivial & not b1 is empty & b1 is reflexive )
proof end;
end;

registration
cluster non empty trivial -> non empty well-complemented de_Morgan involutive with_Top OrthoLattStr ;
coherence
for b1 being non empty OrthoLattStr st b1 is trivial holds
( b1 is involutive & b1 is with_Top & b1 is de_Morgan & b1 is well-complemented )
proof end;
end;

registration
cluster non empty trivial reflexive -> non empty reflexive PartialOrdered Pure OrderInvolutive OrthoRelStr ;
coherence
for b1 being non empty reflexive OrthoRelStr st b1 is trivial holds
( b1 is OrderInvolutive & b1 is Pure & b1 is PartialOrdered )
proof end;
end;

registration
cluster non empty trivial reflexive -> non empty reflexive naturally_sup-generated naturally_inf-generated LattRelStr ;
coherence
for b1 being non empty reflexive LattRelStr st b1 is trivial holds
( b1 is naturally_sup-generated & b1 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 OrthoLattRelStr ;
existence
ex b1 being non empty OrthoLattRelStr st
( b1 is with_infima & b1 is with_suprema & b1 is naturally_sup-generated & b1 is naturally_inf-generated & b1 is de_Morgan & b1 is Lattice-like & b1 is OrderInvolutive & b1 is Pure & b1 is PartialOrdered )
proof end;
end;

registration
cluster non empty Lattice-like with_suprema with_infima naturally_sup-generated naturally_inf-generated LattRelStr ;
existence
ex b1 being non empty LattRelStr st
( b1 is with_infima & b1 is with_suprema & b1 is naturally_sup-generated & b1 is naturally_inf-generated & b1 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 )
proof end;

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 LattRelStr ;
coherence
for b1 being non empty LattRelStr st b1 is naturally_sup-generated & b1 is Lattice-like holds
( b1 is with_infima & b1 is with_suprema )
proof end;
end;

begin

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 b1 being OrthoLattRelStr st OrthoLattStr(# the carrier of b1, the L_join of b1, the L_meet of b1, the Compl of b1 #) = 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 b2 being OrthoLattRelStr holds
( b2 is CLatAugmentation of R iff OrthoLattStr(# the carrier of b2, the L_join of b2, the L_meet of b2, the Compl of b2 #) = 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 CLatAugmentation of L;
coherence
for b1 being CLatAugmentation of L holds not b1 is empty
proof end;
end;

registration
let L be non empty meet-associative OrthoLattStr ;
cluster -> meet-associative CLatAugmentation of L;
coherence
for b1 being CLatAugmentation of L holds b1 is meet-associative
proof end;
end;

registration
let L be non empty join-associative OrthoLattStr ;
cluster -> join-associative CLatAugmentation of L;
coherence
for b1 being CLatAugmentation of L holds b1 is join-associative
proof end;
end;

registration
let L be non empty meet-commutative OrthoLattStr ;
cluster -> meet-commutative CLatAugmentation of L;
coherence
for b1 being CLatAugmentation of L holds b1 is meet-commutative
proof end;
end;

registration
let L be non empty join-commutative OrthoLattStr ;
cluster -> join-commutative CLatAugmentation of L;
coherence
for b1 being CLatAugmentation of L holds b1 is join-commutative
proof end;
end;

registration
let L be non empty meet-absorbing OrthoLattStr ;
cluster -> meet-absorbing CLatAugmentation of L;
coherence
for b1 being CLatAugmentation of L holds b1 is meet-absorbing
proof end;
end;

registration
let L be non empty join-absorbing OrthoLattStr ;
cluster -> join-absorbing CLatAugmentation of L;
coherence
for b1 being CLatAugmentation of L holds b1 is join-absorbing
proof end;
end;

registration
let L be non empty with_Top OrthoLattStr ;
cluster -> with_Top CLatAugmentation of L;
coherence
for b1 being CLatAugmentation of L holds b1 is with_Top
proof end;
end;

registration
let L be non empty 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 CLatAugmentation of L;
existence
ex b1 being CLatAugmentation of L st
( b1 is naturally_sup-generated & b1 is naturally_inf-generated & b1 is Lattice-like )
proof end;
end;

registration
cluster non empty Lattice-like well-complemented de_Morgan involutive with_Top naturally_sup-generated OrthoLattRelStr ;
existence
ex b1 being non empty OrthoLattRelStr st
( b1 is involutive & b1 is with_Top & b1 is de_Morgan & b1 is Lattice-like & b1 is naturally_sup-generated & b1 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 -> M2( 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 -> M2( 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 LattRelStr ;
coherence
for b1 being non empty LattRelStr st b1 is meet-absorbing & b1 is join-absorbing & b1 is meet-commutative & b1 is naturally_sup-generated holds
b1 is reflexive
proof end;
end;

registration
cluster non empty join-associative naturally_sup-generated -> non empty transitive LattRelStr ;
coherence
for b1 being non empty LattRelStr st b1 is join-associative & b1 is naturally_sup-generated holds
b1 is transitive
proof end;
end;

registration
cluster non empty join-commutative naturally_sup-generated -> non empty antisymmetric LattRelStr ;
coherence
for b1 being non empty LattRelStr st b1 is join-commutative & b1 is naturally_sup-generated holds
b1 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 CLatAugmentation of L;
coherence
for b1 being CLatAugmentation of L holds b1 is involutive
proof end;
end;

registration
let L be Ortholattice;
cluster -> de_Morgan CLatAugmentation of L;
coherence
for b1 being CLatAugmentation of L holds b1 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 CLatAugmentation of L;
coherence
for b1 being naturally_sup-generated CLatAugmentation of L holds b1 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 OrthoLattStr ;
coherence
for b1 being non empty OrthoLattStr st b1 is Boolean & b1 is well-complemented & b1 is Lattice-like holds
( b1 is involutive & b1 is with_Top & b1 is de_Morgan ) by Th30;
end;