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


begin

:: Originally proved by McCune with the help of OTTER
definition
let L be non empty \/-SemiLattStr ;
attrL 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 ;
attrL 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 ;
attrL 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 )
proofend;

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 )
proofend;

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
proofend;

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 )
proofend;

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 ) )
proofend;

registration
cluster non empty Lattice-like  ->  non empty join-Associative meet-Associative meet-Absorbing for 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 for 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 for OrthoRelStr ;
coherence
 for b1 being non empty PartialOrdered OrthoRelStr st b1 is OrderInvolutive holds
b1 is Dneg
proofend;
end;

theorem Th6: :: ROBBINS3:6
for L being non empty Dneg OrthoRelStr
for x being Element of L holds (x `) ` = x
proofend;

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 `
proofend;

registration
cluster non empty reflexive transitive antisymmetric with_suprema with_infima strict Dneg PartialOrdered Pure OrderInvolutive for OrthoRelStr ;
existence
 ex b1 being PreOrthoPoset st
( b1 is with_infima &amp; b1 is with_suprema &amp; b1 is strict )
proofend;
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
attrc1 is strict ;
struct \/-SemiLattRelStr  ->  \/-SemiLattStr , RelStr ;
aggr\/-SemiLattRelStr(# carrier, L_join, InternalRel #) ->  \/-SemiLattRelStr ;
end;

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

definition
attrc1 is strict ;
struct LattRelStr  ->  /\-SemiLattRelStr , \/-SemiLattRelStr , LattStr ;
aggrLattRelStr(# 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  -> 1 -element ;
coherence
 TrivLattRelStr is 1 -element
proofend;
end;

registration
cluster non empty for \/-SemiLattRelStr ;
existence
 not for b1 being \/-SemiLattRelStr holds b1 is empty
proofend;
cluster non empty for /\-SemiLattRelStr ;
existence
 not for b1 being /\-SemiLattRelStr holds b1 is empty
proofend;
cluster non empty for LattRelStr ;
existence
 not for b1 being LattRelStr holds b1 is empty
proofend;
end;

theorem :: ROBBINS3:8
for R being non empty RelStr st the InternalRel of R is_reflexive_in the carrier of R &amp; the InternalRel of R is antisymmetric &amp; the InternalRel of R is transitive holds
( R is reflexive &amp; R is antisymmetric &amp; R is transitive )
proofend;

registration
cluster TrivLattRelStr  ->  reflexive ;
coherence
 TrivLattRelStr is reflexive
proofend;
end;

registration
cluster reflexive transitive antisymmetric with_suprema with_infima for LattRelStr ;
existence
 ex b1 being LattRelStr st
( b1 is antisymmetric &amp; b1 is reflexive &amp; b1 is transitive &amp; b1 is with_suprema &amp; b1 is with_infima )
proofend;
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 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
proofend;
end;

begin

definition
attrc1 is strict ;
struct OrthoLattRelStr  ->  LattRelStr , OrthoLattStr , OrthoRelStr ;
aggrOrthoLattRelStr(# 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 #);

:: 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 ;
attrL 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 ;
attrL 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 &amp; TrivOrtLat is with_Top )
proofend;
end;

registration
cluster TrivCLRelStr  -> 1 -element ;
coherence
 TrivCLRelStr is 1 -element
proofend;
end;

registration
cluster TrivCLRelStr  ->  reflexive ;
coherence
 TrivCLRelStr is reflexive
proofend;
end;

registration
cluster TrivCLRelStr  ->  involutive with_Top ;
coherence
 ( TrivCLRelStr is involutive &amp; TrivCLRelStr is with_Top )
proofend;
end;

registration
cluster non empty trivial V50() 1 -element join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V147() complemented Boolean de_Morgan upper-bounded' lower-bounded' distributive' complemented' join-Associative meet-Associative meet-Absorbing involutive with_Top for OrthoLattStr ;
existence
 ex b1 being 1 -element OrthoLattStr st
( b1 is involutive &amp; b1 is with_Top &amp; b1 is de_Morgan &amp; b1 is Lattice-like )
proofend;
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 #) &amp; K is join-commutative holds
L is join-commutative
proofend;

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 #) &amp; K is meet-commutative holds
L is meet-commutative
proofend;

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 #) &amp; K is join-associative holds
L is join-associative
proofend;

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 #) &amp; K is meet-associative holds
L is meet-associative
proofend;

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 #) &amp; K is join-absorbing holds
L is join-absorbing
proofend;

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 #) &amp; K is meet-absorbing holds
L is meet-absorbing
proofend;

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 #) &amp; K is Lattice-like holds
L is Lattice-like
proofend;

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 &amp; 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 &amp; 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 &amp; x = y holds
x ` = y `
proofend;

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 #) &amp; K is with_Top holds
L is with_Top
proofend;

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 #) &amp; K is de_Morgan holds
L is de_Morgan
proofend;

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 #) &amp; K is involutive holds
L is involutive
proofend;

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 #)
proofend;
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 #)
proofend;
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 for LatAugmentation of L;
coherence
 for b1 being LatAugmentation of L holds not b1 is empty
proofend;
end;

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

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

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

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

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

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

definition
let L be non empty \/-SemiLattRelStr ;
attrL 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 ;
attrL 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 for LatAugmentation of L;
existence
 ex b1 being LatAugmentation of L st
( b1 is naturally_sup-generated &amp; b1 is naturally_inf-generated &amp; b1 is Lattice-like )
proofend;
end;

registration
cluster1 -element reflexive for LattRelStr ;
existence
 ex b1 being LattRelStr st
( b1 is 1 -element &amp; b1 is reflexive )
proofend;
end;

registration
cluster1 -element reflexive for OrthoLattRelStr ;
existence
 ex b1 being OrthoLattRelStr st
( b1 is 1 -element &amp; b1 is reflexive )
proofend;
end;

registration
cluster1 -element reflexive for OrthoRelStr ;
existence
 ex b1 being OrthoRelStr st
( b1 is 1 -element &amp; b1 is reflexive )
proofend;
end;

registration
cluster1 -element  -> 1 -element well-complemented de_Morgan involutive with_Top for OrthoLattStr ;
coherence
 for b1 being 1 -element OrthoLattStr holds
( b1 is involutive &amp; b1 is with_Top &amp; b1 is de_Morgan &amp; b1 is well-complemented )
proofend;
end;

registration
cluster1 -element reflexive  -> 1 -element reflexive PartialOrdered Pure OrderInvolutive for OrthoRelStr ;
coherence
 for b1 being 1 -element reflexive OrthoRelStr holds
( b1 is OrderInvolutive &amp; b1 is Pure &amp; b1 is PartialOrdered )
proofend;
end;

registration
cluster1 -element reflexive  -> 1 -element reflexive naturally_sup-generated naturally_inf-generated for LattRelStr ;
coherence
 for b1 being 1 -element reflexive LattRelStr holds
( b1 is naturally_sup-generated &amp; b1 is naturally_inf-generated )
proofend;
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 b1 being non empty OrthoLattRelStr st
( b1 is with_infima &amp; b1 is with_suprema &amp; b1 is naturally_sup-generated &amp; b1 is naturally_inf-generated &amp; b1 is de_Morgan &amp; b1 is Lattice-like &amp; b1 is OrderInvolutive &amp; b1 is Pure &amp; b1 is PartialOrdered )
proofend;
end;

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

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
proofend;

registration
cluster non empty Lattice-like naturally_sup-generated  ->  non empty with_suprema with_infima for LattRelStr ;
coherence
 for b1 being non empty LattRelStr st b1 is naturally_sup-generated &amp; b1 is Lattice-like holds
( b1 is with_infima &amp; b1 is with_suprema )
proofend;
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 #)
proofend;
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 for CLatAugmentation of L;
coherence
 for b1 being CLatAugmentation of L holds not b1 is empty
proofend;
end;

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

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

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

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

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

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

registration
let L be non empty with_Top OrthoLattStr ;
cluster  ->  with_Top for CLatAugmentation of L;
coherence
 for b1 being CLatAugmentation of L holds b1 is with_Top
proofend;
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 b1 being CLatAugmentation of L st
( b1 is naturally_sup-generated &amp; b1 is naturally_inf-generated &amp; b1 is Lattice-like )
proofend;
end;

registration
cluster non empty Lattice-like well-complemented de_Morgan involutive with_Top naturally_sup-generated for OrthoLattRelStr ;
existence
 ex b1 being non empty OrthoLattRelStr st
( b1 is involutive &amp; b1 is with_Top &amp; b1 is de_Morgan &amp; b1 is Lattice-like &amp; b1 is naturally_sup-generated &amp; b1 is well-complemented )
proofend;
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 &amp; x = x "|^|" y )
proofend;

definition
let L be non empty meet-commutative /\-SemiLattStr ;
let a, b be Element of L;
:: original:|^|
redefine funca |^| 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 funca |_| 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 for LattRelStr ;
coherence
 for b1 being non empty LattRelStr st b1 is meet-absorbing &amp; b1 is join-absorbing &amp; b1 is meet-commutative &amp; b1 is naturally_sup-generated holds
b1 is reflexive
proofend;
end;

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

registration
cluster non empty join-commutative naturally_sup-generated  ->  non empty antisymmetric for LattRelStr ;
coherence
 for b1 being non empty LattRelStr st b1 is join-commutative &amp; b1 is naturally_sup-generated holds
b1 is antisymmetric
proofend;
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
proofend;

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
proofend;

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
proofend;

registration
let L be Ortholattice;
cluster  ->  involutive for CLatAugmentation of L;
coherence
 for b1 being CLatAugmentation of L holds b1 is involutive
proofend;
end;

registration
let L be Ortholattice;
cluster  ->  de_Morgan for CLatAugmentation of L;
coherence
 for b1 being CLatAugmentation of L holds b1 is de_Morgan
proofend;
end;

theorem Th28: :: ROBBINS3:28
for L being non empty OrthoLattRelStr st L is involutive &amp; L is with_Top &amp; L is de_Morgan &amp; L is Lattice-like &amp; L is naturally_sup-generated holds
( L is Orthocomplemented &amp; L is PartialOrdered )
proofend;

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 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 &amp; L is well-complemented &amp; L is Lattice-like holds
L is Ortholattice
proofend;

registration
cluster non empty Lattice-like Boolean well-complemented  ->  non empty de_Morgan involutive with_Top for OrthoLattStr ;
coherence
 for b1 being non empty OrthoLattStr st b1 is Boolean &amp; b1 is well-complemented &amp; b1 is Lattice-like holds
( b1 is involutive &amp; b1 is with_Top &amp; b1 is de_Morgan ) by Th30;
end;