:: by Adam Grabowski and Markus Moschner

::

:: Received December 28, 2004

:: Copyright (c) 2004-2019 Association of Mizar Users

:: Originally proved by McCune with the help of OTTER

definition

let L be non empty \/-SemiLattStr ;

end;
attr L is join-Associative means :: ROBBINS3:def 1

for x, y, z being Element of L holds x "\/" (y "\/" z) = y "\/" (x "\/" z);

for x, y, z being Element of L holds x "\/" (y "\/" z) = y "\/" (x "\/" z);

:: deftheorem defines join-Associative ROBBINS3:def 1 :

for L being non empty \/-SemiLattStr holds

( L is join-Associative iff for x, y, z being Element of L holds x "\/" (y "\/" z) = y "\/" (x "\/" z) );

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 ;

end;
attr L is meet-Associative means :: ROBBINS3:def 2

for x, y, z being Element of L holds x "/\" (y "/\" z) = y "/\" (x "/\" z);

for x, y, z being Element of L holds x "/\" (y "/\" z) = y "/\" (x "/\" z);

:: deftheorem defines meet-Associative ROBBINS3:def 2 :

for L being non empty /\-SemiLattStr holds

( L is meet-Associative iff for x, y, z being Element of L holds x "/\" (y "/\" z) = y "/\" (x "/\" z) );

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 ;

end;
attr L is meet-Absorbing means :: ROBBINS3:def 3

for x, y being Element of L holds x "\/" (x "/\" y) = x;

for x, y being Element of L holds x "\/" (x "/\" y) = x;

:: deftheorem defines meet-Absorbing ROBBINS3:def 3 :

for L being non empty LattStr holds

( L is meet-Absorbing iff for x, y being Element of L holds x "\/" (x "/\" y) = x );

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 )

( L is meet-idempotent & L is join-idempotent )

proof end;

theorem Th2: :: ROBBINS3:2

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

( L is meet-commutative & L is join-commutative )

( L is meet-commutative & L is join-commutative )

proof end;

theorem Th3: :: ROBBINS3:3

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

L is meet-absorbing

L is meet-absorbing

proof end;

theorem Th4: :: ROBBINS3:4

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

( L is meet-associative & L is join-associative )

( L is meet-associative & L is join-associative )

proof end;

theorem Th5: :: ROBBINS3:5

for L being non empty LattStr holds

( L is Lattice-like iff ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) )

( L is Lattice-like iff ( L is meet-Associative & L is join-Associative & L is meet-Absorbing & L is join-absorbing ) )

proof end;

registration

for b_{1} being non empty LattStr st b_{1} is Lattice-like holds

( b_{1} is meet-Associative & b_{1} is join-Associative & b_{1} is meet-Absorbing )
by Th5;

for b_{1} being non empty LattStr st b_{1} is meet-Associative & b_{1} is join-Associative & b_{1} is meet-Absorbing & b_{1} is join-absorbing holds

b_{1} is Lattice-like
by Th5;

end;

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

coherence for b

( b

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

coherence for b

b

registration

coherence

for b_{1} being non empty PartialOrdered OrthoRelStr st b_{1} is OrderInvolutive holds

b_{1} is Dneg

end;
for b

b

proof end;

theorem Th7: :: ROBBINS3:7

for O being non empty PartialOrdered OrderInvolutive OrthoRelStr

for x, y being Element of O st x <= y holds

y ` <= x `

for x, y being Element of O st x <= y holds

y ` <= x `

proof end;

registration

ex b_{1} being PreOrthoPoset st

( b_{1} is with_infima & b_{1} is with_suprema & b_{1} is strict )
end;

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

existence ex b

( b

proof end;

notation
end;

notation
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;
let x, y be Element of L;

synonym x "|^|" y for x "/\" y;

synonym x "|_|" y for x "\/" y;

definition

attr c_{1} is strict ;

struct \/-SemiLattRelStr -> \/-SemiLattStr , RelStr ;

aggr \/-SemiLattRelStr(# carrier, L_join, InternalRel #) -> \/-SemiLattRelStr ;

end;
struct \/-SemiLattRelStr -> \/-SemiLattStr , RelStr ;

aggr \/-SemiLattRelStr(# carrier, L_join, InternalRel #) -> \/-SemiLattRelStr ;

definition

attr c_{1} is strict ;

struct /\-SemiLattRelStr -> /\-SemiLattStr , RelStr ;

aggr /\-SemiLattRelStr(# carrier, L_meet, InternalRel #) -> /\-SemiLattRelStr ;

end;
struct /\-SemiLattRelStr -> /\-SemiLattStr , RelStr ;

aggr /\-SemiLattRelStr(# carrier, L_meet, InternalRel #) -> /\-SemiLattRelStr ;

definition

attr c_{1} is strict ;

struct LattRelStr -> /\-SemiLattRelStr , \/-SemiLattRelStr , LattStr ;

aggr LattRelStr(# carrier, L_join, L_meet, InternalRel #) -> LattRelStr ;

end;
struct LattRelStr -> /\-SemiLattRelStr , \/-SemiLattRelStr , LattStr ;

aggr LattRelStr(# carrier, L_join, L_meet, InternalRel #) -> LattRelStr ;

:: deftheorem defines TrivLattRelStr ROBBINS3:def 4 :

TrivLattRelStr = LattRelStr(# {0},op2,op2,(id {0}) #);

TrivLattRelStr = LattRelStr(# {0},op2,op2,(id {0}) #);

registration

existence

not for b_{1} being \/-SemiLattRelStr holds b_{1} is empty

not for b_{1} being /\-SemiLattRelStr holds b_{1} is empty

not for b_{1} being LattRelStr holds b_{1} is empty

end;
not for b

proof end;

existence not for b

proof end;

existence not for b

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

( R is reflexive & R is antisymmetric & R is transitive )

proof end;

registration
end;

registration

existence

ex b_{1} being LattRelStr st

( b_{1} is antisymmetric & b_{1} is reflexive & b_{1} is transitive & b_{1} is with_suprema & b_{1} is with_infima )

end;
ex b

( b

proof end;

registration
end;

Lm1: TrivLattRelStr is Lattice-like

;

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

end;
:: original: LattRel

redefine func LattRel L -> Order of the carrier of L;

coherence

LattRel L is Order of the carrier of L

proof end;

definition

attr c_{1} is strict ;

struct OrthoLattRelStr -> LattRelStr , OrthoLattStr , OrthoRelStr ;

aggr OrthoLattRelStr(# carrier, L_join, L_meet, InternalRel, Compl #) -> OrthoLattRelStr ;

end;
struct OrthoLattRelStr -> LattRelStr , OrthoLattStr , OrthoRelStr ;

aggr OrthoLattRelStr(# carrier, L_join, L_meet, InternalRel, Compl #) -> OrthoLattRelStr ;

definition

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

end;

func TrivCLRelStr -> OrthoLattRelStr equals :: ROBBINS3:def 5

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

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

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

:: deftheorem defines TrivCLRelStr ROBBINS3:def 5 :

TrivCLRelStr = OrthoLattRelStr(# {0},op2,op2,(id {0}),op1 #);

TrivCLRelStr = OrthoLattRelStr(# {0},op2,op2,(id {0}),op1 #);

:: Axiomatics for ortholattices is the classical one for lattices extended

:: by the three following:

:: x ^ y = c(c(x) v c(y)). % DM de_Morgan from ROBBINS1

:: c(c(x)) = x. % CC involutive from OPOSET_1, too specific

:: x v c(x) = y v c(y). % ONE

:: by the three following:

:: x ^ y = c(c(x) v c(y)). % DM de_Morgan from ROBBINS1

:: c(c(x)) = x. % CC involutive from OPOSET_1, too specific

:: x v c(x) = y v c(y). % ONE

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

for L being non empty ComplStr holds

( L is involutive iff for x being Element of L holds (x `) ` = x );

:: 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 `) );

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

registration
end;

registration
end;

registration

ex b_{1} being 1 -element OrthoLattStr st

( b_{1} is involutive & b_{1} is with_Top & b_{1} is de_Morgan & b_{1} is Lattice-like )
end;

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

existence ex b

( b

proof end;

definition
end;

theorem Th9: :: ROBBINS3:9

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

L is join-commutative

L is join-commutative

proof end;

theorem Th10: :: ROBBINS3:10

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

L is meet-commutative

L is meet-commutative

proof end;

theorem Th11: :: ROBBINS3:11

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

L is join-associative

L is join-associative

proof end;

theorem Th12: :: ROBBINS3:12

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

L is meet-associative

L is meet-associative

proof end;

theorem Th13: :: ROBBINS3:13

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

L is join-absorbing

L is join-absorbing

proof end;

theorem Th14: :: ROBBINS3:14

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

L is meet-absorbing

L is meet-absorbing

proof end;

theorem :: ROBBINS3:15

theorem :: ROBBINS3:16

theorem :: ROBBINS3:17

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 `

for x being Element of K

for y being Element of L st the Compl of K = the Compl of L & x = y holds

x ` = y `

proof end;

theorem Th19: :: ROBBINS3:19

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

L is with_Top

L is with_Top

proof end;

theorem Th20: :: ROBBINS3:20

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

L is de_Morgan

L is de_Morgan

proof end;

theorem Th21: :: ROBBINS3:21

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

L is involutive

L is involutive

proof end;

definition

let R be RelStr ;

ex b_{1} being LattRelStr st RelStr(# the carrier of b_{1}, the InternalRel of b_{1} #) = RelStr(# the carrier of R, the InternalRel of R #)

end;
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 RelStr(# the carrier of it, the InternalRel of it #) = RelStr(# the carrier of R, the InternalRel of R #);

ex b

proof end;

:: deftheorem defines RelAugmentation ROBBINS3:def 8 :

for R being RelStr

for b_{2} being LattRelStr holds

( b_{2} is RelAugmentation of R iff RelStr(# the carrier of b_{2}, the InternalRel of b_{2} #) = RelStr(# the carrier of R, the InternalRel of R #) );

for R being RelStr

for b

( b

definition

let R be LattStr ;

ex b_{1} being LattRelStr st LattStr(# the carrier of b_{1}, the L_join of b_{1}, the L_meet of b_{1} #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #)

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

ex b

proof end;

:: deftheorem Def9 defines LatAugmentation ROBBINS3:def 9 :

for R being LattStr

for b_{2} being LattRelStr holds

( b_{2} is LatAugmentation of R iff LattStr(# the carrier of b_{2}, the L_join of b_{2}, the L_meet of b_{2} #) = LattStr(# the carrier of R, the L_join of R, the L_meet of R #) );

for R being LattStr

for b

( b

registration

let L be non empty LattStr ;

coherence

for b_{1} being LatAugmentation of L holds not b_{1} is empty

end;
coherence

for b

proof end;

registration

let L be non empty meet-associative LattStr ;

coherence

for b_{1} being LatAugmentation of L holds b_{1} is meet-associative

end;
coherence

for b

proof end;

registration

let L be non empty join-associative LattStr ;

coherence

for b_{1} being LatAugmentation of L holds b_{1} is join-associative

end;
coherence

for b

proof end;

registration

let L be non empty meet-commutative LattStr ;

coherence

for b_{1} being LatAugmentation of L holds b_{1} is meet-commutative

end;
coherence

for b

proof end;

registration

let L be non empty join-commutative LattStr ;

coherence

for b_{1} being LatAugmentation of L holds b_{1} is join-commutative

end;
coherence

for b

proof end;

registration

let L be non empty join-absorbing LattStr ;

coherence

for b_{1} being LatAugmentation of L holds b_{1} is join-absorbing

end;
coherence

for b

proof end;

registration

let L be non empty meet-absorbing LattStr ;

coherence

for b_{1} being LatAugmentation of L holds b_{1} is meet-absorbing

end;
coherence

for b

proof end;

definition

let L be non empty \/-SemiLattRelStr ;

end;
attr L is naturally_sup-generated means :Def10: :: ROBBINS3:def 10

for x, y being Element of L holds

( x <= y iff x |_| y = y );

for x, y being Element of L holds

( x <= y iff x |_| y = y );

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

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 ;

end;
attr L is naturally_inf-generated means :: ROBBINS3:def 11

for x, y being Element of L holds

( x <= y iff x |^| y = x );

for x, y being Element of L holds

( x <= y iff x |^| y = x );

:: deftheorem defines naturally_inf-generated ROBBINS3:def 11 :

for L being non empty /\-SemiLattRelStr holds

( L is naturally_inf-generated iff for x, y being Element of L holds

( x <= y iff x |^| y = x ) );

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;

ex b_{1} being LatAugmentation of L st

( b_{1} is naturally_sup-generated & b_{1} is naturally_inf-generated & b_{1} is Lattice-like )

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

existence ex b

( b

proof end;

registration
end;

registration
end;

registration
end;

registration

coherence

for b_{1} being 1 -element OrthoLattStr holds

( b_{1} is involutive & b_{1} is with_Top & b_{1} is de_Morgan & b_{1} is well-complemented )

end;
for b

( b

proof end;

registration

for b_{1} being 1 -element reflexive OrthoRelStr holds

( b_{1} is OrderInvolutive & b_{1} is Pure & b_{1} is PartialOrdered )
end;

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

coherence for b

( b

proof end;

registration

for b_{1} being 1 -element reflexive LattRelStr holds

( b_{1} is naturally_sup-generated & b_{1} is naturally_inf-generated )
end;

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

coherence for b

( b

proof end;

registration

ex b_{1} being non empty OrthoLattRelStr st

( b_{1} is with_infima & b_{1} is with_suprema & b_{1} is naturally_sup-generated & b_{1} is naturally_inf-generated & b_{1} is de_Morgan & b_{1} is Lattice-like & b_{1} is OrderInvolutive & b_{1} is Pure & b_{1} is PartialOrdered )
end;

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

existence ex b

( b

proof end;

registration

ex b_{1} being non empty LattRelStr st

( b_{1} is with_infima & b_{1} is with_suprema & b_{1} is naturally_sup-generated & b_{1} is naturally_inf-generated & b_{1} is Lattice-like )
end;

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

existence ex b

( b

proof end;

theorem Th22: :: ROBBINS3:22

for L being non empty naturally_sup-generated LattRelStr

for x, y being Element of L holds

( x <= y iff x [= y ) by Def10;

for x, y being Element of L holds

( x <= y iff x [= y ) by Def10;

theorem Th23: :: ROBBINS3:23

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

proof end;

registration

for b_{1} being non empty LattRelStr st b_{1} is naturally_sup-generated & b_{1} is Lattice-like holds

( b_{1} is with_infima & b_{1} is with_suprema )
end;

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

coherence for b

( b

proof end;

definition

let R be OrthoLattStr ;

ex b_{1} being OrthoLattRelStr st OrthoLattStr(# the carrier of b_{1}, the L_join of b_{1}, the L_meet of b_{1}, the Compl of b_{1} #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #)

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

ex b

proof end;

:: deftheorem Def12 defines CLatAugmentation ROBBINS3:def 12 :

for R being OrthoLattStr

for b_{2} being OrthoLattRelStr holds

( b_{2} is CLatAugmentation of R iff OrthoLattStr(# the carrier of b_{2}, the L_join of b_{2}, the L_meet of b_{2}, the Compl of b_{2} #) = OrthoLattStr(# the carrier of R, the L_join of R, the L_meet of R, the Compl of R #) );

for R being OrthoLattStr

for b

( b

registration

let L be non empty OrthoLattStr ;

coherence

for b_{1} being CLatAugmentation of L holds not b_{1} is empty

end;
coherence

for b

proof end;

registration

let L be non empty meet-associative OrthoLattStr ;

coherence

for b_{1} being CLatAugmentation of L holds b_{1} is meet-associative

end;
coherence

for b

proof end;

registration

let L be non empty join-associative OrthoLattStr ;

coherence

for b_{1} being CLatAugmentation of L holds b_{1} is join-associative

end;
coherence

for b

proof end;

registration

let L be non empty meet-commutative OrthoLattStr ;

coherence

for b_{1} being CLatAugmentation of L holds b_{1} is meet-commutative

end;
coherence

for b

proof end;

registration

let L be non empty join-commutative OrthoLattStr ;

coherence

for b_{1} being CLatAugmentation of L holds b_{1} is join-commutative

end;
coherence

for b

proof end;

registration

let L be non empty meet-absorbing OrthoLattStr ;

coherence

for b_{1} being CLatAugmentation of L holds b_{1} is meet-absorbing

end;
coherence

for b

proof end;

registration

let L be non empty join-absorbing OrthoLattStr ;

coherence

for b_{1} being CLatAugmentation of L holds b_{1} is join-absorbing

end;
coherence

for b

proof end;

registration

let L be non empty with_Top OrthoLattStr ;

coherence

for b_{1} being CLatAugmentation of L holds b_{1} is with_Top

end;
coherence

for b

proof end;

registration

let L be Ortholattice;

ex b_{1} being CLatAugmentation of L st

( b_{1} is naturally_sup-generated & b_{1} is naturally_inf-generated & b_{1} is Lattice-like )

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

existence ex b

( b

proof end;

registration

ex b_{1} being non empty OrthoLattRelStr st

( b_{1} is involutive & b_{1} is with_Top & b_{1} is de_Morgan & b_{1} is Lattice-like & b_{1} is naturally_sup-generated & b_{1} is well-complemented )
end;

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

existence ex b

( b

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

for x, y being Element of L st x <= y holds

( y = x "|_|" y & x = x "|^|" y )

proof end;

definition

let L be non empty meet-commutative /\-SemiLattStr ;

let a, b be Element of L;

:: original: |^|

redefine func a |^| b -> M3( the carrier of L);

commutativity

for a, b being Element of L holds a |^| b = b |^| a by LATTICES:def 6;

end;
let a, b be Element of L;

:: original: |^|

redefine func a |^| b -> M3( the carrier of L);

commutativity

for a, b being Element of L holds a |^| b = b |^| a by LATTICES:def 6;

definition

let L be non empty join-commutative \/-SemiLattStr ;

let a, b be Element of L;

:: original: |_|

redefine func a |_| b -> M3( the carrier of L);

commutativity

for a, b being Element of L holds a |_| b = b |_| a by LATTICES:def 4;

end;
let a, b be Element of L;

:: original: |_|

redefine func a |_| b -> M3( the carrier of L);

commutativity

for a, b being Element of L holds a |_| b = b |_| a by LATTICES:def 4;

registration

for b_{1} being non empty LattRelStr st b_{1} is meet-absorbing & b_{1} is join-absorbing & b_{1} is meet-commutative & b_{1} is naturally_sup-generated holds

b_{1} is reflexive
end;

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

coherence for b

b

proof end;

registration

coherence

for b_{1} being non empty LattRelStr st b_{1} is join-associative & b_{1} is naturally_sup-generated holds

b_{1} is transitive

end;
for b

b

proof end;

registration

for b_{1} being non empty LattRelStr st b_{1} is join-commutative & b_{1} is naturally_sup-generated holds

b_{1} is antisymmetric
end;

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

coherence for b

b

proof 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

for x, y being Element of L holds x "|_|" y = x |_| y

proof end;

theorem Th26: :: ROBBINS3:26

for L being non empty Lattice-like with_suprema with_infima naturally_sup-generated OrthoLattRelStr

for x, y being Element of L holds x "|^|" y = x |^| y

for x, y being Element of L holds x "|^|" y = x |^| y

proof end;

theorem :: ROBBINS3:27

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

proof end;

registration

let L be Ortholattice;

coherence

for b_{1} being CLatAugmentation of L holds b_{1} is involutive

end;
coherence

for b

proof end;

registration

let L be Ortholattice;

coherence

for b_{1} being CLatAugmentation of L holds b_{1} is de_Morgan

end;
coherence

for b

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

( L is Orthocomplemented & L is PartialOrdered )

proof end;

theorem :: ROBBINS3:29

for L being Ortholattice

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

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

registration

let L be Ortholattice;

for b_{1} being naturally_sup-generated CLatAugmentation of L holds b_{1} is Orthocomplemented
by Th28;

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

coherence for b

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

L is Ortholattice

proof end;

registration

for b_{1} being non empty OrthoLattStr st b_{1} is Boolean & b_{1} is well-complemented & b_{1} is Lattice-like holds

( b_{1} is involutive & b_{1} is with_Top & b_{1} is de_Morgan )
by Th30;

end;

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

coherence for b

( b