:: ROBBINS3 semantic presentation

definition
let c1 be non empty \/-SemiLattStr ;
attr a1 is join-Associative means :Def1: :: ROBBINS3:def 1
for b1, b2, b3 being Element of a1 holds b1 "\/" (b2 "\/" b3) = b2 "\/" (b1 "\/" b3);
end;

:: deftheorem Def1 defines join-Associative ROBBINS3:def 1 :
for b1 being non empty \/-SemiLattStr holds
( b1 is join-Associative iff for b2, b3, b4 being Element of b1 holds b2 "\/" (b3 "\/" b4) = b3 "\/" (b2 "\/" b4) );

definition
let c1 be non empty /\-SemiLattStr ;
attr a1 is meet-Associative means :Def2: :: ROBBINS3:def 2
for b1, b2, b3 being Element of a1 holds b1 "/\" (b2 "/\" b3) = b2 "/\" (b1 "/\" b3);
end;

:: deftheorem Def2 defines meet-Associative ROBBINS3:def 2 :
for b1 being non empty /\-SemiLattStr holds
( b1 is meet-Associative iff for b2, b3, b4 being Element of b1 holds b2 "/\" (b3 "/\" b4) = b3 "/\" (b2 "/\" b4) );

definition
let c1 be non empty LattStr ;
attr a1 is meet-Absorbing means :Def3: :: ROBBINS3:def 3
for b1, b2 being Element of a1 holds b1 "\/" (b1 "/\" b2) = b1;
end;

:: deftheorem Def3 defines meet-Absorbing ROBBINS3:def 3 :
for b1 being non empty LattStr holds
( b1 is meet-Absorbing iff for b2, b3 being Element of b1 holds b2 "\/" (b2 "/\" b3) = b2 );

theorem Th1: :: ROBBINS3:1
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 meet-idempotent & b1 is join-idempotent )
proof end;

theorem Th2: :: ROBBINS3:2
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 meet-commutative & b1 is join-commutative )
proof end;

theorem Th3: :: ROBBINS3:3
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 meet-absorbing
proof end;

theorem Th4: :: ROBBINS3:4
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 meet-associative & b1 is join-associative )
proof end;

theorem Th5: :: ROBBINS3:5
for b1 being non empty LattStr holds
( b1 is Lattice-like iff ( b1 is meet-Associative & b1 is join-Associative & b1 is meet-Absorbing & b1 is join-absorbing ) )
proof end;

registration
cluster non empty Lattice-like -> non empty meet-absorbing join-absorbing join-Associative meet-Associative 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 & b1 is join-absorbing )
by Th5, LATTICES:def 10;
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;

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 b1 being non empty Dneg OrthoRelStr
for b2 being Element of b1 holds (b2 ` ) ` = b2
proof end;

theorem Th7: :: ROBBINS3:7
for b1 being non empty PartialOrdered OrderInvolutive OrthoRelStr
for b2, b3 being Element of b1 st b2 <= b3 holds
b3 ` <= b2 `
proof end;

registration
cluster with_suprema with_infima strict Dneg OrthoRelStr ;
existence
ex b1 being PreOrthoPoset st
( b1 is with_infima & b1 is with_suprema & b1 is strict )
proof end;
end;

notation
let c1 be non empty \/-SemiLattStr ;
let c2, c3 be Element of c1;
synonym c2 |_| c3 for c2 "\/" c3;
end;

notation
let c1 be non empty /\-SemiLattStr ;
let c2, c3 be Element of c1;
synonym c2 |^| c3 for c2 "/\" c3;
end;

notation
let c1 be non empty RelStr ;
let c2, c3 be Element of c1;
synonym c2 "|^|" c3 for c2 "/\" c3;
synonym c2 "|_|" c3 for c2 "\/" c3;
end;

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

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

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

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

registration
cluster TrivLattRelStr -> non empty trivial join-Associative meet-Associative ;
coherence
( not TrivLattRelStr is empty & TrivLattRelStr is trivial )
by STRUCT_0:def 1, REALSET2:def 5;
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 Th8: :: ROBBINS3:8
for b1 being non empty RelStr st the InternalRel of b1 is_reflexive_in the carrier of b1 & the InternalRel of b1 is antisymmetric & the InternalRel of b1 is transitive holds
( b1 is reflexive & b1 is antisymmetric & b1 is transitive )
proof end;

registration
cluster TrivLattRelStr -> non empty reflexive trivial join-Associative meet-Associative ;
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 -> non empty reflexive trivial join-Associative meet-Associative meet-Absorbing ;
coherence
TrivLattRelStr is meet-Absorbing
proof end;
end;

Lemma11: TrivLattRelStr is Lattice-like
;

registration
cluster non empty meet-absorbing join-absorbing Lattice-like join-Associative meet-Associative LattRelStr ;
existence
ex b1 being non empty LattRelStr st b1 is Lattice-like
by Lemma11;
end;

definition
let c1 be Lattice;
redefine func LattRel as LattRel c1 -> Order of the carrier of a1;
coherence
LattRel c1 is Order of the carrier of c1
proof end;
end;

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

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

definition
let c1 be non empty ComplStr ;
attr a1 is involutive means :Def6: :: ROBBINS3:def 6
for b1 being Element of a1 holds (b1 ` ) ` = b1;
end;

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

definition
let c1 be non empty ComplLattStr ;
attr a1 is with_Top means :Def7: :: ROBBINS3:def 7
for b1, b2 being Element of a1 holds b1 |_| (b1 ` ) = b2 |_| (b2 ` );
end;

:: deftheorem Def7 defines with_Top ROBBINS3:def 7 :
for b1 being non empty ComplLattStr holds
( b1 is with_Top iff for b2, b3 being Element of b1 holds b2 |_| (b2 ` ) = b3 |_| (b3 ` ) );

registration
cluster TrivOrtLat -> join-Associative meet-Associative involutive with_Top ;
coherence
( TrivOrtLat is involutive & TrivOrtLat is with_Top )
proof end;
end;

registration
cluster TrivCLRelStr -> non empty trivial join-Associative meet-Associative ;
coherence
( not TrivCLRelStr is empty & TrivCLRelStr is trivial )
by STRUCT_0:def 1, REALSET2:def 5;
end;

registration
cluster TrivCLRelStr -> non empty reflexive trivial join-Associative meet-Associative ;
coherence
TrivCLRelStr is reflexive
proof end;
end;

registration
cluster TrivCLRelStr -> non empty reflexive trivial join-Associative meet-Associative involutive with_Top ;
coherence
( TrivCLRelStr is involutive & TrivCLRelStr is with_Top )
proof end;
end;

registration
cluster non empty meet-absorbing join-absorbing Lattice-like de_Morgan join-Associative meet-Associative 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;

theorem Th9: :: ROBBINS3:9
for b1, b2 being non empty LattStr st LattStr(# the carrier of b1,the L_join of b1,the L_meet of b1 #) = LattStr(# the carrier of b2,the L_join of b2,the L_meet of b2 #) & b1 is join-commutative holds
b2 is join-commutative
proof end;

theorem Th10: :: ROBBINS3:10
for b1, b2 being non empty LattStr st LattStr(# the carrier of b1,the L_join of b1,the L_meet of b1 #) = LattStr(# the carrier of b2,the L_join of b2,the L_meet of b2 #) & b1 is meet-commutative holds
b2 is meet-commutative
proof end;

theorem Th11: :: ROBBINS3:11
for b1, b2 being non empty LattStr st LattStr(# the carrier of b1,the L_join of b1,the L_meet of b1 #) = LattStr(# the carrier of b2,the L_join of b2,the L_meet of b2 #) & b1 is join-associative holds
b2 is join-associative
proof end;

theorem Th12: :: ROBBINS3:12
for b1, b2 being non empty LattStr st LattStr(# the carrier of b1,the L_join of b1,the L_meet of b1 #) = LattStr(# the carrier of b2,the L_join of b2,the L_meet of b2 #) & b1 is meet-associative holds
b2 is meet-associative
proof end;

theorem Th13: :: ROBBINS3:13
for b1, b2 being non empty LattStr st LattStr(# the carrier of b1,the L_join of b1,the L_meet of b1 #) = LattStr(# the carrier of b2,the L_join of b2,the L_meet of b2 #) & b1 is join-absorbing holds
b2 is join-absorbing
proof end;

theorem Th14: :: ROBBINS3:14
for b1, b2 being non empty LattStr st LattStr(# the carrier of b1,the L_join of b1,the L_meet of b1 #) = LattStr(# the carrier of b2,the L_join of b2,the L_meet of b2 #) & b1 is meet-absorbing holds
b2 is meet-absorbing
proof end;

theorem Th15: :: ROBBINS3:15
for b1, b2 being non empty LattStr st LattStr(# the carrier of b1,the L_join of b1,the L_meet of b1 #) = LattStr(# the carrier of b2,the L_join of b2,the L_meet of b2 #) & b1 is Lattice-like holds
b2 is Lattice-like
proof end;

theorem Th16: :: ROBBINS3:16
for b1, b2 being non empty \/-SemiLattStr st \/-SemiLattStr(# the carrier of b1,the L_join of b1 #) = \/-SemiLattStr(# the carrier of b2,the L_join of b2 #) holds
for b3, b4 being Element of b1
for b5, b6 being Element of b2 st b3 = b5 & b4 = b6 holds
b3 "\/" b4 = b5 "\/" b6 ;

theorem Th17: :: ROBBINS3:17
for b1, b2 being non empty /\-SemiLattStr st /\-SemiLattStr(# the carrier of b1,the L_meet of b1 #) = /\-SemiLattStr(# the carrier of b2,the L_meet of b2 #) holds
for b3, b4 being Element of b1
for b5, b6 being Element of b2 st b3 = b5 & b4 = b6 holds
b3 "/\" b4 = b5 "/\" b6 ;

theorem Th18: :: ROBBINS3:18
for b1, b2 being non empty ComplStr
for b3 being Element of b1
for b4 being Element of b2 st the Compl of b1 = the Compl of b2 & b3 = b4 holds
b3 ` = b4 `
proof end;

theorem Th19: :: ROBBINS3:19
for b1, b2 being non empty ComplLattStr st ComplLattStr(# the carrier of b1,the L_join of b1,the Compl of b1 #) = ComplLattStr(# the carrier of b2,the L_join of b2,the Compl of b2 #) & b1 is with_Top holds
b2 is with_Top
proof end;

theorem Th20: :: ROBBINS3:20
for b1, b2 being non empty OrthoLattStr st OrthoLattStr(# the carrier of b1,the L_join of b1,the L_meet of b1,the Compl of b1 #) = OrthoLattStr(# the carrier of b2,the L_join of b2,the L_meet of b2,the Compl of b2 #) & b1 is de_Morgan holds
b2 is de_Morgan
proof end;

theorem Th21: :: ROBBINS3:21
for b1, b2 being non empty OrthoLattStr st OrthoLattStr(# the carrier of b1,the L_join of b1,the L_meet of b1,the Compl of b1 #) = OrthoLattStr(# the carrier of b2,the L_join of b2,the L_meet of b2,the Compl of b2 #) & b1 is involutive holds
b2 is involutive
proof end;

definition
let c1 be RelStr ;
mode RelAugmentation of c1 -> LattRelStr means :: ROBBINS3:def 8
RelStr(# the carrier of a2,the InternalRel of a2 #) = RelStr(# the carrier of a1,the InternalRel of a1 #);
existence
ex b1 being LattRelStr st RelStr(# the carrier of b1,the InternalRel of b1 #) = RelStr(# the carrier of c1,the InternalRel of c1 #)
proof end;
end;

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

definition
let c1 be LattStr ;
mode LatAugmentation of c1 -> LattRelStr means :Def9: :: ROBBINS3:def 9
LattStr(# the carrier of a2,the L_join of a2,the L_meet of a2 #) = LattStr(# the carrier of a1,the L_join of a1,the L_meet of a1 #);
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 c1,the L_join of c1,the L_meet of c1 #)
proof end;
end;

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

registration
let c1 be non empty LattStr ;
cluster -> non empty LatAugmentation of a1;
coherence
for b1 being LatAugmentation of c1 holds not b1 is empty
proof end;
end;

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

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

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

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

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

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

definition
let c1 be non empty \/-SemiLattRelStr ;
attr a1 is naturally_sup-generated means :Def10: :: ROBBINS3:def 10
for b1, b2 being Element of a1 holds
( b1 <= b2 iff b1 |_| b2 = b2 );
end;

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

definition
let c1 be non empty /\-SemiLattRelStr ;
attr a1 is naturally_inf-generated means :Def11: :: ROBBINS3:def 11
for b1, b2 being Element of a1 holds
( b1 <= b2 iff b1 |^| b2 = b1 );
end;

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

registration
let c1 be Lattice;
cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like join-Associative meet-Associative naturally_sup-generated naturally_inf-generated LatAugmentation of a1;
existence
ex b1 being LatAugmentation of c1 st
( b1 is naturally_sup-generated & b1 is naturally_inf-generated & b1 is Lattice-like )
proof end;
end;

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

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

registration
cluster non empty reflexive trivial 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 reflexive trivial -> non empty reflexive Dneg 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 reflexive trivial -> 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 meet-absorbing join-absorbing Lattice-like with_suprema with_infima de_Morgan Dneg PartialOrdered Pure OrderInvolutive join-Associative meet-Associative 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 meet-absorbing join-absorbing Lattice-like with_suprema with_infima join-Associative meet-Associative 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 b1 being non empty naturally_sup-generated LattRelStr
for b2, b3 being Element of b1 holds
( b2 <= b3 iff b2 [= b3 )
proof end;

theorem Th23: :: ROBBINS3:23
for b1 being non empty Lattice-like naturally_sup-generated LattRelStr holds RelStr(# the carrier of b1,the InternalRel of b1 #) = LattPOSet b1
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;

definition
let c1 be OrthoLattStr ;
mode CLatAugmentation of c1 -> OrthoLattRelStr means :Def12: :: ROBBINS3:def 12
OrthoLattStr(# the carrier of a2,the L_join of a2,the L_meet of a2,the Compl of a2 #) = OrthoLattStr(# the carrier of a1,the L_join of a1,the L_meet of a1,the Compl of a1 #);
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 c1,the L_join of c1,the L_meet of c1,the Compl of c1 #)
proof end;
end;

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

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

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

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

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

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

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

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

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

registration
let c1 be non empty Ortholattice;
cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like with_suprema with_infima join-Associative meet-Associative with_Top naturally_sup-generated naturally_inf-generated CLatAugmentation of a1;
existence
ex b1 being CLatAugmentation of c1 st
( b1 is naturally_sup-generated & b1 is naturally_inf-generated & b1 is Lattice-like )
proof end;
end;

registration
cluster non empty meet-absorbing join-absorbing Lattice-like with_suprema with_infima well-complemented de_Morgan join-Associative meet-Associative 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 b1 being non empty with_suprema with_infima PartialOrdered OrthoRelStr
for b2, b3 being Element of b1 st b2 <= b3 holds
( b3 = b2 "|_|" b3 & b2 = b2 "|^|" b3 )
proof end;

definition
let c1 be non empty meet-commutative /\-SemiLattStr ;
let c2, c3 be Element of c1;
redefine func |^| as c2 |^| c3 -> M2(the carrier of a1);
commutativity
for b1, b2 being Element of c1 holds b1 |^| b2 = b2 |^| b1
by LATTICES:def 6;
end;

definition
let c1 be non empty join-commutative \/-SemiLattStr ;
let c2, c3 be Element of c1;
redefine func |_| as c2 |_| c3 -> M2(the carrier of a1);
commutativity
for b1, b2 being Element of c1 holds b1 |_| b2 = b2 |_| b1
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 b1 being non empty Lattice-like with_suprema with_infima naturally_sup-generated OrthoLattRelStr
for b2, b3 being Element of b1 holds b2 "|_|" b3 = b2 |_| b3
proof end;

theorem Th26: :: ROBBINS3:26
for b1 being non empty Lattice-like with_suprema with_infima naturally_sup-generated OrthoLattRelStr
for b2, b3 being Element of b1 holds b2 "|^|" b3 = b2 |^| b3
proof end;

theorem Th27: :: ROBBINS3:27
for b1 being non empty Lattice-like with_suprema with_infima PartialOrdered OrderInvolutive naturally_sup-generated naturally_inf-generated OrthoLattRelStr holds b1 is de_Morgan
proof end;

registration
let c1 be Ortholattice;
cluster -> non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing join-Associative meet-Associative involutive with_Top CLatAugmentation of a1;
coherence
for b1 being CLatAugmentation of c1 holds b1 is involutive
proof end;
end;

registration
let c1 be Ortholattice;
cluster -> non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing de_Morgan join-Associative meet-Associative involutive with_Top CLatAugmentation of a1;
coherence
for b1 being CLatAugmentation of c1 holds b1 is de_Morgan
proof end;
end;

theorem Th28: :: ROBBINS3:28
for 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 holds
( b1 is Orthocomplemented & b1 is PartialOrdered )
proof end;

theorem Th29: :: ROBBINS3:29
for b1 being Ortholattice
for b2 being naturally_sup-generated CLatAugmentation of b1 holds b2 is Orthocomplemented by Th28;

registration
let c1 be Ortholattice;
cluster naturally_sup-generated -> non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing reflexive transitive antisymmetric with_suprema with_infima de_Morgan Orthocomplemented join-Associative meet-Associative involutive with_Top naturally_sup-generated CLatAugmentation of a1;
coherence
for b1 being naturally_sup-generated CLatAugmentation of c1 holds b1 is Orthocomplemented
by Th28;
end;

theorem Th30: :: ROBBINS3:30
for b1 being non empty OrthoLattStr st b1 is Boolean & b1 is well-complemented & b1 is Lattice-like holds
b1 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;