:: ROBBINS3 semantic presentation

begin

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 )
proof
let L be non empty LattStr ; ::_thesis: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing implies ( L is meet-idempotent & L is join-idempotent ) )
assume A1: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) ; ::_thesis: ( L is meet-idempotent & L is join-idempotent )
A2: for x being Element of L holds x "\/" x = x
proof
let a be Element of L; ::_thesis: a "\/" a = a
 a = a "\/" (a "/\" a) by A1, Def3;
hence  a "\/" a = a by A1, LATTICES:def_9; ::_thesis: verum
end;
 for x being Element of L holds x "/\" x = x
proof
let a be Element of L; ::_thesis: a "/\" a = a
 a = a "/\" (a "\/" a) by A1, LATTICES:def_9;
hence  a "/\" a = a by A1, Def3; ::_thesis: verum
end;
hence  ( L is meet-idempotent & L is join-idempotent ) by A2, ROBBINS1:def_7, SHEFFER1:def_9; ::_thesis: verum
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
let L be non empty LattStr ; ::_thesis: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing implies ( L is meet-commutative & L is join-commutative ) )
assume A1: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) ; ::_thesis: ( L is meet-commutative & L is join-commutative )
then A2: ( L is join-idempotent & L is meet-idempotent ) by Th1;
A3: for x, y being Element of L holds x "/\" y = y "/\" x
proof
let a, b be Element of L; ::_thesis: a "/\" b = b "/\" a
a "/\" b = a "/\" (b "/\" (b "\/" a)) by A1, LATTICES:def_9
.= b "/\" (a "/\" (b "\/" a)) by A1, Def2
.= b "/\" (a "/\" (b "\/" (a "\/" a))) by A2, ROBBINS1:def_7
.= b "/\" (a "/\" (a "\/" (b "\/" a))) by A1, Def1
.= b "/\" a by A1, LATTICES:def_9 ;
hence  a "/\" b = b "/\" a ; ::_thesis: verum
end;
 for x, y being Element of L holds x "\/" y = y "\/" x
proof
let a, b be Element of L; ::_thesis: a "\/" b = b "\/" a
a "\/" b = a "\/" (b "\/" (b "/\" a)) by A1, Def3
.= b "\/" (a "\/" (b "/\" a)) by A1, Def1
.= b "\/" (a "\/" (b "/\" (a "/\" a))) by A2, SHEFFER1:def_9
.= b "\/" (a "\/" (a "/\" (b "/\" a))) by A1, Def2
.= b "\/" a by A1, Def3 ;
hence  a "\/" b = b "\/" a ; ::_thesis: verum
end;
hence  ( L is meet-commutative & L is join-commutative ) by A3, LATTICES:def_4, LATTICES:def_6; ::_thesis: verum
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
let L be non empty LattStr ; ::_thesis: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing implies L is meet-absorbing )
assume A1: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) ; ::_thesis: L is meet-absorbing
then A2: ( L is meet-commutative & L is join-commutative ) by Th2;
 for x, y being Element of L holds (x "/\" y) "\/" y = y
proof
let a, b be Element of L; ::_thesis: (a "/\" b) "\/" b = b
b = b "\/" (b "/\" a) by A1, Def3
.= b "\/" (a "/\" b) by A2, LATTICES:def_6
.= (a "/\" b) "\/" b by A2, LATTICES:def_4 ;
hence  (a "/\" b) "\/" b = b ; ::_thesis: verum
end;
hence  L is meet-absorbing by LATTICES:def_8; ::_thesis: verum
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
let L be non empty LattStr ; ::_thesis: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing implies ( L is meet-associative & L is join-associative ) )
assume A1: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) ; ::_thesis: ( L is meet-associative & L is join-associative )
then A2: ( L is meet-commutative & L is join-commutative ) by Th2;
A3: for x, y, z being Element of L holds x "\/" (y "\/" z) = (x "\/" y) "\/" z
proof
let a, b, c be Element of L; ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
a "\/" (b "\/" c) = a "\/" (c "\/" b) by A2, LATTICES:def_4
.= c "\/" (a "\/" b) by A1, Def1
.= (a "\/" b) "\/" c by A2, LATTICES:def_4 ;
hence  a "\/" (b "\/" c) = (a "\/" b) "\/" c ; ::_thesis: verum
end;
 for x, y, z being Element of L holds x "/\" (y "/\" z) = (x "/\" y) "/\" z
proof
let a, b, c be Element of L; ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
a "/\" (b "/\" c) = a "/\" (c "/\" b) by A2, LATTICES:def_6
.= c "/\" (a "/\" b) by A1, Def2
.= (a "/\" b) "/\" c by A2, LATTICES:def_6 ;
hence  a "/\" (b "/\" c) = (a "/\" b) "/\" c ; ::_thesis: verum
end;
hence  ( L is meet-associative & L is join-associative ) by A3, LATTICES:def_5, LATTICES:def_7; ::_thesis: verum
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
let L be non empty LattStr ; ::_thesis: ( L is Lattice-like iff ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) )
A1: ( L is Lattice-like implies ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) )
proof
assume A2: L is Lattice-like ; ::_thesis: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing )
A3: for x, y, z being Element of L holds x "/\" (y "/\" z) = y "/\" (x "/\" z)
proof
let a, b, c be Element of L; ::_thesis: a "/\" (b "/\" c) = b "/\" (a "/\" c)
a "/\" (b "/\" c) = (a "/\" b) "/\" c by A2, LATTICES:def_7
.= (b "/\" a) "/\" c by A2, LATTICES:def_6
.= b "/\" (a "/\" c) by A2, LATTICES:def_7 ;
hence  a "/\" (b "/\" c) = b "/\" (a "/\" c) ; ::_thesis: verum
end;
A4: for x, y being Element of L holds x "\/" (x "/\" y) = x
proof
let a, b be Element of L; ::_thesis: a "\/" (a "/\" b) = a
a = (b "/\" a) "\/" a by A2, LATTICES:def_8
.= (a "/\" b) "\/" a by A2, LATTICES:def_6
.= a "\/" (a "/\" b) by A2, LATTICES:def_4 ;
hence  a "\/" (a "/\" b) = a ; ::_thesis: verum
end;
 for x, y, z being Element of L holds x "\/" (y "\/" z) = y "\/" (x "\/" z)
proof
let a, b, c be Element of L; ::_thesis: a "\/" (b "\/" c) = b "\/" (a "\/" c)
a "\/" (b "\/" c) = (a "\/" b) "\/" c by A2, LATTICES:def_5
.= (b "\/" a) "\/" c by A2, LATTICES:def_4
.= b "\/" (a "\/" c) by A2, LATTICES:def_5 ;
hence  a "\/" (b "\/" c) = b "\/" (a "\/" c) ; ::_thesis: verum
end;
hence  ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) by A2, A3, A4, Def1, Def2, Def3; ::_thesis: verum
end;
 ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing implies L is Lattice-like )
proof
assume A5: ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) ; ::_thesis: L is Lattice-like
then A6: L is meet-absorbing by Th3;
 ( L is meet-commutative & L is join-commutative & L is meet-associative & L is join-associative ) by A5, Th2, Th4;
hence  L is Lattice-like by A5, A6; ::_thesis: verum
end;
hence  ( L is Lattice-like iff ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) ) by A1; ::_thesis: verum
end;

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
proof
let L be non empty PartialOrdered OrthoRelStr ; ::_thesis: ( L is OrderInvolutive implies L is Dneg )
assume  L is OrderInvolutive ; ::_thesis: L is Dneg
then consider f being Function of L,L such that
A1: f = the Compl of L and
A2: f is Orderinvolutive by OPOSET_1:def_18;
 ( f is V296() & f is antitone ) by A2, OPOSET_1:def_17;
hence  L is Dneg by A1, OPOSET_1:def_3; ::_thesis: verum
end;
end;

theorem Th6: :: ROBBINS3:6
for L being non empty Dneg OrthoRelStr
for x being Element of L holds (x `) ` = x
proof
let L be non empty Dneg OrthoRelStr ; ::_thesis: for x being Element of L holds (x `) ` = x
let x be Element of L; ::_thesis: (x `) ` = x
consider f being Function of L,L such that
A1: f = the Compl of L and
A2: f is V296() by OPOSET_1:def_3;
 ( f . x = x ` & f . (f . x) = x ) by A1, A2, PARTIT_2:def_3, ROBBINS1:def_3;
hence  (x `) ` = x by A1, ROBBINS1:def_3; ::_thesis: verum
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
let O be non empty PartialOrdered OrderInvolutive OrthoRelStr ; ::_thesis: for x, y being Element of O st x <= y holds
y ` <= x `
let x, y be Element of O; ::_thesis: ( x <= y implies y ` <= x ` )
assume A1: x <= y ; ::_thesis: y ` <= x `
consider f being Function of O,O such that
A2: f = the Compl of O and
A3: f is Orderinvolutive by OPOSET_1:def_18;
 ( f is V296() & f is antitone ) by A3, OPOSET_1:def_17;
then  f . x >= f . y by A1, WAYBEL_9:def_1;
then  x ` >= f . y by A2, ROBBINS1:def_3;
hence  y ` <= x ` by A2, ROBBINS1:def_3; ::_thesis: verum
end;

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 & b1 is with_suprema & b1 is strict )
proof
take  TrivOrthoRelStr ; ::_thesis: ( TrivOrthoRelStr is with_infima & TrivOrthoRelStr is with_suprema & TrivOrthoRelStr is strict )
thus  ( TrivOrthoRelStr is with_infima & TrivOrthoRelStr is with_suprema & TrivOrthoRelStr is strict ) ; ::_thesis: verum
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
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
proof
 the carrier of TrivLattRelStr = {0} by CARD_1:49;
hence  the carrier of TrivLattRelStr is 1 -element ; :: according to STRUCT_0:def_19 ::_thesis: verum
end;
end;

registration
cluster non empty for \/-SemiLattRelStr ;
existence
 not for b1 being \/-SemiLattRelStr holds b1 is empty
proof
take  TrivLattRelStr ; ::_thesis: not TrivLattRelStr is empty
thus  not TrivLattRelStr is empty ; ::_thesis: verum
end;
cluster non empty for /\-SemiLattRelStr ;
existence
 not for b1 being /\-SemiLattRelStr holds b1 is empty
proof
take  TrivLattRelStr ; ::_thesis: not TrivLattRelStr is empty
thus  not TrivLattRelStr is empty ; ::_thesis: verum
end;
cluster non empty for LattRelStr ;
existence
 not for b1 being LattRelStr holds b1 is empty
proof
take  TrivLattRelStr ; ::_thesis: not TrivLattRelStr is empty
thus  not TrivLattRelStr is empty ; ::_thesis: verum
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
let r be non empty RelStr ; ::_thesis: ( the InternalRel of r is_reflexive_in the carrier of r & the InternalRel of r is antisymmetric & the InternalRel of r is transitive implies ( r is reflexive & r is antisymmetric & r is transitive ) )
set i = the InternalRel of r;
set c = the carrier of r;
assume that
A1: the InternalRel of r is_reflexive_in the carrier of r and
A2: ( the InternalRel of r is antisymmetric & the InternalRel of r is transitive ) ; ::_thesis: ( r is reflexive & r is antisymmetric & r is transitive )
A3: the InternalRel of r is_transitive_in field the InternalRel of r by A2, RELAT_2:def_16;
A4: field the InternalRel of r = the carrier of r by A1, PARTIT_2:21;
then  the InternalRel of r is_antisymmetric_in the carrier of r by A2, RELAT_2:def_12;
hence  ( r is reflexive & r is antisymmetric & r is transitive ) by A1, A4, A3, ORDERS_2:def_2, ORDERS_2:def_3, ORDERS_2:def_4; ::_thesis: verum
end;

registration
cluster TrivLattRelStr  ->  reflexive ;
coherence
 TrivLattRelStr is reflexive
proof
set T = TrivLattRelStr ;
set C = the carrier of TrivLattRelStr;
set I = the InternalRel of TrivLattRelStr;
 field the InternalRel of TrivLattRelStr = the carrier of TrivLattRelStr by PARTIT_2:18;
then  the InternalRel of TrivLattRelStr is_reflexive_in the carrier of TrivLattRelStr by RELAT_2:def_9;
hence  TrivLattRelStr is reflexive by ORDERS_2:def_2; ::_thesis: verum
end;
end;

registration
cluster reflexive transitive antisymmetric with_suprema with_infima for 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
take  TrivLattRelStr ; ::_thesis: ( TrivLattRelStr is antisymmetric & TrivLattRelStr is reflexive & TrivLattRelStr is transitive & TrivLattRelStr is with_suprema & TrivLattRelStr is with_infima )
thus  ( TrivLattRelStr is antisymmetric & TrivLattRelStr is reflexive & TrivLattRelStr is transitive & TrivLattRelStr is with_suprema & TrivLattRelStr is with_infima ) ; ::_thesis: verum
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 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
A1: LattRel L =  {  [p,q] where p, q is Element of L : p [= q  }  by FILTER_1:def_8;
 LattRel L c= [: the carrier of L, the carrier of L:]
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LattRel L or x in [: the carrier of L, the carrier of L:] )
assume  x in LattRel L ; ::_thesis: x in [: the carrier of L, the carrier of L:]
then  ex p, q being Element of L st
( x = [p,q] & p [= q ) by A1;
hence  x in [: the carrier of L, the carrier of L:] by ZFMISC_1:87; ::_thesis: verum
end;
then reconsider R = LattRel L as Relation of the carrier of L ;
A2: R is_antisymmetric_in the carrier of L
proof
let x, y be set ; :: according to RELAT_2:def_4 ::_thesis: ( not x in the carrier of L or not y in the carrier of L or not [x,y] in R or not [y,x] in R or x = y )
assume  ( x in the carrier of L & y in the carrier of L ) ; ::_thesis: ( not [x,y] in R or not [y,x] in R or x = y )
then reconsider x9 = x, y9 = y as Element of L ;
assume  ( [x,y] in R & [y,x] in R ) ; ::_thesis: x = y
then  ( x9 [= y9 & y9 [= x9 ) by FILTER_1:31;
hence  x = y by LATTICES:8; ::_thesis: verum
end;
A3: R is_transitive_in the carrier of L
proof
let x, y, z be set ; :: according to RELAT_2:def_8 ::_thesis: ( not x in the carrier of L or not y in the carrier of L or not z in the carrier of L or not [x,y] in R or not [y,z] in R or [x,z] in R )
assume  ( x in the carrier of L & y in the carrier of L & z in the carrier of L ) ; ::_thesis: ( not [x,y] in R or not [y,z] in R or [x,z] in R )
then reconsider x9 = x, y9 = y, z9 = z as Element of L ;
assume  ( [x,y] in R & [y,z] in R ) ; ::_thesis: [x,z] in R
then  ( x9 [= y9 & y9 [= z9 ) by FILTER_1:31;
then  x9 [= z9 by LATTICES:7;
hence  [x,z] in R by FILTER_1:31; ::_thesis: verum
end;
A4: R is_reflexive_in the carrier of L
proof
let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in the carrier of L or [x,x] in R )
assume  x in the carrier of L ; ::_thesis: [x,x] in R
then reconsider x = x as Element of L ;
 x [= x ;
hence  [x,x] in R by FILTER_1:31; ::_thesis: verum
end;
then  ( dom R = the carrier of L & field R = the carrier of L ) by ORDERS_1:13;
hence  LattRel L is Order of the carrier of L by A4, A2, A3, PARTFUN1:def_2, RELAT_2:def_9, RELAT_2:def_12, RELAT_2:def_16; ::_thesis: verum
end;
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 #);

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 & TrivOrtLat is with_Top )
proof
thus  TrivOrtLat is involutive ::_thesis: TrivOrtLat is with_Top
proof
let x be Element of TrivOrtLat; :: according to ROBBINS3:def_6 ::_thesis: (x `) ` = x
thus  (x `) ` = x by STRUCT_0:def_10; ::_thesis: verum
end;
thus  TrivOrtLat is with_Top ::_thesis: verum
proof
let x, y be Element of TrivOrtLat; :: according to ROBBINS3:def_7 ::_thesis: x |_| (x `) = y |_| (y `)
thus  x |_| (x `) = y |_| (y `) by STRUCT_0:def_10; ::_thesis: verum
end;
end;
end;

registration
cluster TrivCLRelStr  -> 1 -element ;
coherence
 TrivCLRelStr is 1 -element
proof
 the carrier of TrivCLRelStr = {0} by CARD_1:49;
hence  the carrier of TrivCLRelStr is 1 -element ; :: according to STRUCT_0:def_19 ::_thesis: verum
end;
end;

registration
cluster TrivCLRelStr  ->  reflexive ;
coherence
 TrivCLRelStr is reflexive
proof
 for x being Element of TrivCLRelStr holds x <= x
proof
let x be Element of TrivCLRelStr; ::_thesis: x <= x
 [x,x] in id {{}} by CARD_1:49, RELAT_1:def_10;
hence  x <= x by CARD_1:49, ORDERS_2:def_5; ::_thesis: verum
end;
hence  TrivCLRelStr is reflexive by YELLOW_0:def_1; ::_thesis: verum
end;
end;

registration
cluster TrivCLRelStr  ->  involutive with_Top ;
coherence
 ( TrivCLRelStr is involutive & TrivCLRelStr is with_Top )
proof
set L = TrivCLRelStr ;
thus  TrivCLRelStr is involutive ::_thesis: TrivCLRelStr is with_Top
proof
let x be Element of TrivCLRelStr; :: according to ROBBINS3:def_6 ::_thesis: (x `) ` = x
thus  (x `) ` = x by STRUCT_0:def_10; ::_thesis: verum
end;
thus  TrivCLRelStr is with_Top ::_thesis: verum
proof
let x, y be Element of TrivCLRelStr; :: according to ROBBINS3:def_7 ::_thesis: x |_| (x `) = y |_| (y `)
thus  x |_| (x `) = y |_| (y `) by STRUCT_0:def_10; ::_thesis: verum
end;
end;
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 & b1 is with_Top & b1 is de_Morgan & b1 is Lattice-like )
proof
take  TrivOrtLat ; ::_thesis: ( TrivOrtLat is involutive & TrivOrtLat is with_Top & TrivOrtLat is de_Morgan & TrivOrtLat is Lattice-like )
thus  ( TrivOrtLat is involutive & TrivOrtLat is with_Top & TrivOrtLat is de_Morgan & TrivOrtLat is Lattice-like ) ; ::_thesis: verum
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
let K, L be non empty LattStr ; ::_thesis: ( 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 implies L is join-commutative )
assume that
A1: 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 #) and
A2: K is join-commutative ; ::_thesis: L is join-commutative
 L is join-commutative
proof
let x, y be Element of L; :: according to LATTICES:def_4 ::_thesis: x |_| y = y |_| x
reconsider x9 = x, y9 = y as Element of K by A1;
 x9 |_| y9 = y9 |_| x9 by A2, LATTICES:def_4;
hence  x |_| y = y |_| x by A1; ::_thesis: verum
end;
hence  L is join-commutative ; ::_thesis: verum
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
let K, L be non empty LattStr ; ::_thesis: ( 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 implies L is meet-commutative )
assume that
A1: 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 #) and
A2: K is meet-commutative ; ::_thesis: L is meet-commutative
 L is meet-commutative
proof
let x, y be Element of L; :: according to LATTICES:def_6 ::_thesis: x |^| y = y |^| x
reconsider x9 = x, y9 = y as Element of K by A1;
 x9 "/\" y9 = y9 "/\" x9 by A2, LATTICES:def_6;
hence  x |^| y = y |^| x by A1; ::_thesis: verum
end;
hence  L is meet-commutative ; ::_thesis: verum
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
let K, L be non empty LattStr ; ::_thesis: ( 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 implies L is join-associative )
assume that
A1: 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 #) and
A2: K is join-associative ; ::_thesis: L is join-associative
 L is join-associative
proof
let x, y, z be Element of L; :: according to LATTICES:def_5 ::_thesis: x |_| (y |_| z) = (x |_| y) |_| z
reconsider x9 = x, y9 = y, z9 = z as Element of K by A1;
 (x9 |_| y9) |_| z9 = x9 |_| (y9 |_| z9) by A2, LATTICES:def_5;
hence  x |_| (y |_| z) = (x |_| y) |_| z by A1; ::_thesis: verum
end;
hence  L is join-associative ; ::_thesis: verum
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
let K, L be non empty LattStr ; ::_thesis: ( 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 implies L is meet-associative )
assume that
A1: 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 #) and
A2: K is meet-associative ; ::_thesis: L is meet-associative
 L is meet-associative
proof
let x, y, z be Element of L; :: according to LATTICES:def_7 ::_thesis: x |^| (y |^| z) = (x |^| y) |^| z
reconsider x9 = x, y9 = y, z9 = z as Element of K by A1;
 (x9 "/\" y9) "/\" z9 = x9 "/\" (y9 "/\" z9) by A2, LATTICES:def_7;
hence  x |^| (y |^| z) = (x |^| y) |^| z by A1; ::_thesis: verum
end;
hence  L is meet-associative ; ::_thesis: verum
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
let K, L be non empty LattStr ; ::_thesis: ( 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 implies L is join-absorbing )
assume that
A1: 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 #) and
A2: K is join-absorbing ; ::_thesis: L is join-absorbing
 L is join-absorbing
proof
let x, y be Element of L; :: according to LATTICES:def_9 ::_thesis: x |^| (x |_| y) = x
reconsider x9 = x, y9 = y as Element of K by A1;
 x9 "/\" (x9 "\/" y9) = x9 by A2, LATTICES:def_9;
hence  x |^| (x |_| y) = x by A1; ::_thesis: verum
end;
hence  L is join-absorbing ; ::_thesis: verum
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
let K, L be non empty LattStr ; ::_thesis: ( 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 implies L is meet-absorbing )
assume that
A1: 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 #) and
A2: K is meet-absorbing ; ::_thesis: L is meet-absorbing
 L is meet-absorbing
proof
let x, y be Element of L; :: according to LATTICES:def_8 ::_thesis: (x |^| y) |_| y = y
reconsider x9 = x, y9 = y as Element of K by A1;
 (x9 "/\" y9) "\/" y9 = y9 by A2, LATTICES:def_8;
hence  (x |^| y) |_| y = y by A1; ::_thesis: verum
end;
hence  L is meet-absorbing ; ::_thesis: verum
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
let K, L be non empty LattStr ; ::_thesis: ( 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 implies L is Lattice-like )
assume  ( 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 ) ; ::_thesis: L is Lattice-like
then  ( L is join-commutative & L is join-associative & L is meet-absorbing & L is meet-commutative & L is meet-associative & L is join-absorbing ) by Th9, Th10, Th11, Th12, Th13, Th14;
hence  L is Lattice-like ; ::_thesis: verum
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
let K, L be non empty ComplStr ; ::_thesis: 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 `
let x be Element of K; ::_thesis: for y being Element of L st the Compl of K = the Compl of L & x = y holds
x ` = y `
let y be Element of L; ::_thesis: ( the Compl of K = the Compl of L & x = y implies x ` = y ` )
assume  ( the Compl of K = the Compl of L & x = y ) ; ::_thesis: x ` = y `
then x ` = the Compl of L . y by ROBBINS1:def_3
.= y ` by ROBBINS1:def_3 ;
hence  x ` = y ` ; ::_thesis: verum
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
let K, L be non empty ComplLLattStr ; ::_thesis: ( 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 implies L is with_Top )
assume that
A1: 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 #) and
A2: K is with_Top ; ::_thesis: L is with_Top
 for x, y being Element of L holds x |_| (x `) = y |_| (y `)
proof
let x, y be Element of L; ::_thesis: x |_| (x `) = y |_| (y `)
reconsider x9 = x, y9 = y as Element of K by A1;
x |_| (x `) = x9 |_| (x9 `) by A1, Th18
.= y9 |_| (y9 `) by A2, Def7
.= y |_| (y `) by A1, Th18 ;
hence  x |_| (x `) = y |_| (y `) ; ::_thesis: verum
end;
hence  L is with_Top by Def7; ::_thesis: verum
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
let K, L be non empty OrthoLattStr ; ::_thesis: ( 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 implies L is de_Morgan )
assume that
A1: 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 #) and
A2: K is de_Morgan ; ::_thesis: L is de_Morgan
 for x, y being Element of L holds x "/\" y = ((x `) "\/" (y `)) `
proof
let x, y be Element of L; ::_thesis: x "/\" y = ((x `) "\/" (y `)) `
reconsider x9 = x, y9 = y as Element of K by A1;
A3: ( x ` = x9 ` & y ` = y9 ` ) by A1, Th18;
x "/\" y = x9 "/\" y9 by A1
.= ((x9 `) "\/" (y9 `)) ` by A2, ROBBINS1:def_23
.= ((x `) "\/" (y `)) ` by A1, A3, Th18 ;
hence  x "/\" y = ((x `) "\/" (y `)) ` ; ::_thesis: verum
end;
hence  L is de_Morgan by ROBBINS1:def_23; ::_thesis: verum
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
let K, L be non empty OrthoLattStr ; ::_thesis: ( 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 implies L is involutive )
assume that
A1: 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 #) and
A2: K is involutive ; ::_thesis: L is involutive
 for x being Element of L holds (x `) ` = x
proof
let x be Element of L; ::_thesis: (x `) ` = x
reconsider x9 = x as Element of K by A1;
 x ` = x9 ` by A1, Th18;
then (x `) ` = (x9 `) ` by A1, Th18
.= x by A2, Def6 ;
hence  (x `) ` = x ; ::_thesis: verum
end;
hence  L is involutive by Def6; ::_thesis: verum
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
set A = the BinOp of the carrier of R;
set L = LattRelStr(# the carrier of R, the BinOp of the carrier of R, the BinOp of the carrier of R, the InternalRel of R #);
take  LattRelStr(# the carrier of R, the BinOp of the carrier of R, the BinOp of the carrier of R, the InternalRel of R #) ; ::_thesis: RelStr(# the carrier of LattRelStr(# the carrier of R, the BinOp of the carrier of R, the BinOp of the carrier of R, the InternalRel of R #), the InternalRel of LattRelStr(# the carrier of R, the BinOp of the carrier of R, the BinOp of the carrier of R, the InternalRel of R #) #) = RelStr(# the carrier of R, the InternalRel of R #)
thus  RelStr(# the carrier of LattRelStr(# the carrier of R, the BinOp of the carrier of R, the BinOp of the carrier of R, the InternalRel of R #), the InternalRel of LattRelStr(# the carrier of R, the BinOp of the carrier of R, the BinOp of the carrier of R, the InternalRel of R #) #) = RelStr(# the carrier of R, the InternalRel of R #) ; ::_thesis: verum
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
set IR = the Relation of the carrier of R;
set L = LattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R #);
take  LattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R #) ; ::_thesis: LattStr(# the carrier of LattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R #), the L_join of LattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R #), the L_meet of LattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R #) #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #)
thus  LattStr(# the carrier of LattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R #), the L_join of LattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R #), the L_meet of LattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R #) #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) ; ::_thesis: verum
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 for LatAugmentation of L;
coherence
 for b1 being LatAugmentation of L holds not b1 is empty
proof
let R be LatAugmentation of L; ::_thesis: not R is empty
 LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) by Def9;
hence  not R is empty ; ::_thesis: verum
end;
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
proof
let R be LatAugmentation of L; ::_thesis: R is meet-associative
 LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) by Def9;
hence  R is meet-associative by Th12; ::_thesis: verum
end;
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
proof
let R be LatAugmentation of L; ::_thesis: R is join-associative
 LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) by Def9;
hence  R is join-associative by Th11; ::_thesis: verum
end;
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
proof
let R be LatAugmentation of L; ::_thesis: R is meet-commutative
 LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) by Def9;
hence  R is meet-commutative by Th10; ::_thesis: verum
end;
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
proof
let R be LatAugmentation of L; ::_thesis: R is join-commutative
 LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) by Def9;
hence  R is join-commutative by Th9; ::_thesis: verum
end;
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
proof
let R be LatAugmentation of L; ::_thesis: R is join-absorbing
 LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) by Def9;
hence  R is join-absorbing by Th13; ::_thesis: verum
end;
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
proof
let R be LatAugmentation of L; ::_thesis: R is meet-absorbing
 LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) by Def9;
hence  R is meet-absorbing by Th14; ::_thesis: verum
end;
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 & b1 is naturally_inf-generated & b1 is Lattice-like )
proof
set R = LattRel L;
set S = LattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L) #);
 LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of LattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L) #), the L_join of LattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L) #), the L_meet of LattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L) #) #) ;
then reconsider S = LattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L) #) as LatAugmentation of L by Def9;
 for x, y being Element of S holds
( x <= y iff x |^| y = x )
proof
let x, y be Element of S; ::_thesis: ( x <= y iff x |^| y = x )
reconsider x9 = x, y9 = y as Element of L ;
hereby  ::_thesis: ( x |^| y = x implies x <= y )
assume  x <= y ; ::_thesis: x |^| y = x
then  [x,y] in the InternalRel of S by ORDERS_2:def_5;
then  x9 [= y9 by FILTER_1:31;
then  x9 |^| y9 = x9 by LATTICES:4;
hence  x |^| y = x ; ::_thesis: verum
end;
A1: x9 |^| y9 = x |^| y ;
assume  x |^| y = x ; ::_thesis: x <= y
then  x9 [= y9 by A1, LATTICES:4;
then  [x9,y9] in LattRel L by FILTER_1:31;
hence  x <= y by ORDERS_2:def_5; ::_thesis: verum
end;
then A2: S is naturally_inf-generated by Def11;
 for x, y being Element of S holds
( x <= y iff x |_| y = y )
proof
let x, y be Element of S; ::_thesis: ( x <= y iff x |_| y = y )
reconsider x9 = x, y9 = y as Element of L ;
hereby  ::_thesis: ( x |_| y = y implies x <= y )
assume  x <= y ; ::_thesis: x |_| y = y
then  [x,y] in the InternalRel of S by ORDERS_2:def_5;
then  x9 [= y9 by FILTER_1:31;
then  x9 |_| y9 = y9 by LATTICES:def_3;
hence  x |_| y = y ; ::_thesis: verum
end;
A3: x9 |_| y9 = x |_| y ;
assume  x |_| y = y ; ::_thesis: x <= y
then  x9 [= y9 by A3, LATTICES:def_3;
then  [x9,y9] in LattRel L by FILTER_1:31;
hence  x <= y by ORDERS_2:def_5; ::_thesis: verum
end;
then  S is naturally_sup-generated by Def10;
hence  ex b1 being LatAugmentation of L st
( b1 is naturally_sup-generated & b1 is naturally_inf-generated & b1 is Lattice-like ) by A2; ::_thesis: verum
end;
end;

registration
cluster1 -element reflexive for LattRelStr ;
existence
 ex b1 being LattRelStr st
( b1 is 1 -element & b1 is reflexive )
proof
take  TrivLattRelStr ; ::_thesis: ( TrivLattRelStr is 1 -element & TrivLattRelStr is reflexive )
thus  ( TrivLattRelStr is 1 -element & TrivLattRelStr is reflexive ) ; ::_thesis: verum
end;
end;

registration
cluster1 -element reflexive for OrthoLattRelStr ;
existence
 ex b1 being OrthoLattRelStr st
( b1 is 1 -element & b1 is reflexive )
proof
take  TrivCLRelStr ; ::_thesis: ( TrivCLRelStr is 1 -element & TrivCLRelStr is reflexive )
thus  ( TrivCLRelStr is 1 -element & TrivCLRelStr is reflexive ) ; ::_thesis: verum
end;
end;

registration
cluster1 -element reflexive for OrthoRelStr ;
existence
 ex b1 being OrthoRelStr st
( b1 is 1 -element & b1 is reflexive )
proof
take  TrivOrthoRelStr ; ::_thesis: ( TrivOrthoRelStr is 1 -element & TrivOrthoRelStr is reflexive )
thus  ( TrivOrthoRelStr is 1 -element & TrivOrthoRelStr is reflexive ) ; ::_thesis: verum
end;
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 & b1 is with_Top & b1 is de_Morgan & b1 is well-complemented )
proof
let L be 1 -element OrthoLattStr ; ::_thesis: ( L is involutive & L is with_Top & L is de_Morgan & L is well-complemented )
reconsider L9 = L as 1 -element OrthoLattStr ;
A1: for x being Element of L9 holds (x `) ` = x by STRUCT_0:def_10;
A2: for x being Element of L9 holds x ` is_a_complement_of x
proof
let x be Element of L9; ::_thesis: x ` is_a_complement_of x
A3: ( (x `) |_| x = Top L9 & (x `) |^| x = Bottom L9 ) by STRUCT_0:def_10;
 ( x |_| (x `) = Top L9 & x |^| (x `) = Bottom L9 ) by STRUCT_0:def_10;
hence  x ` is_a_complement_of x by A3, LATTICES:def_18; ::_thesis: verum
end;
 ( ( for x, y being Element of L9 holds x |_| (x `) = y |_| (y `) ) & ( for x, y being Element of L9 holds x |^| y = ((x `) |_| (y `)) ` ) ) by STRUCT_0:def_10;
hence  ( L is involutive & L is with_Top & L is de_Morgan & L is well-complemented ) by A1, A2, Def6, Def7, ROBBINS1:def_10, ROBBINS1:def_23; ::_thesis: verum
end;
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 & b1 is Pure & b1 is PartialOrdered )
proof
let L be 1 -element reflexive OrthoRelStr ; ::_thesis: ( L is OrderInvolutive & L is Pure & L is PartialOrdered )
reconsider L9 = L as 1 -element reflexive OrthoRelStr ;
reconsider f = the Compl of L9 as Function of L9,L9 ;
consider x being set  such that
A1: the carrier of L9 = {x} by ZFMISC_1:131;
 f = id {x} by A1, FUNCT_2:51;
then A2: f is V296() ;
then A3: L9 is Dneg by OPOSET_1:def_3;
 for z, y being Element of L9 st z <= y holds
f . z >= f . y
proof
let z, y be Element of L9; ::_thesis: ( z <= y implies f . z >= f . y )
assume  z <= y ; ::_thesis: f . z >= f . y
 ( f . z = x & f . y = x ) by A1, FUNCT_2:50;
hence  f . z >= f . y by YELLOW_0:def_1; ::_thesis: verum
end;
then  f is antitone by WAYBEL_9:def_1;
then  f is Orderinvolutive by A2, OPOSET_1:def_17;
hence  ( L is OrderInvolutive & L is Pure & L is PartialOrdered ) by A3, OPOSET_1:def_15, OPOSET_1:def_18; ::_thesis: verum
end;
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 & b1 is naturally_inf-generated )
proof
let L be 1 -element reflexive LattRelStr ; ::_thesis: ( L is naturally_sup-generated & L is naturally_inf-generated )
reconsider L9 = L as 1 -element reflexive LattRelStr ;
 ( ( for x, y being Element of L9 holds
( x <= y iff x |_| y = y ) ) & ( for x, y being Element of L9 holds
( x <= y iff x |^| y = x ) ) ) by STRUCT_0:def_10;
hence  ( L is naturally_sup-generated & L is naturally_inf-generated ) by Def10, Def11; ::_thesis: verum
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 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
take  TrivCLRelStr ; ::_thesis: ( TrivCLRelStr is with_infima & TrivCLRelStr is with_suprema & TrivCLRelStr is naturally_sup-generated & TrivCLRelStr is naturally_inf-generated & TrivCLRelStr is de_Morgan & TrivCLRelStr is Lattice-like & TrivCLRelStr is OrderInvolutive & TrivCLRelStr is Pure & TrivCLRelStr is PartialOrdered )
thus  ( TrivCLRelStr is with_infima & TrivCLRelStr is with_suprema & TrivCLRelStr is naturally_sup-generated & TrivCLRelStr is naturally_inf-generated & TrivCLRelStr is de_Morgan & TrivCLRelStr is Lattice-like & TrivCLRelStr is OrderInvolutive & TrivCLRelStr is Pure & TrivCLRelStr is PartialOrdered ) ; ::_thesis: verum
end;
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 & b1 is with_suprema & b1 is naturally_sup-generated & b1 is naturally_inf-generated & b1 is Lattice-like )
proof
take  TrivLattRelStr ; ::_thesis: ( TrivLattRelStr is with_infima & TrivLattRelStr is with_suprema & TrivLattRelStr is naturally_sup-generated & TrivLattRelStr is naturally_inf-generated & TrivLattRelStr is Lattice-like )
thus  ( TrivLattRelStr is with_infima & TrivLattRelStr is with_suprema & TrivLattRelStr is naturally_sup-generated & TrivLattRelStr is naturally_inf-generated & TrivLattRelStr is Lattice-like ) ; ::_thesis: verum
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
let L be non empty naturally_sup-generated LattRelStr ; ::_thesis: for x, y being Element of L holds
( x <= y iff x [= y )
let x, y be Element of L; ::_thesis: ( x <= y iff x [= y )
hereby  ::_thesis: ( x [= y implies x <= y )
assume  x <= y ; ::_thesis: x [= y
then  x |_| y = y by Def10;
hence  x [= y by LATTICES:def_3; ::_thesis: verum
end;
assume  x [= y ; ::_thesis: x <= y
then  x |_| y = y by LATTICES:def_3;
hence  x <= y by Def10; ::_thesis: verum
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
let L be non empty Lattice-like naturally_sup-generated LattRelStr ; ::_thesis: RelStr(# the carrier of L, the InternalRel of L #) = LattPOSet L
A1: for x, y being set holds
( [x,y] in the InternalRel of L iff [x,y] in LattRel L )
proof
let x, y be set ; ::_thesis: ( [x,y] in the InternalRel of L iff [x,y] in LattRel L )
hereby  ::_thesis: ( [x,y] in LattRel L implies [x,y] in the InternalRel of L )
assume A2: [x,y] in the InternalRel of L ; ::_thesis: [x,y] in LattRel L
then reconsider x9 = x, y9 = y as Element of L by ZFMISC_1:87;
 x9 <= y9 by A2, ORDERS_2:def_5;
then  x9 [= y9 by Th22;
hence  [x,y] in LattRel L by FILTER_1:31; ::_thesis: verum
end;
assume A3: [x,y] in LattRel L ; ::_thesis: [x,y] in the InternalRel of L
then reconsider x9 = x, y9 = y as Element of L by ZFMISC_1:87;
 x9 [= y9 by A3, FILTER_1:31;
then  x9 <= y9 by Th22;
hence  [x,y] in the InternalRel of L by ORDERS_2:def_5; ::_thesis: verum
end;
 LattPOSet L = RelStr(# the carrier of L,(LattRel L) #) by LATTICE3:def_2;
hence  RelStr(# the carrier of L, the InternalRel of L #) = LattPOSet L by A1, RELAT_1:def_2; ::_thesis: verum
end;

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 & b1 is Lattice-like holds
( b1 is with_infima & b1 is with_suprema )
proof
let L be non empty LattRelStr ; ::_thesis: ( L is naturally_sup-generated & L is Lattice-like implies ( L is with_infima & L is with_suprema ) )
assume  ( L is naturally_sup-generated & L is Lattice-like ) ; ::_thesis: ( L is with_infima & L is with_suprema )
then reconsider L9 = L as non empty Lattice-like naturally_sup-generated LattRelStr ;
 ( LattPOSet L9 is with_suprema & LattPOSet L9 is with_infima ) ;
then  ( RelStr(# the carrier of L9, the InternalRel of L9 #) is with_suprema & RelStr(# the carrier of L9, the InternalRel of L9 #) is with_infima ) by Th23;
hence  ( L is with_infima & L is with_suprema ) by YELLOW_7:14, YELLOW_7:15; ::_thesis: verum
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
set IR = the Relation of the carrier of R;
set L = OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #);
take  OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #) ; ::_thesis: OrthoLattStr(# the carrier of OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #), the L_join of OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #), the L_meet of OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #), the Compl of OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #) #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #)
thus  OrthoLattStr(# the carrier of OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #), the L_join of OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #), the L_meet of OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #), the Compl of OrthoLattRelStr(# the carrier of R, the L_join of R, the L_meet of R, the Relation of the carrier of R, the Compl of R #) #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) ; ::_thesis: verum
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 for CLatAugmentation of L;
coherence
 for b1 being CLatAugmentation of L holds not b1 is empty
proof
let R be CLatAugmentation of L; ::_thesis: not R is empty
 OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) by Def12;
hence  not R is empty ; ::_thesis: verum
end;
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
proof
let R be CLatAugmentation of L; ::_thesis: R is meet-associative
 OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) by Def12;
then  LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) ;
hence  R is meet-associative by Th12; ::_thesis: verum
end;
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
proof
let R be CLatAugmentation of L; ::_thesis: R is join-associative
 OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) by Def12;
then  LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) ;
hence  R is join-associative by Th11; ::_thesis: verum
end;
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
proof
let R be CLatAugmentation of L; ::_thesis: R is meet-commutative
 OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) by Def12;
then  LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) ;
hence  R is meet-commutative by Th10; ::_thesis: verum
end;
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
proof
let R be CLatAugmentation of L; ::_thesis: R is join-commutative
 OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) by Def12;
then  LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) ;
hence  R is join-commutative by Th9; ::_thesis: verum
end;
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
proof
let R be CLatAugmentation of L; ::_thesis: R is meet-absorbing
 OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) by Def12;
then  LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) ;
hence  R is meet-absorbing by Th14; ::_thesis: verum
end;
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
proof
let R be CLatAugmentation of L; ::_thesis: R is join-absorbing
 OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) by Def12;
then  LattStr(# the carrier of L, the L_join of L, the L_meet of L #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) ;
hence  R is join-absorbing by Th13; ::_thesis: verum
end;
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
proof
let R be CLatAugmentation of L; ::_thesis: R is with_Top
 OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) by Def12;
then  ComplLLattStr(# the carrier of L, the L_join of L, the Compl of L #) = ComplLLattStr(# the carrier of R, the L_join of R, the Compl of R #) ;
hence  R is with_Top by Th19; ::_thesis: verum
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 b1 being CLatAugmentation of L st
( b1 is naturally_sup-generated & b1 is naturally_inf-generated & b1 is Lattice-like )
proof
set R = LattRel L;
set S = OrthoLattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L), the Compl of L #);
 OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of OrthoLattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L), the Compl of L #), the L_join of OrthoLattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L), the Compl of L #), the L_meet of OrthoLattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L), the Compl of L #), the Compl of OrthoLattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L), the Compl of L #) #) ;
then reconsider S = OrthoLattRelStr(# the carrier of L, the L_join of L, the L_meet of L,(LattRel L), the Compl of L #) as CLatAugmentation of L by Def12;
 for x, y being Element of S holds
( x <= y iff x |^| y = x )
proof
let x, y be Element of S; ::_thesis: ( x <= y iff x |^| y = x )
reconsider x9 = x, y9 = y as Element of L ;
hereby  ::_thesis: ( x |^| y = x implies x <= y )
assume  x <= y ; ::_thesis: x |^| y = x
then  [x9,y9] in the InternalRel of S by ORDERS_2:def_5;
then  x9 [= y9 by FILTER_1:31;
then  x9 |^| y9 = x9 by LATTICES:4;
hence  x |^| y = x ; ::_thesis: verum
end;
A1: x9 |^| y9 = x |^| y ;
assume  x |^| y = x ; ::_thesis: x <= y
then  x9 [= y9 by A1, LATTICES:4;
then  [x9,y9] in LattRel L by FILTER_1:31;
hence  x <= y by ORDERS_2:def_5; ::_thesis: verum
end;
then A2: S is naturally_inf-generated by Def11;
 for x, y being Element of S holds
( x <= y iff x |_| y = y )
proof
let x, y be Element of S; ::_thesis: ( x <= y iff x |_| y = y )
reconsider x9 = x, y9 = y as Element of L ;
hereby  ::_thesis: ( x |_| y = y implies x <= y )
assume  x <= y ; ::_thesis: x |_| y = y
then  [x,y] in the InternalRel of S by ORDERS_2:def_5;
then  x9 [= y9 by FILTER_1:31;
then  x9 |_| y9 = y9 by LATTICES:def_3;
hence  x |_| y = y ; ::_thesis: verum
end;
A3: x9 |_| y9 = x |_| y ;
assume  x |_| y = y ; ::_thesis: x <= y
then  x9 [= y9 by A3, LATTICES:def_3;
then  [x9,y9] in LattRel L by FILTER_1:31;
hence  x <= y by ORDERS_2:def_5; ::_thesis: verum
end;
then  S is naturally_sup-generated by Def10;
hence  ex b1 being CLatAugmentation of L st
( b1 is naturally_sup-generated & b1 is naturally_inf-generated & b1 is Lattice-like ) by A2; ::_thesis: verum
end;
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 & b1 is with_Top & b1 is de_Morgan & b1 is Lattice-like & b1 is naturally_sup-generated & b1 is well-complemented )
proof
take  TrivCLRelStr ; ::_thesis: ( TrivCLRelStr is involutive & TrivCLRelStr is with_Top & TrivCLRelStr is de_Morgan & TrivCLRelStr is Lattice-like & TrivCLRelStr is naturally_sup-generated & TrivCLRelStr is well-complemented )
thus  ( TrivCLRelStr is involutive & TrivCLRelStr is with_Top & TrivCLRelStr is de_Morgan & TrivCLRelStr is Lattice-like & TrivCLRelStr is naturally_sup-generated & TrivCLRelStr is well-complemented ) ; ::_thesis: verum
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
let L be non empty with_suprema with_infima PartialOrdered OrthoRelStr ; ::_thesis: for x, y being Element of L st x <= y holds
( y = x "|_|" y & x = x "|^|" y )
let a, b be Element of L; ::_thesis: ( a <= b implies ( b = a "|_|" b & a = a "|^|" b ) )
assume A1: a <= b ; ::_thesis: ( b = a "|_|" b & a = a "|^|" b )
then  b = b "|_|" a by YELLOW_0:24;
hence  ( b = a "|_|" b & a = a "|^|" b ) by A1, LATTICE3:13, YELLOW_0:25; ::_thesis: verum
end;

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 & b1 is join-absorbing & b1 is meet-commutative & b1 is naturally_sup-generated holds
b1 is reflexive
proof
let L be non empty LattRelStr ; ::_thesis: ( L is meet-absorbing & L is join-absorbing & L is meet-commutative & L is naturally_sup-generated implies L is reflexive )
assume  ( L is meet-absorbing & L is join-absorbing & L is meet-commutative & L is naturally_sup-generated ) ; ::_thesis: L is reflexive
then reconsider L9 = L as non empty meet-commutative meet-absorbing join-absorbing naturally_sup-generated LattRelStr ;
 for x being Element of L9 holds x <= x
proof
let x be Element of L9; ::_thesis: x <= x
 x [= x ;
hence  x <= x by Th22; ::_thesis: verum
end;
hence  L is reflexive by YELLOW_0:def_1; ::_thesis: verum
end;
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 & b1 is naturally_sup-generated holds
b1 is transitive
proof
let L be non empty LattRelStr ; ::_thesis: ( L is join-associative & L is naturally_sup-generated implies L is transitive )
assume  ( L is join-associative & L is naturally_sup-generated ) ; ::_thesis: L is transitive
then reconsider L9 = L as non empty join-associative naturally_sup-generated LattRelStr ;
 for x, y, z being Element of L9 st x <= y & y <= z holds
x <= z
proof
let x, y, z be Element of L9; ::_thesis: ( x <= y & y <= z implies x <= z )
assume  ( x <= y & y <= z ) ; ::_thesis: x <= z
then  ( x [= y & y [= z ) by Th22;
then  x [= z by LATTICES:7;
hence  x <= z by Th22; ::_thesis: verum
end;
hence  L is transitive by YELLOW_0:def_2; ::_thesis: verum
end;
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 & b1 is naturally_sup-generated holds
b1 is antisymmetric
proof
let L be non empty LattRelStr ; ::_thesis: ( L is join-commutative & L is naturally_sup-generated implies L is antisymmetric )
assume  ( L is join-commutative & L is naturally_sup-generated ) ; ::_thesis: L is antisymmetric
then reconsider L9 = L as non empty join-commutative naturally_sup-generated LattRelStr ;
 for x, y being Element of L9 st x <= y & y <= x holds
x = y
proof
let x, y be Element of L9; ::_thesis: ( x <= y & y <= x implies x = y )
assume  ( x <= y & y <= x ) ; ::_thesis: x = y
then  ( x [= y & y [= x ) by Th22;
hence  x = y by LATTICES:8; ::_thesis: verum
end;
hence  L is antisymmetric by YELLOW_0:def_3; ::_thesis: verum
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
let L be non empty Lattice-like with_suprema with_infima naturally_sup-generated OrthoLattRelStr ; ::_thesis: for x, y being Element of L holds x "|_|" y = x |_| y
let x, y be Element of L; ::_thesis: x "|_|" y = x |_| y
 x <= x "|_|" y by YELLOW_0:22;
then A1: x [= x "|_|" y by Th22;
 y <= x "|_|" y by YELLOW_0:22;
then A2: y [= x "|_|" y by Th22;
 x [= x |_| y by LATTICES:5;
then A3: x <= x |_| y by Th22;
 y [= x |_| y by LATTICES:5;
then A4: y <= x |_| y by Th22;
(x |_| y) "|_|" (x "|_|" y) = ((x |_| y) "|_|" x) "|_|" y by LATTICE3:14
.= (x |_| y) "|_|" y by A3, YELLOW_0:24
.= x |_| y by A4, YELLOW_0:24 ;
then  x "|_|" y <= x |_| y by YELLOW_0:24;
then A5: x "|_|" y [= x |_| y by Th22;
(x "|_|" y) |_| (x |_| y) = ((x "|_|" y) |_| x) |_| y by LATTICES:def_5
.= (x "|_|" y) |_| y by A1, LATTICES:def_3
.= x "|_|" y by A2, LATTICES:def_3 ;
hence  x "|_|" y = x |_| y by A5, LATTICES:def_3; ::_thesis: verum
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
let L be non empty Lattice-like with_suprema with_infima naturally_sup-generated OrthoLattRelStr ; ::_thesis: for x, y being Element of L holds x "|^|" y = x |^| y
let x, y be Element of L; ::_thesis: x "|^|" y = x |^| y
 x "|^|" y <= x by YELLOW_0:23;
then A1: x "|^|" y [= x by Th22;
 x "|^|" y <= y by YELLOW_0:23;
then A2: x "|^|" y [= y by Th22;
 x |^| y [= x by LATTICES:6;
then A3: x |^| y <= x by Th22;
 x |^| y [= y by LATTICES:6;
then A4: x |^| y <= y by Th22;
(x |^| y) "|^|" (x "|^|" y) = ((x |^| y) "|^|" x) "|^|" y by LATTICE3:16
.= (x |^| y) "|^|" y by A3, YELLOW_0:25
.= x |^| y by A4, YELLOW_0:25 ;
then  x |^| y <= x "|^|" y by YELLOW_0:25;
then A5: x |^| y [= x "|^|" y by Th22;
(x "|^|" y) |^| (x |^| y) = ((x "|^|" y) |^| x) |^| y by LATTICES:def_7
.= (x "|^|" y) |^| y by A1, LATTICES:4
.= x "|^|" y by A2, LATTICES:4 ;
hence  x "|^|" y = x |^| y by A5, LATTICES:4; ::_thesis: verum
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
let L be non empty Lattice-like with_suprema with_infima PartialOrdered OrderInvolutive naturally_sup-generated naturally_inf-generated OrthoLattRelStr ; ::_thesis: L is de_Morgan
A1: for x, y being Element of L holds (x `) "|_|" (y `) <= (x "|^|" y) `
proof
let a, b be Element of L; ::_thesis: (a `) "|_|" (b `) <= (a "|^|" b) `
set i = a "|^|" b;
set s = (a `) "|_|" (b `);
 a "|^|" b <= a by YELLOW_0:23;
then  a ` <= (a "|^|" b) ` by Th7;
then A2: (a `) "|_|" (b `) <= ((a "|^|" b) `) "|_|" (b `) by WAYBEL_1:2;
 a "|^|" b <= b by YELLOW_0:23;
then  b ` <= (a "|^|" b) ` by Th7;
then  (a "|^|" b) ` = (b `) "|_|" ((a "|^|" b) `) by Th24;
hence  (a `) "|_|" (b `) <= (a "|^|" b) ` by A2, LATTICE3:13; ::_thesis: verum
end;
A3: for x, y being Element of L holds (x "|_|" y) ` <= (x `) "|^|" (y `)
proof
let a, b be Element of L; ::_thesis: (a "|_|" b) ` <= (a `) "|^|" (b `)
set i = (a `) "|^|" (b `);
set s = a "|_|" b;
 a <= a "|_|" b by YELLOW_0:22;
then  (a "|_|" b) ` <= a ` by Th7;
then A4: ((a "|_|" b) `) "|^|" (b `) <= (a `) "|^|" (b `) by WAYBEL_1:1;
 b <= a "|_|" b by YELLOW_0:22;
then  (a "|_|" b) ` <= b ` by Th7;
hence  (a "|_|" b) ` <= (a `) "|^|" (b `) by A4, Th24; ::_thesis: verum
end;
 for x, y being Element of L holds ((x `) |_| (y `)) ` = x |^| y
proof
let a, b be Element of L; ::_thesis: ((a `) |_| (b `)) ` = a |^| b
set s = (a `) "|_|" (b `);
set i = a "|^|" b;
 ( (a `) ` = a & (b `) ` = b ) by Th6;
then A5: ((a `) "|_|" (b `)) ` <= a "|^|" b by A3;
 ((a "|^|" b) `) ` <= ((a `) "|_|" (b `)) ` by A1, Th7;
then A6: a "|^|" b <= ((a `) "|_|" (b `)) ` by Th6;
 ( a "|^|" b = a |^| b & (a `) "|_|" (b `) = (a `) |_| (b `) ) by Th25, Th26;
hence  ((a `) |_| (b `)) ` = a |^| b by A5, A6, ORDERS_2:2; ::_thesis: verum
end;
hence  L is de_Morgan by ROBBINS1:def_23; ::_thesis: verum
end;

registration
let L be Ortholattice;
cluster  ->  involutive for CLatAugmentation of L;
coherence
 for b1 being CLatAugmentation of L holds b1 is involutive
proof
let R be CLatAugmentation of L; ::_thesis: R is involutive
 OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) by Def12;
hence  R is involutive by Th21; ::_thesis: verum
end;
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
proof
let R be CLatAugmentation of L; ::_thesis: R is de_Morgan
 OrthoLattStr(# the carrier of L, the L_join of L, the L_meet of L, the Compl of L #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) by Def12;
hence  R is de_Morgan by Th20; ::_thesis: verum
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
let L be non empty OrthoLattRelStr ; ::_thesis: ( L is involutive & L is with_Top & L is de_Morgan & L is Lattice-like & L is naturally_sup-generated implies ( L is Orthocomplemented & L is PartialOrdered ) )
assume  ( L is involutive & L is with_Top & L is de_Morgan & L is Lattice-like & L is naturally_sup-generated ) ; ::_thesis: ( L is Orthocomplemented & L is PartialOrdered )
then reconsider L9 = L as non empty Lattice-like de_Morgan involutive with_Top naturally_sup-generated OrthoLattRelStr ;
reconsider f = the Compl of L9 as Function of L9,L9 ;
 for x, y being Element of L9 st x <= y holds
f . x >= f . y
proof
let x, y be Element of L9; ::_thesis: ( x <= y implies f . x >= f . y )
assume  x <= y ; ::_thesis: f . x >= f . y
then  x [= y by Th22;
then A1: x ` = (x |^| y) ` by LATTICES:4
.= (((x `) |_| (y `)) `) ` by ROBBINS1:def_23
.= (x `) |_| (y `) by Def6 ;
 ( f . x = x ` & f . y = y ` ) by ROBBINS1:def_3;
hence  f . x >= f . y by A1, Def10; ::_thesis: verum
end;
then A2: f is antitone by WAYBEL_9:def_1;
A3: for y being Element of L9 holds
( ex_sup_of {y,(f . y)},L9 & ex_inf_of {y,(f . y)},L9 & "\/" ({y,(f . y)},L9) is_maximum_of the carrier of L9 & "/\" ({y,(f . y)},L9) is_minimum_of the carrier of L9 )
proof
set xx = "\/" ( the carrier of L9,L9);
let y be Element of L9; ::_thesis: ( ex_sup_of {y,(f . y)},L9 & ex_inf_of {y,(f . y)},L9 & "\/" ({y,(f . y)},L9) is_maximum_of the carrier of L9 & "/\" ({y,(f . y)},L9) is_minimum_of the carrier of L9 )
thus  ex_sup_of {y,(f . y)},L9 by YELLOW_0:20; ::_thesis: ( ex_inf_of {y,(f . y)},L9 & "\/" ({y,(f . y)},L9) is_maximum_of the carrier of L9 & "/\" ({y,(f . y)},L9) is_minimum_of the carrier of L9 )
thus  ex_inf_of {y,(f . y)},L9 by YELLOW_0:21; ::_thesis: ( "\/" ({y,(f . y)},L9) is_maximum_of the carrier of L9 & "/\" ({y,(f . y)},L9) is_minimum_of the carrier of L9 )
set t = y |_| (y `);
 for b being Element of L9 st b in the carrier of L9 holds
b <= y |_| (y `)
proof
let b be Element of L9; ::_thesis: ( b in the carrier of L9 implies b <= y |_| (y `) )
assume  b in the carrier of L9 ; ::_thesis: b <= y |_| (y `)
b |_| (y |_| (y `)) = b |_| (b |_| (b `)) by Def7
.= (b |_| b) |_| (b `) by LATTICES:def_5
.= b |_| (b `)
.= y |_| (y `) by Def7 ;
then  b [= y |_| (y `) by LATTICES:def_3;
hence  b <= y |_| (y `) by Th22; ::_thesis: verum
end;
then A4: y |_| (y `) is_>=_than the carrier of L9 by LATTICE3:def_9;
then  L9 is upper-bounded by YELLOW_0:def_5;
then A5: ex_sup_of the carrier of L9,L9 by YELLOW_0:43;
reconsider t = y |_| (y `) as Element of L9 ;
A6: for a being Element of L9 st the carrier of L9 is_<=_than a holds
t <= a by LATTICE3:def_9;
"\/" ({y,(f . y)},L9) = "\/" ({y,(y `)},L9) by ROBBINS1:def_3
.= y "|_|" (y `) by YELLOW_0:41
.= y |_| (y `) by Th25
.= "\/" ( the carrier of L9,L9) by A4, A5, A6, YELLOW_0:def_9 ;
hence  "\/" ({y,(f . y)},L9) is_maximum_of the carrier of L9 by A5, WAYBEL_1:def_7; ::_thesis: "/\" ({y,(f . y)},L9) is_minimum_of the carrier of L9
set xx = "/\" ( the carrier of L9,L9);
set t = y |^| (y `);
A7: for a, b being Element of L9 holds a |^| (a `) = b |^| (b `)
proof
let a, b be Element of L9; ::_thesis: a |^| (a `) = b |^| (b `)
a |^| (a `) = ((a `) |_| ((a `) `)) ` by ROBBINS1:def_23
.= ((b `) |_| ((b `) `)) ` by Def7
.= b |^| (b `) by ROBBINS1:def_23 ;
hence  a |^| (a `) = b |^| (b `) ; ::_thesis: verum
end;
 for b being Element of L9 st b in the carrier of L9 holds
b >= y |^| (y `)
proof
let b be Element of L9; ::_thesis: ( b in the carrier of L9 implies b >= y |^| (y `) )
assume  b in the carrier of L9 ; ::_thesis: b >= y |^| (y `)
b |^| (y |^| (y `)) = b |^| (b |^| (b `)) by A7
.= (b |^| b) |^| (b `) by LATTICES:def_7
.= b |^| (b `)
.= y |^| (y `) by A7 ;
then  y |^| (y `) [= b by LATTICES:4;
hence  b >= y |^| (y `) by Th22; ::_thesis: verum
end;
then A8: y |^| (y `) is_<=_than the carrier of L9 by LATTICE3:def_8;
then  L9 is lower-bounded by YELLOW_0:def_4;
then A9: ex_inf_of the carrier of L9,L9 by YELLOW_0:42;
reconsider t = y |^| (y `) as Element of L9 ;
A10: for a being Element of L9 st the carrier of L9 is_>=_than a holds
t >= a by LATTICE3:def_8;
"/\" ({y,(f . y)},L9) = "/\" ({y,(y `)},L9) by ROBBINS1:def_3
.= y "|^|" (y `) by YELLOW_0:40
.= y |^| (y `) by Th26
.= "/\" ( the carrier of L9,L9) by A8, A9, A10, YELLOW_0:def_10 ;
hence  "/\" ({y,(f . y)},L9) is_minimum_of the carrier of L9 by A9, WAYBEL_1:def_6; ::_thesis: verum
end;
 for x being Element of L9 holds f . (f . x) = x
proof
let x be Element of L9; ::_thesis: f . (f . x) = x
f . (f . x) = f . (x `) by ROBBINS1:def_3
.= (x `) ` by ROBBINS1:def_3
.= x by Def6 ;
hence  f . (f . x) = x ; ::_thesis: verum
end;
then  f is V296() by PARTIT_2:def_3;
then  f is Orderinvolutive by A2, OPOSET_1:def_17;
then  f OrthoComplement_on L9 by A3, OPOSET_1:def_21;
hence  ( L is Orthocomplemented & L is PartialOrdered ) by OPOSET_1:def_22; ::_thesis: verum
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 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
let L be non empty OrthoLattStr ; ::_thesis: ( L is Boolean & L is well-complemented & L is Lattice-like implies L is Ortholattice )
assume  ( L is Boolean & L is well-complemented & L is Lattice-like ) ; ::_thesis: L is Ortholattice
then reconsider L9 = L as non empty Lattice-like Boolean well-complemented OrthoLattStr ;
A1: for x, y being Element of L9 holds x "/\" y = ((x `) "\/" (y `)) ` by ROBBINS1:33;
 ( ( for x being Element of L9 holds (x `) ` = x ) & ( for x, y being Element of L9 holds x |_| (x `) = y |_| (y `) ) ) by ROBBINS1:3, ROBBINS1:4;
hence  L is Ortholattice by A1, Def6, Def7, ROBBINS1:def_23; ::_thesis: verum
end;

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 & b1 is well-complemented & b1 is Lattice-like holds
( b1 is involutive & b1 is with_Top & b1 is de_Morgan ) by Th30;
end;