:: Formalization of Ortholattices via Orthoposets
:: by Adam Grabowski and Markus Moschner
::
:: Received December 28, 2004
:: Copyright (c) 2004-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, LATTICES, SUBSET_1, EQREL_1, SHEFFER1, ROBBINS1,
OPOSET_1, QMAX_1, FUNCT_1, WAYBEL_0, XXREAL_0, LATTICE3, STRUCT_0,
ORDERS_2, BINOP_1, RELAT_1, FUNCT_5, ZFMISC_1, RELAT_2, FILTER_1,
ORDERS_1, PBOOLE, TARSKI, YELLOW_0, WAYBEL_1, ROBBINS3, CARD_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, BINOP_1, RELAT_1, RELSET_1, PARTFUN1,
RELAT_2, FUNCT_2, FUNCT_5, ORDINAL1, CARD_1, STRUCT_0, LATTICE3,
LATTICES, ORDERS_1, ORDERS_2, FILTER_1, ROBBINS1, QMAX_1, OPOSET_1,
WAYBEL_0, WAYBEL_1, YELLOW_0, SHEFFER1, PARTIT_2;
constructors BINOP_1, REALSET2, LATTICE3, WAYBEL_1, YELLOW_6, OPOSET_1,
SHEFFER1, FUNCT_5, RELSET_1, PARTIT_2;
registrations RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, STRUCT_0, LATTICES,
YELLOW_0, YELLOW_1, ROBBINS1, OPOSET_1, SHEFFER1, PARTIT_2, CARD_1;
requirements SUBSET, BOOLE;
definitions LATTICES, RELAT_2, TARSKI;
equalities LATTICES, ORDINAL1;
expansions LATTICES, RELAT_2, STRUCT_0;
theorems ZFMISC_1, STRUCT_0, LATTICE3, RELAT_1, FILTER_1, LATTICES, OPOSET_1,
ORDERS_1, ROBBINS1, PARTFUN1, RELAT_2, YELLOW_0, ORDERS_2, WAYBEL_9,
WAYBEL_1, FUNCT_2, YELLOW_7, SHEFFER1, PARTIT_2;
begin :: Another short axiomatization of lattices
:: Originally proved by McCune with the help of OTTER
definition
let L be non empty \/-SemiLattStr;
attr L is join-Associative means
for x, y, z being Element of L holds x "\/" (y "\/" z) = y "\/" (x "\/" z);
end;
definition
let L be non empty /\-SemiLattStr;
attr L is meet-Associative means
for x, y, z being Element of L holds x "/\" (y "/\" z) = y "/\" (x "/\" z);
end;
definition
let L be non empty LattStr;
attr L is meet-Absorbing means
for x, y being Element of L holds x "\/" (x "/\" y) = x;
end;
theorem Th1:
for L being non empty LattStr holds L is meet-Associative
join-Associative meet-Absorbing join-absorbing implies L is meet-idempotent
join-idempotent
proof
let L be non empty LattStr;
assume
A1: L is meet-Associative join-Associative meet-Absorbing join-absorbing;
A2: for x being Element of L holds x "\/" x = x
proof
let a be Element of L;
a = a "\/" (a "/\" a) by A1;
hence thesis by A1;
end;
for x being Element of L holds x "/\" x = x
proof
let a be Element of L;
a = a "/\" (a "\/" a) by A1;
hence thesis by A1;
end;
hence thesis by A2,ROBBINS1:def 7,SHEFFER1:def 9;
end;
theorem Th2:
for L being non empty LattStr holds L is meet-Associative
join-Associative meet-Absorbing join-absorbing implies L is meet-commutative
join-commutative
proof
let L be non empty LattStr;
assume
A1: L is meet-Associative join-Associative meet-Absorbing join-absorbing;
then
A2: L is join-idempotent 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;
a "/\" b = a "/\" (b "/\" (b "\/" a)) by A1
.= b "/\" (a "/\" (b "\/" a)) by A1
.= b "/\" (a "/\" (b "\/" (a "\/" a))) by A2,ROBBINS1:def 7
.= b "/\" (a "/\" (a "\/" (b "\/" a))) by A1
.= b "/\" a by A1;
hence thesis;
end;
for x,y being Element of L holds x "\/" y = y "\/" x
proof
let a,b be Element of L;
a "\/" b = a "\/" (b "\/" (b "/\" a)) by A1
.= b "\/" (a "\/" (b "/\" a)) by A1
.= b "\/" (a "\/" (b "/\" (a "/\" a))) by A2,SHEFFER1:def 9
.= b "\/" (a "\/" (a "/\" (b "/\" a))) by A1
.= b "\/" a by A1;
hence thesis;
end;
hence thesis by A3;
end;
theorem Th3:
for L being non empty LattStr holds L is meet-Associative
join-Associative meet-Absorbing join-absorbing implies L is meet-absorbing
proof
let L be non empty LattStr;
assume
A1: L is meet-Associative join-Associative meet-Absorbing join-absorbing;
then
A2: L is meet-commutative join-commutative by Th2;
for x,y being Element of L holds (x "/\" y) "\/" y = y
proof
let a,b be Element of L;
b = b "\/" (b "/\" a) by A1
.= b "\/" (a "/\" b) by A2
.= (a "/\" b) "\/" b by A2;
hence thesis;
end;
hence thesis;
end;
theorem Th4:
for L being non empty LattStr holds L is meet-Associative
join-Associative meet-Absorbing join-absorbing implies L is meet-associative
join-associative
proof
let L be non empty LattStr;
assume
A1: L is meet-Associative join-Associative meet-Absorbing join-absorbing;
then
A2: L is meet-commutative 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;
a "\/" (b "\/" c) = a "\/" (c "\/" b) by A2
.= c "\/" (a "\/" b) by A1
.= (a "\/" b) "\/" c by A2;
hence thesis;
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;
a "/\" (b "/\" c) = a "/\" (c "/\" b) by A2
.= c "/\" (a "/\" b) by A1
.= (a "/\" b) "/\" c by A2;
hence thesis;
end;
hence thesis by A3;
end;
theorem Th5:
for L being non empty LattStr holds L is Lattice-like iff L is
meet-Associative join-Associative meet-Absorbing join-absorbing
proof
let L be non empty LattStr;
A1: L is Lattice-like implies L is meet-Associative join-Associative
meet-Absorbing join-absorbing
proof
assume
A2: L is Lattice-like;
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;
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 thesis;
end;
A4: for x,y being Element of L holds x "\/" (x "/\" y) = x
proof
let a,b be Element of L;
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 thesis;
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;
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 thesis;
end;
hence thesis by A2,A3,A4;
end;
L is meet-Associative join-Associative meet-Absorbing join-absorbing
implies L is Lattice-like
by Th3,Th2,Th4;
hence thesis by A1;
end;
registration
cluster Lattice-like -> meet-Associative join-Associative meet-Absorbing for
non empty LattStr;
coherence by Th5;
cluster meet-Associative join-Associative meet-Absorbing join-absorbing ->
Lattice-like for non empty LattStr;
coherence by Th5;
end;
begin :: Orthoposets
registration
cluster OrderInvolutive -> Dneg for PartialOrdered non empty OrthoRelStr;
coherence
proof
let L be PartialOrdered non empty OrthoRelStr;
assume L is OrderInvolutive;
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 involutive antitone by A2,OPOSET_1:def 17;
hence thesis by A1,OPOSET_1:def 3;
end;
end;
theorem Th6:
for L being Dneg non empty OrthoRelStr, x being Element of L holds x`` = x
proof
let L be Dneg non empty OrthoRelStr, x be Element of L;
consider f being Function of L,L such that
A1: f = the Compl of L and
A2: f is involutive by OPOSET_1:def 3;
f.x = x` & f.(f.x) = x by A1,A2,PARTIT_2:def 3,ROBBINS1:def 3;
hence thesis by A1,ROBBINS1:def 3;
end;
theorem Th7:
for O being OrderInvolutive PartialOrdered non empty OrthoRelStr
, x, y being Element of O holds x <= y implies y` <= x`
proof
let O be OrderInvolutive PartialOrdered non empty OrthoRelStr, x, y be
Element of O;
assume
A1: x <= y;
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 involutive 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 thesis by A2,ROBBINS1:def 3;
end;
registration
cluster with_infima with_suprema strict for PreOrthoPoset;
existence
proof
take TrivOrthoRelStr;
thus thesis;
end;
end;
notation
let L be non empty \/-SemiLattStr, x, y be Element of L;
synonym x |_| y for x "\/" y;
end;
notation
let L be non empty /\-SemiLattStr, x, y be Element of L;
synonym x |^| y for x "/\" y;
end;
notation
let L be non empty RelStr, x, y be Element of L;
synonym x "|^|" y for x "/\" y;
synonym x "|_|" y for x "\/" y;
end;
begin :: Merging relational structures and lattice structures together
definition
struct (\/-SemiLattStr, RelStr) \/-SemiLattRelStr (# carrier -> set, L_join
-> (BinOp of the carrier), InternalRel -> Relation of the carrier #);
end;
definition
struct (/\-SemiLattStr, RelStr) /\-SemiLattRelStr (# carrier -> set, L_meet
-> (BinOp of the carrier), InternalRel -> Relation of the carrier #);
end;
definition
struct (/\-SemiLattRelStr, \/-SemiLattRelStr, LattStr) LattRelStr (# carrier
-> set, L_join, L_meet -> (BinOp of the carrier), InternalRel -> Relation of
the carrier #);
end;
definition
func TrivLattRelStr -> LattRelStr equals
LattRelStr (# {0}, op2, op2, id{0} #);
coherence;
end;
registration
cluster TrivLattRelStr -> 1-element;
coherence;
end;
registration
cluster non empty for \/-SemiLattRelStr;
existence
proof
take TrivLattRelStr;
thus thesis;
end;
cluster non empty for /\-SemiLattRelStr;
existence
proof
take TrivLattRelStr;
thus thesis;
end;
cluster non empty for LattRelStr;
existence
proof
take TrivLattRelStr;
thus thesis;
end;
end;
theorem
for R being non empty RelStr st the InternalRel of R is_reflexive_in
the carrier of R & the InternalRel of R is antisymmetric transitive holds R is
reflexive antisymmetric transitive
proof
let r be non empty RelStr;
set i = the InternalRel of r;
set c = the carrier of r;
assume that
A1: i is_reflexive_in c and
A2: i is antisymmetric transitive;
A3: i is_transitive_in field i by A2;
A4: field i = c by A1,PARTIT_2:21;
then i is_antisymmetric_in c by A2;
hence thesis by A1,A4,A3,ORDERS_2:def 2,def 3,def 4;
end;
registration
cluster TrivLattRelStr -> reflexive;
coherence
proof
set T = TrivLattRelStr;
set C = the carrier of T;
set I = the InternalRel of T;
field I = C by PARTIT_2:18;
then I is_reflexive_in C by RELAT_2:def 9;
hence thesis by ORDERS_2:def 2;
end;
end;
registration
cluster antisymmetric reflexive transitive with_suprema with_infima
for LattRelStr;
existence
proof
take TrivLattRelStr;
thus thesis;
end;
end;
registration
cluster TrivLattRelStr -> meet-Absorbing;
coherence;
end;
Lm1: TrivLattRelStr is Lattice-like;
registration
cluster Lattice-like for non empty LattRelStr;
existence by Lm1;
end;
definition
let L be Lattice;
redefine func LattRel L -> Order of the carrier of L; :: redefines LattRel (FILTER_1, definition)
coherence
proof
A1: LattRel L = { [p,q] where p is Element of L, 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 object;
assume x in LattRel L;
then ex p,q being Element of L st x = [p,q] & p [= q by A1;
hence thesis by ZFMISC_1:87;
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 object;
assume x in the carrier of L & y in the carrier of L;
then reconsider x9 = x, y9 = y as Element of L;
assume [x,y] in R & [y,x] in R;
then x9 [= y9 & y9 [= x9 by FILTER_1:31;
hence thesis by LATTICES:8;
end;
A3: R is_transitive_in the carrier of L
proof
let x,y,z be object;
assume
x in the carrier of L & y in the carrier of L & z in the carrier of L;
then reconsider x9 = x, y9 = y, z9 = z as Element of L;
assume [x,y] in R & [y,z] in R;
then x9 [= y9 & y9 [= z9 by FILTER_1:31;
then x9 [= z9 by LATTICES:7;
hence thesis by FILTER_1:31;
end;
A4: R is_reflexive_in the carrier of L
by FILTER_1:31;
then dom R = the carrier of L & field R = the carrier of L by ORDERS_1:13;
hence thesis by A4,A2,A3,PARTFUN1:def 2,RELAT_2:def 9,def 12,def 16;
end;
end;
begin :: Binary approach to ortholattices
definition
struct (LattRelStr, OrthoLattStr, OrthoRelStr) OrthoLattRelStr (# carrier ->
set, L_join, L_meet -> (BinOp of the carrier), InternalRel -> (Relation of the
carrier), Compl -> UnOp of the carrier #);
end;
definition
func TrivCLRelStr -> OrthoLattRelStr equals
OrthoLattRelStr (# {0}, op2, op2, id {0}, op1 #);
coherence;
end;
:: Axiomatics for ortholattices is the classical one for lattices extended
:: by the three following:
:: x ^ y = c(c(x) v c(y)). % DM de_Morgan from ROBBINS1
:: c(c(x)) = x. % CC involutive from OPOSET_1, too specific
:: x v c(x) = y v c(y). % ONE
definition
let L be non empty ComplStr;
attr L is involutive means
:Def6:
for x being Element of L holds x`` = x;
end;
definition
let L be non empty ComplLLattStr;
attr L is with_Top means
:Def7:
for x, y being Element of L holds x |_| x` = y |_| y`;
end;
registration
cluster TrivOrtLat -> involutive with_Top;
coherence
by STRUCT_0:def 10;
end;
registration
cluster TrivCLRelStr -> 1-element;
coherence;
end;
registration
cluster TrivCLRelStr -> reflexive;
coherence
proof
for x being Element of TrivCLRelStr holds x <= x
proof
let x be Element of TrivCLRelStr;
[x,x] in id {{}} by RELAT_1:def 10;
hence thesis by ORDERS_2:def 5;
end;
hence thesis by YELLOW_0:def 1;
end;
end;
registration
cluster TrivCLRelStr -> involutive with_Top;
coherence
by STRUCT_0:def 10;
end;
registration
cluster involutive with_Top de_Morgan Lattice-like for
1-element OrthoLattStr;
existence
proof
take TrivOrtLat;
thus thesis;
end;
end;
definition
mode Ortholattice is involutive with_Top de_Morgan Lattice-like non empty
OrthoLattStr;
end;
begin :: Lemmas
theorem Th9:
for K, L being non empty LattStr st the LattStr of K = the
LattStr of L & K is join-commutative holds L is join-commutative
proof
let K, L be non empty LattStr;
assume that
A1: the LattStr of K = the LattStr of L and
A2: K is join-commutative;
L is join-commutative
proof
let x, y be Element of L;
reconsider x9 = x, y9 = y as Element of K by A1;
x9 |_| y9 = y9 |_| x9 by A2;
hence thesis by A1;
end;
hence thesis;
end;
theorem Th10:
for K, L being non empty LattStr st the LattStr of K = the
LattStr of L & K is meet-commutative holds L is meet-commutative
proof
let K, L be non empty LattStr;
assume that
A1: the LattStr of K = the LattStr of L and
A2: K is meet-commutative;
L is meet-commutative
proof
let x, y be Element of L;
reconsider x9 = x, y9 = y as Element of K by A1;
x9 "/\" y9 = y9 "/\" x9 by A2;
hence thesis by A1;
end;
hence thesis;
end;
theorem Th11:
for K, L being non empty LattStr st the LattStr of K = the
LattStr of L & K is join-associative holds L is join-associative
proof
let K, L be non empty LattStr;
assume that
A1: the LattStr of K = the LattStr of L and
A2: K is join-associative;
L is join-associative
proof
let x, y, z be Element of L;
reconsider x9 = x, y9 = y, z9 = z as Element of K by A1;
(x9 |_| y9) |_| z9 = x9 |_| (y9 |_| z9) by A2;
hence thesis by A1;
end;
hence thesis;
end;
theorem Th12:
for K, L being non empty LattStr st the LattStr of K = the
LattStr of L & K is meet-associative holds L is meet-associative
proof
let K, L be non empty LattStr;
assume that
A1: the LattStr of K = the LattStr of L and
A2: K is meet-associative;
L is meet-associative
proof
let x, y, z be Element of L;
reconsider x9 = x, y9 = y, z9 = z as Element of K by A1;
(x9 "/\" y9) "/\" z9 = x9 "/\" (y9 "/\" z9) by A2;
hence thesis by A1;
end;
hence thesis;
end;
theorem Th13:
for K, L being non empty LattStr st the LattStr of K = the
LattStr of L & K is join-absorbing holds L is join-absorbing
proof
let K, L be non empty LattStr;
assume that
A1: the LattStr of K = the LattStr of L and
A2: K is join-absorbing;
L is join-absorbing
proof
let x, y be Element of L;
reconsider x9 = x, y9 = y as Element of K by A1;
x9 "/\" (x9 "\/" y9) = x9 by A2;
hence thesis by A1;
end;
hence thesis;
end;
theorem Th14:
for K, L being non empty LattStr st the LattStr of K = the
LattStr of L & K is meet-absorbing holds L is meet-absorbing
proof
let K, L be non empty LattStr;
assume that
A1: the LattStr of K = the LattStr of L and
A2: K is meet-absorbing;
L is meet-absorbing
proof
let x, y be Element of L;
reconsider x9 = x, y9 = y as Element of K by A1;
(x9 "/\" y9) "\/" y9 = y9 by A2;
hence thesis by A1;
end;
hence thesis;
end;
theorem
for K, L being non empty LattStr st the LattStr of K = the LattStr of
L & K is Lattice-like holds L is Lattice-like
by Th9,Th10,Th11,Th12,Th13,Th14;
theorem
for L1,L2 being non empty \/-SemiLattStr st the \/-SemiLattStr of L1 =
the \/-SemiLattStr of L2 for a1,b1 being Element of L1, a2,b2 being Element of
L2 st a1 = a2 & b1 = b2 holds a1 "\/" b1 = a2 "\/" b2;
theorem
for L1,L2 being non empty /\-SemiLattStr st the /\-SemiLattStr of L1 =
the /\-SemiLattStr of L2 for a1,b1 being Element of L1, a2,b2 being Element of
L2 st a1 = a2 & b1 = b2 holds a1 "/\" b1 = a2 "/\" b2;
theorem Th18:
for K, L being non empty ComplStr, x being Element of K, 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, x be Element of K, y be Element of L;
assume the Compl of K = the Compl of L & x = y;
then x` = (the Compl of L).y by ROBBINS1:def 3
.= y` by ROBBINS1:def 3;
hence thesis;
end;
theorem Th19:
for K, L being non empty ComplLLattStr st the ComplLLattStr of K =
the ComplLLattStr of L & K is with_Top holds L is with_Top
proof
let K, L be non empty ComplLLattStr;
assume that
A1: the ComplLLattStr of K = the ComplLLattStr of L and
A2: K is with_Top;
for x, y being Element of L holds x |_| x` = y |_| y`
proof
let x, y be Element of L;
reconsider x9 = x, y9 = y as Element of K by A1;
x |_| x` = x9 |_| x9` by A1,Th18
.= y9 |_| y9` by A2
.= y |_| y` by A1,Th18;
hence thesis;
end;
hence thesis;
end;
theorem Th20:
for K, L being non empty OrthoLattStr st the OrthoLattStr of K =
the OrthoLattStr of L & K is de_Morgan holds L is de_Morgan
proof
let K, L be non empty OrthoLattStr;
assume that
A1: the OrthoLattStr of K = the OrthoLattStr of L and
A2: K is de_Morgan;
for x, y being Element of L holds x "/\" y = (x` "\/" y`)`
proof
let x, y be Element of L;
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 thesis;
end;
hence thesis by ROBBINS1:def 23;
end;
theorem Th21:
for K, L being non empty OrthoLattStr st the OrthoLattStr of K =
the OrthoLattStr of L & K is involutive holds L is involutive
proof
let K, L be non empty OrthoLattStr;
assume that
A1: the OrthoLattStr of K = the OrthoLattStr of L and
A2: K is involutive;
for x being Element of L holds x`` = x
proof
let x be Element of L;
reconsider x9 = x as Element of K by A1;
x` = x9` by A1,Th18;
then x`` = x9`` by A1,Th18
.= x by A2;
hence thesis;
end;
hence thesis;
end;
begin :: Structure Extensions
definition
let R be RelStr;
mode RelAugmentation of R -> LattRelStr means
the RelStr of it = the RelStr of R;
existence
proof
set A = the BinOp of the carrier of R;
set L = LattRelStr (# the carrier of R, A, A, the InternalRel of R #);
take L;
thus thesis;
end;
end;
definition
let R be LattStr;
mode LatAugmentation of R -> LattRelStr means
:Def9:
the LattStr of it = the LattStr of R;
existence
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,
IR #);
take L;
thus thesis;
end;
end;
registration
let L be non empty LattStr;
cluster -> non empty for LatAugmentation of L;
coherence
proof
let R be LatAugmentation of L;
the LattStr of L = the LattStr of R by Def9;
hence thesis;
end;
end;
registration
let L be meet-associative non empty LattStr;
cluster -> meet-associative for LatAugmentation of L;
coherence
proof
let R be LatAugmentation of L;
the LattStr of L = the LattStr of R by Def9;
hence thesis by Th12;
end;
end;
registration
let L be join-associative non empty LattStr;
cluster -> join-associative for LatAugmentation of L;
coherence
proof
let R be LatAugmentation of L;
the LattStr of L = the LattStr of R by Def9;
hence thesis by Th11;
end;
end;
registration
let L be meet-commutative non empty LattStr;
cluster -> meet-commutative for LatAugmentation of L;
coherence
proof
let R be LatAugmentation of L;
the LattStr of L = the LattStr of R by Def9;
hence thesis by Th10;
end;
end;
registration
let L be join-commutative non empty LattStr;
cluster -> join-commutative for LatAugmentation of L;
coherence
proof
let R be LatAugmentation of L;
the LattStr of L = the LattStr of R by Def9;
hence thesis by Th9;
end;
end;
registration
let L be join-absorbing non empty LattStr;
cluster -> join-absorbing for LatAugmentation of L;
coherence
proof
let R be LatAugmentation of L;
the LattStr of L = the LattStr of R by Def9;
hence thesis by Th13;
end;
end;
registration
let L be meet-absorbing non empty LattStr;
cluster -> meet-absorbing for LatAugmentation of L;
coherence
proof
let R be LatAugmentation of L;
the LattStr of L = the LattStr of R by Def9;
hence thesis by Th14;
end;
end;
definition
let L be non empty \/-SemiLattRelStr;
attr L is naturally_sup-generated means
:Def10:
for x, y being Element of L holds x <= y iff x |_| y = y;
end;
definition
let L be non empty /\-SemiLattRelStr;
attr L is naturally_inf-generated means
for x, y being Element of L holds x <= y iff x |^| y = x;
end;
registration
let L be Lattice;
cluster naturally_sup-generated naturally_inf-generated Lattice-like
for LatAugmentation of L;
existence
proof
set R = LattRel L;
set S = LattRelStr (# the carrier of L, the L_join of L, the L_meet of L,
R #);
the LattStr of L = the LattStr of S;
then reconsider S 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;
reconsider x9 = x, y9 = y as Element of L;
hereby
assume x <= y;
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;
end;
A1: x9 |^| y9 = x |^| y;
assume x |^| y = x;
then x9 [= y9 by A1,LATTICES:4;
then [x9,y9] in LattRel L by FILTER_1:31;
hence thesis by ORDERS_2:def 5;
end;
then
A2: S is naturally_inf-generated;
for x, y being Element of S holds x <= y iff x |_| y = y
proof
let x, y be Element of S;
reconsider x9 = x, y9 = y as Element of L;
hereby
assume x <= 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;
hence x |_| y = y;
end;
assume x |_| y = y;
then x9 [= y9;
then [x9,y9] in LattRel L by FILTER_1:31;
hence thesis by ORDERS_2:def 5;
end;
then S is naturally_sup-generated;
hence thesis by A2;
end;
end;
registration
cluster 1-element reflexive for LattRelStr;
existence
proof
take TrivLattRelStr;
thus thesis;
end;
end;
registration
cluster 1-element reflexive for OrthoLattRelStr;
existence
proof
take TrivCLRelStr;
thus thesis;
end;
end;
registration
cluster 1-element reflexive for OrthoRelStr;
existence
proof
take TrivOrthoRelStr;
thus thesis;
end;
end;
registration
cluster -> involutive with_Top de_Morgan well-complemented
for 1-element OrthoLattStr;
coherence
proof
let L be 1-element OrthoLattStr;
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
by STRUCT_0:def 10;
( 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 thesis by A1,A2,ROBBINS1:def 10,def 23;
end;
end;
registration
cluster -> OrderInvolutive Pure PartialOrdered
for 1-element reflexive OrthoRelStr;
coherence
proof
let L be 1-element reflexive OrthoRelStr;
reconsider L9 = L as 1-element reflexive OrthoRelStr;
reconsider f = the Compl of L9 as Function of L9, L9;
consider x being object such that
A1: the carrier of L9 = {x} by ZFMISC_1:131;
f = id {x} by A1,FUNCT_2:51;
then
A2: f is involutive;
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;
assume z <= y;
f.z = x & f.y = x by A1,FUNCT_2:50;
hence thesis by YELLOW_0:def 1;
end;
then f is antitone by WAYBEL_9:def 1;
then f is Orderinvolutive by A2,OPOSET_1:def 17;
hence thesis by A3,OPOSET_1:def 15,def 18;
end;
end;
registration
cluster -> naturally_sup-generated naturally_inf-generated
for 1-element reflexive LattRelStr;
coherence
proof
let L be 1-element reflexive LattRelStr;
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 thesis;
end;
end;
registration
cluster with_infima with_suprema naturally_sup-generated
naturally_inf-generated de_Morgan Lattice-like OrderInvolutive Pure
PartialOrdered for non empty OrthoLattRelStr;
existence
proof
take TrivCLRelStr;
thus thesis;
end;
end;
registration
cluster with_infima with_suprema naturally_sup-generated
naturally_inf-generated Lattice-like for non empty LattRelStr;
existence
proof
take TrivLattRelStr;
thus thesis;
end;
end;
theorem Th22:
for L being naturally_sup-generated non empty LattRelStr, x, y
being Element of L holds x <= y iff x [= y
by Def10;
theorem Th23:
for L being naturally_sup-generated Lattice-like non empty
LattRelStr holds the RelStr of L = LattPOSet L
proof
let L be naturally_sup-generated Lattice-like non empty LattRelStr;
A1: for x, y being object holds [x,y] in the InternalRel of L iff [x,y] in
LattRel L
proof
let x, y be object;
hereby
assume
A2: [x,y] in the InternalRel of 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;
end;
assume
A3: [x,y] in LattRel 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 thesis by ORDERS_2:def 5;
end;
LattPOSet L = RelStr (#the carrier of L, LattRel L#) by LATTICE3:def 2;
hence thesis by A1,RELAT_1:def 2;
end;
registration
cluster naturally_sup-generated Lattice-like -> with_infima with_suprema for
non empty LattRelStr;
coherence
proof
let L be non empty LattRelStr;
assume L is naturally_sup-generated Lattice-like;
then reconsider L9 = L as naturally_sup-generated Lattice-like non empty
LattRelStr;
LattPOSet L9 is with_suprema with_infima;
then the RelStr of L9 is with_suprema with_infima by Th23;
hence thesis by YELLOW_7:14,15;
end;
end;
begin :: Extending OrthoLattStr
definition
let R be OrthoLattStr;
mode CLatAugmentation of R -> OrthoLattRelStr means
:Def12:
the OrthoLattStr of it = the OrthoLattStr of R;
existence
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, IR, the Compl of R #);
take L;
thus thesis;
end;
end;
registration
let L be non empty OrthoLattStr;
cluster -> non empty for CLatAugmentation of L;
coherence
proof
let R be CLatAugmentation of L;
the OrthoLattStr of L = the OrthoLattStr of R by Def12;
hence thesis;
end;
end;
registration
let L be meet-associative non empty OrthoLattStr;
cluster -> meet-associative for CLatAugmentation of L;
coherence
proof
let R be CLatAugmentation of L;
the OrthoLattStr of L = the OrthoLattStr of R by Def12;
then the LattStr of L = the LattStr of R;
hence thesis by Th12;
end;
end;
registration
let L be join-associative non empty OrthoLattStr;
cluster -> join-associative for CLatAugmentation of L;
coherence
proof
let R be CLatAugmentation of L;
the OrthoLattStr of L = the OrthoLattStr of R by Def12;
then the LattStr of L = the LattStr of R;
hence thesis by Th11;
end;
end;
registration
let L be meet-commutative non empty OrthoLattStr;
cluster -> meet-commutative for CLatAugmentation of L;
coherence
proof
let R be CLatAugmentation of L;
the OrthoLattStr of L = the OrthoLattStr of R by Def12;
then the LattStr of L = the LattStr of R;
hence thesis by Th10;
end;
end;
registration
let L be join-commutative non empty OrthoLattStr;
cluster -> join-commutative for CLatAugmentation of L;
coherence
proof
let R be CLatAugmentation of L;
the OrthoLattStr of L = the OrthoLattStr of R by Def12;
then the LattStr of L = the LattStr of R;
hence thesis by Th9;
end;
end;
registration
let L be meet-absorbing non empty OrthoLattStr;
cluster -> meet-absorbing for CLatAugmentation of L;
coherence
proof
let R be CLatAugmentation of L;
the OrthoLattStr of L = the OrthoLattStr of R by Def12;
then the LattStr of L = the LattStr of R;
hence thesis by Th14;
end;
end;
registration
let L be join-absorbing non empty OrthoLattStr;
cluster -> join-absorbing for CLatAugmentation of L;
coherence
proof
let R be CLatAugmentation of L;
the OrthoLattStr of L = the OrthoLattStr of R by Def12;
then the LattStr of L = the LattStr of R;
hence thesis by Th13;
end;
end;
registration
let L be with_Top non empty OrthoLattStr;
cluster -> with_Top for CLatAugmentation of L;
coherence
proof
let R be CLatAugmentation of L;
the OrthoLattStr of L = the OrthoLattStr of R by Def12;
then the ComplLLattStr of L = the ComplLLattStr of R;
hence thesis by Th19;
end;
end;
registration
let L be non empty Ortholattice;
cluster naturally_sup-generated naturally_inf-generated Lattice-like
for CLatAugmentation of L;
existence
proof
set R = LattRel L;
set S = OrthoLattRelStr (# the carrier of L, the L_join of L, the L_meet
of L, R, the Compl of L #);
the OrthoLattStr of L = the OrthoLattStr of S;
then reconsider S 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;
reconsider x9 = x, y9 = y as Element of L;
hereby
assume x <= y;
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;
end;
A1: x9 |^| y9 = x |^| y;
assume x |^| y = x;
then x9 [= y9 by A1,LATTICES:4;
then [x9,y9] in LattRel L by FILTER_1:31;
hence thesis by ORDERS_2:def 5;
end;
then
A2: S is naturally_inf-generated;
for x, y being Element of S holds x <= y iff x |_| y = y
proof
let x, y be Element of S;
reconsider x9 = x, y9 = y as Element of L;
hereby
assume x <= 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;
hence x |_| y = y;
end;
assume x |_| y = y;
then x9 [= y9;
then [x9,y9] in LattRel L by FILTER_1:31;
hence thesis by ORDERS_2:def 5;
end;
then S is naturally_sup-generated;
hence thesis by A2;
end;
end;
registration
cluster involutive with_Top de_Morgan Lattice-like naturally_sup-generated
well-complemented for non empty OrthoLattRelStr;
existence
proof
take TrivCLRelStr;
thus thesis;
end;
end;
theorem Th24:
for L being with_infima with_suprema PartialOrdered non empty
OrthoRelStr for x,y being Element of L holds x <= y implies y = x "|_|" y & x
= x "|^|" y
proof
let L be with_infima with_suprema PartialOrdered non empty OrthoRelStr;
let a,b be Element of L;
assume
A1: a <= b;
then b = b "|_|" a by YELLOW_0:24;
hence thesis by A1,LATTICE3:13,YELLOW_0:25;
end;
definition
let L be meet-commutative non empty /\-SemiLattStr, a, b be Element of L;
redefine func a |^| b; :: redefines |^| (ROBBINS3, synonym) → "/\" (LATTICES, definition)
commutativity by LATTICES:def 6;
end;
definition
let L be join-commutative non empty \/-SemiLattStr, a, b be Element of L;
redefine func a |_| b; :: redefines |_| (ROBBINS3, synonym) → "\/" (LATTICES, definition)
commutativity by LATTICES:def 4;
end;
registration
cluster meet-absorbing join-absorbing meet-commutative
naturally_sup-generated -> reflexive for non empty LattRelStr;
coherence
proof
let L be non empty LattRelStr;
assume L is meet-absorbing join-absorbing meet-commutative
naturally_sup-generated;
then reconsider L9 = L as meet-absorbing join-absorbing meet-commutative
naturally_sup-generated non empty LattRelStr;
for x being Element of L9 holds x <= x
proof
let x be Element of L9;
x [= x;
hence thesis by Th22;
end;
hence thesis by YELLOW_0:def 1;
end;
end;
registration
cluster join-associative naturally_sup-generated -> transitive for non empty
LattRelStr;
coherence
proof
let L be non empty LattRelStr;
assume L is join-associative naturally_sup-generated;
then reconsider
L9 = L as join-associative naturally_sup-generated non empty
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;
assume x <= y & y <= z;
then x [= y & y [= z by Th22;
then x [= z by LATTICES:7;
hence thesis by Th22;
end;
hence thesis by YELLOW_0:def 2;
end;
end;
registration
cluster join-commutative naturally_sup-generated -> antisymmetric for
non empty
LattRelStr;
coherence
proof
let L be non empty LattRelStr;
assume L is join-commutative naturally_sup-generated;
then reconsider
L9 = L as join-commutative naturally_sup-generated non empty
LattRelStr;
for x, y being Element of L9 st x <= y & y <= x holds x = y
proof
let x, y be Element of L9;
assume x <= y & y <= x;
then x [= y & y [= x by Th22;
hence thesis by LATTICES:8;
end;
hence thesis by YELLOW_0:def 3;
end;
end;
theorem Th25:
for L being with_infima with_suprema naturally_sup-generated
Lattice-like non empty OrthoLattRelStr, x, y being Element of L holds x "|_|"
y = x |_| y
proof
let L be with_infima with_suprema naturally_sup-generated Lattice-like non
empty OrthoLattRelStr, x, y be Element of L;
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
.= x "|_|" y by A2;
hence thesis by A5;
end;
theorem Th26:
for L being with_infima with_suprema naturally_sup-generated
Lattice-like non empty OrthoLattRelStr, x, y being Element of L holds x "|^|"
y = x |^| y
proof
let L be with_infima with_suprema naturally_sup-generated Lattice-like non
empty OrthoLattRelStr, x, y be Element of L;
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 thesis by A5,LATTICES:4;
end;
theorem
for L being with_infima with_suprema naturally_sup-generated
naturally_inf-generated Lattice-like OrderInvolutive PartialOrdered non empty
OrthoLattRelStr holds L is de_Morgan
proof
let L be with_infima with_suprema naturally_sup-generated
naturally_inf-generated Lattice-like OrderInvolutive PartialOrdered non empty
OrthoLattRelStr;
A1: for x,y being Element of L holds x` "|_|" y` <= ( x "|^|" y )`
proof
let a,b be Element of L;
set i = a "|^|" b;
set s = a` "|_|" b`;
i <= a by YELLOW_0:23;
then a` <= i` by Th7;
then
A2: s <= i` "|_|" b` by WAYBEL_1:2;
i <= b by YELLOW_0:23;
then b` <= i` by Th7;
then i` = b` "|_|" i` by Th24;
hence thesis by A2,LATTICE3:13;
end;
A3: for x,y being Element of L holds ( x "|_|" y )` <= x` "|^|" y`
proof
let a,b be Element of L;
set i = a` "|^|" b`;
set s = a "|_|" b;
a <= s by YELLOW_0:22;
then s` <= a` by Th7;
then
A4: s` "|^|" b` <= i by WAYBEL_1:1;
b <= s by YELLOW_0:22;
then s` <= b` by Th7;
hence thesis by A4,Th24;
end;
for x,y being Element of L holds (x` |_| y`)` = x |^| y
proof
let a,b be Element of L;
set s = a` "|_|" b`;
set i = a "|^|" b;
a`` = a & b`` = b by Th6;
then
A5: s` <= i by A3;
i`` <= s` by A1,Th7;
then
A6: i <= s` by Th6;
i = a |^| b & s = a` |_| b` by Th25,Th26;
hence thesis by A5,A6,ORDERS_2:2;
end;
hence thesis by ROBBINS1:def 23;
end;
registration
let L be Ortholattice;
cluster -> involutive for CLatAugmentation of L;
coherence
proof
let R be CLatAugmentation of L;
the OrthoLattStr of L = the OrthoLattStr of R by Def12;
hence thesis by Th21;
end;
end;
registration
let L be Ortholattice;
cluster -> de_Morgan for CLatAugmentation of L;
coherence
proof
let R be CLatAugmentation of L;
the OrthoLattStr of L = the OrthoLattStr of R by Def12;
hence thesis by Th20;
end;
end;
theorem Th28:
for L being non empty OrthoLattRelStr st L is involutive
with_Top de_Morgan Lattice-like naturally_sup-generated holds L is
Orthocomplemented PartialOrdered
proof
let L be non empty OrthoLattRelStr;
assume
L is involutive with_Top de_Morgan Lattice-like naturally_sup-generated;
then reconsider L9 = L as involutive with_Top de_Morgan Lattice-like
naturally_sup-generated non empty 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;
assume x <= 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 thesis by A1,Def10;
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;
thus ex_sup_of {y,f.y},L9 by YELLOW_0:20;
thus ex_inf_of {y,f.y},L9 by YELLOW_0:21;
set t = y |_| y`;
for b being Element of L9 st b in the carrier of L9 holds b <= t
proof
let b be Element of L9;
assume b in the carrier of L9;
b |_| (y |_| y`) = b |_| (b |_| b`) by Def7
.= b |_| b |_| b` by LATTICES:def 5
.= b |_| b`
.= y |_| y` by Def7;
then b [= t;
hence thesis by Th22;
end;
then
A4: t 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 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
.= xx 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
;
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;
a |^| a` = (a` |_| a``)` by ROBBINS1:def 23
.= (b` |_| b``)` by Def7
.= b |^| b` by ROBBINS1:def 23;
hence thesis;
end;
for b being Element of L9 st b in the carrier of L9 holds b >= t
proof
let b be Element of L9;
assume b in the carrier of L9;
b |^| (y |^| y`) = b |^| (b |^| b`) by A7
.= b |^| b |^| b` by LATTICES:def 7
.= b |^| b`
.= y |^| y` by A7;
then t [= b by LATTICES:4;
hence thesis by Th22;
end;
then
A8: t 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 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
.= xx by A8,A9,A10,YELLOW_0:def 10;
hence thesis by A9,WAYBEL_1:def 6;
end;
for x being Element of L9 holds f.(f.x) = x
proof
let x be Element of L9;
f.(f.x) = f.(x`) by ROBBINS1:def 3
.= x`` by ROBBINS1:def 3
.= x by Def6;
hence thesis;
end;
then f is involutive 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 thesis by OPOSET_1:def 22;
end;
theorem
for L being Ortholattice, E being naturally_sup-generated
CLatAugmentation of L holds E is Orthocomplemented by Th28;
registration
let L be Ortholattice;
cluster -> Orthocomplemented for
naturally_sup-generated CLatAugmentation of L;
coherence by Th28;
end;
theorem Th30:
for L being non empty OrthoLattStr st L is Boolean
well-complemented Lattice-like holds L is Ortholattice
proof
let L be non empty OrthoLattStr;
assume L is Boolean well-complemented Lattice-like;
then reconsider L9 = L as Boolean well-complemented Lattice-like non empty
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,4;
hence thesis by A1,Def6,Def7,ROBBINS1:def 23;
end;
registration
cluster Boolean well-complemented Lattice-like -> involutive with_Top
de_Morgan for non empty OrthoLattStr;
coherence by Th30;
end;