:: ROBBINS1 semantic presentation

definition

attr a₁ is strict;
struct ComplStr -> 1-sorted ;
aggr ComplStr(# carrier, Compl #) -> ComplStr ;
sel Compl c₁ -> UnOp of the carrier of a₁;

end;

definition

attr a₁ is strict;
struct ComplLattStr -> \/-SemiLattStr , ComplStr ;
aggr ComplLattStr(# carrier, L_join, Compl #) -> ComplLattStr ;

end;

definition

attr a₁ is strict;
struct OrthoLattStr -> ComplLattStr , LattStr ;
aggr OrthoLattStr(# carrier, L_join, L_meet, Compl #) -> OrthoLattStr ;

end;

definition

func TrivComplLat -> strict ComplLattStr equals :: ROBBINS1:def 1
ComplLattStr(# {{} },op2 ,op1 #);
coherence ;

end;

:: deftheorem Def1 defines TrivComplLat ROBBINS1:def 1 :

definition

func TrivOrtLat -> strict OrthoLattStr equals :: ROBBINS1:def 2
OrthoLattStr(# {{} },op2 ,op2 ,op1 #);
coherence ;

end;

:: deftheorem Def2 defines TrivOrtLat ROBBINS1:def 2 :

registration

cluster TrivComplLat -> non empty trivial strict ;
coherence by REALSET2:def 5, STRUCT_0:def 1;
cluster TrivOrtLat -> non empty trivial strict ;
coherence by REALSET2:def 5, STRUCT_0:def 1;

end;

registration

cluster non empty trivial strict OrthoLattStr ;
existence

proof end;

cluster non empty trivial strict ComplLattStr ;
existence

proof end;

end;

registration

let c₁ be non empty trivial ComplLattStr ;
cluster ComplStr(# the carrier of a₁,the Compl of a₁ #) -> non empty trivial ;
coherence

proof end;

end;

registration

cluster non empty trivial strict ComplStr ;
existence

proof end;

end;

definition

let c₁ be non empty ComplStr ;
let c₂ be Element of c₁;
func c₂ ` -> Element of a₁ equals :: ROBBINS1:def 3
the Compl of a₁ . a₂;
coherence ;

end;

:: deftheorem Def3 defines ` ROBBINS1:def 3 :

notation

let c₁ be non empty ComplLattStr ;
let c₂, c₃ be Element of c₁;
synonym c₂ + c₃ for c₂ "\/" c₃;

end;

definition

let c₁ be non empty ComplLattStr ;
let c₂, c₃ be Element of c₁;
func c₂ *' c₃ -> Element of a₁ equals :: ROBBINS1:def 4
((a₂ ` ) "\/" (a₃ ` )) ` ;
coherence ;

end;

:: deftheorem Def4 defines *' ROBBINS1:def 4 :

definition

let c₁ be non empty ComplLattStr ;
attr a₁ is Robbins means :Def5: :: ROBBINS1:def 5
for b₁, b₂ being Element of a₁ holds (((b₁ + b₂) ` ) + ((b₁ + (b₂ ` )) ` )) ` = b₁;
attr a₁ is Huntington means :Def6: :: ROBBINS1:def 6
for b₁, b₂ being Element of a₁ holds (((b₁ ` ) + (b₂ ` )) ` ) + (((b₁ ` ) + b₂) ` ) = b₁;

end;

:: deftheorem Def5 defines Robbins ROBBINS1:def 5 :

:: deftheorem Def6 defines Huntington ROBBINS1:def 6 :

definition

let c₁ be non empty \/-SemiLattStr ;
attr a₁ is join-idempotent means :Def7: :: ROBBINS1:def 7
for b₁ being Element of a₁ holds b₁ "\/" b₁ = b₁;

end;

:: deftheorem Def7 defines join-idempotent ROBBINS1:def 7 :

registration

cluster TrivComplLat -> non empty join-commutative join-associative trivial strict Robbins Huntington join-idempotent ;
coherence

proof end;

cluster TrivOrtLat -> non empty join-commutative join-associative trivial strict Robbins Huntington ;
coherence

proof end;

end;

registration end;

registration

cluster non empty join-commutative join-associative strict Robbins Huntington join-idempotent ComplLattStr ;
existence

proof end;

end;

registration

cluster non empty Lattice-like strict Robbins Huntington OrthoLattStr ;
existence

proof end;

end;

definition

let c₁ be non empty join-commutative ComplLattStr ;
let c₂, c₃ be Element of c₁;
redefine func + as c₂ + c₃ -> M2(the carrier of a₁);
commutativity by LATTICES:def 4;

end;

theorem Th1: :: ROBBINS1:1

for b₁ being non empty join-commutative join-associative Huntington ComplLattStr
for b₂, b₃ being Element of b₁ holds (b₂ *' b₃) + (b₂ *' (b₃ ` )) = b₂ by Def6;

theorem Th2: :: ROBBINS1:2

for b₁ being non empty join-commutative join-associative Huntington ComplLattStr
for b₂ being Element of b₁ holds b₂ + (b₂ ` ) = (b₂ ` ) + ((b₂ ` ) ` )

proof end;

theorem Th3: :: ROBBINS1:3

for b₁ being non empty join-commutative join-associative Huntington ComplLattStr
for b₂ being Element of b₁ holds (b₂ ` ) ` = b₂

proof end;

theorem Th4: :: ROBBINS1:4

for b₁ being non empty join-commutative join-associative Huntington ComplLattStr
for b₂, b₃ being Element of b₁ holds b₂ + (b₂ ` ) = b₃ + (b₃ ` )

proof end;

theorem Th5: :: ROBBINS1:5

for b₁ being non empty join-commutative join-associative Huntington join-idempotent ComplLattStr ex b₂ being Element of b₁ st
for b₃ being Element of b₁ holds
( b₂ + b₃ = b₂ & b₃ + (b₃ ` ) = b₂ )

proof end;

theorem Th6: :: ROBBINS1:6

for b₁ being non empty join-commutative join-associative Huntington join-idempotent ComplLattStr holds b₁ is upper-bounded

proof end;

registration

cluster non empty join-commutative join-associative Huntington join-idempotent -> non empty upper-bounded ComplLattStr ;
coherence by Th6;

end;

definition

let c₁ be non empty join-commutative join-associative Huntington join-idempotent ComplLattStr ;
redefine func Top c₁ -> M2(the carrier of a₁) means :Def8: :: ROBBINS1:def 8
ex b₁ being Element of a₁ st a₂ = b₁ + (b₁ ` );
compatibility

proof end;

end;

:: deftheorem Def8 defines Top ROBBINS1:def 8 :

theorem Th7: :: ROBBINS1:7

for b₁ being non empty join-commutative join-associative Huntington join-idempotent ComplLattStr ex b₂ being Element of b₁ st
for b₃ being Element of b₁ holds
( b₂ *' b₃ = b₂ & (b₃ + (b₃ ` )) ` = b₂ )

proof end;

theorem Th8: :: ROBBINS1:8

for b₁ being non empty join-commutative join-associative ComplLattStr
for b₂, b₃ being Element of b₁ holds b₂ *' b₃ = b₃ *' b₂

proof end;

definition

let c₁ be non empty join-commutative join-associative ComplLattStr ;
let c₂, c₃ be Element of c₁;
redefine func *' as c₂ *' c₃ -> Element of a₁;
commutativity by Th8;

end;

definition

let c₁ be non empty join-commutative join-associative Huntington join-idempotent ComplLattStr ;
func Bot c₁ -> Element of a₁ means :Def9: :: ROBBINS1:def 9
for b₁ being Element of a₁ holds a₂ *' b₁ = a₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines Bot ROBBINS1:def 9 :

theorem Th9: :: ROBBINS1:9

for b₁ being non empty join-commutative join-associative Huntington join-idempotent ComplLattStr
for b₂ being Element of b₁ holds Bot b₁ = (b₂ + (b₂ ` )) `

proof end;

theorem Th10: :: ROBBINS1:10

for b₁ being non empty join-commutative join-associative Huntington join-idempotent ComplLattStr holds
( (Top b₁) ` = Bot b₁ & Top b₁ = (Bot b₁) ` )

proof end;

theorem Th11: :: ROBBINS1:11

for b₁ being non empty join-commutative join-associative Huntington ComplLattStr
for b₂, b₃ being Element of b₁ st b₂ ` = b₃ ` holds
b₂ = b₃

proof end;

theorem Th12: :: ROBBINS1:12

for b₁ being non empty join-commutative join-associative Huntington ComplLattStr
for b₂, b₃ being Element of b₁ holds b₂ + ((b₃ + (b₃ ` )) ` ) = b₂

proof end;

theorem Th13: :: ROBBINS1:13

for b₁ being non empty join-commutative join-associative Huntington ComplLattStr
for b₂ being Element of b₁ holds b₂ + b₂ = b₂

proof end;

registration

cluster non empty join-commutative join-associative Huntington -> non empty join-idempotent ComplLattStr ;
coherence

proof end;

end;

theorem Th14: :: ROBBINS1:14

for b₁ being non empty join-commutative join-associative Huntington ComplLattStr
for b₂ being Element of b₁ holds b₂ + (Bot b₁) = b₂

proof end;

theorem Th15: :: ROBBINS1:15

for b₁ being non empty join-commutative join-associative Huntington ComplLattStr
for b₂ being Element of b₁ holds b₂ *' (Top b₁) = b₂

proof end;

theorem Th16: :: ROBBINS1:16

for b₁ being non empty join-commutative join-associative Huntington ComplLattStr
for b₂ being Element of b₁ holds b₂ *' (b₂ ` ) = Bot b₁

proof end;

theorem Th17: :: ROBBINS1:17

for b₁ being non empty join-commutative join-associative Huntington ComplLattStr
for b₂, b₃, b₄ being Element of b₁ holds b₂ *' (b₃ *' b₄) = (b₂ *' b₃) *' b₄

proof end;

theorem Th18: :: ROBBINS1:18

for b₁ being non empty join-commutative join-associative Huntington ComplLattStr
for b₂, b₃ being Element of b₁ holds b₂ + b₃ = ((b₂ ` ) *' (b₃ ` )) `

proof end;

theorem Th19: :: ROBBINS1:19

for b₁ being non empty join-commutative join-associative Huntington ComplLattStr
for b₂ being Element of b₁ holds b₂ *' b₂ = b₂

proof end;

theorem Th20: :: ROBBINS1:20

for b₁ being non empty join-commutative join-associative Huntington ComplLattStr
for b₂ being Element of b₁ holds b₂ + (Top b₁) = Top b₁

proof end;

theorem Th21: :: ROBBINS1:21

for b₁ being non empty join-commutative join-associative Huntington ComplLattStr
for b₂, b₃ being Element of b₁ holds b₂ + (b₂ *' b₃) = b₂

proof end;

theorem Th22: :: ROBBINS1:22

for b₁ being non empty join-commutative join-associative Huntington ComplLattStr
for b₂, b₃ being Element of b₁ holds b₂ *' (b₂ + b₃) = b₂

proof end;

theorem Th23: :: ROBBINS1:23

for b₁ being non empty join-commutative join-associative Huntington ComplLattStr
for b₂, b₃ being Element of b₁ st (b₂ ` ) + b₃ = Top b₁ & (b₃ ` ) + b₂ = Top b₁ holds
b₂ = b₃

proof end;

theorem Th24: :: ROBBINS1:24

for b₁ being non empty join-commutative join-associative Huntington ComplLattStr
for b₂, b₃ being Element of b₁ st b₂ + b₃ = Top b₁ & b₂ *' b₃ = Bot b₁ holds
b₂ ` = b₃

proof end;

theorem Th25: :: ROBBINS1:25

for b₁ being non empty join-commutative join-associative Huntington ComplLattStr
for b₂, b₃, b₄ being Element of b₁ holds ((((((((b₂ *' b₃) *' b₄) + ((b₂ *' b₃) *' (b₄ ` ))) + ((b₂ *' (b₃ ` )) *' b₄)) + ((b₂ *' (b₃ ` )) *' (b₄ ` ))) + (((b₂ ` ) *' b₃) *' b₄)) + (((b₂ ` ) *' b₃) *' (b₄ ` ))) + (((b₂ ` ) *' (b₃ ` )) *' b₄)) + (((b₂ ` ) *' (b₃ ` )) *' (b₄ ` )) = Top b₁

proof end;

theorem Th26: :: ROBBINS1:26

for b₁ being non empty join-commutative join-associative Huntington ComplLattStr
for b₂, b₃, b₄ being Element of b₁ holds
( (b₂ *' b₄) *' (b₃ *' (b₄ ` )) = Bot b₁ & ((b₂ *' b₃) *' b₄) *' (((b₂ ` ) *' b₃) *' b₄) = Bot b₁ & ((b₂ *' (b₃ ` )) *' b₄) *' (((b₂ ` ) *' b₃) *' b₄) = Bot b₁ & ((b₂ *' b₃) *' b₄) *' (((b₂ ` ) *' (b₃ ` )) *' b₄) = Bot b₁ & ((b₂ *' b₃) *' (b₄ ` )) *' (((b₂ ` ) *' (b₃ ` )) *' (b₄ ` )) = Bot b₁ & ((b₂ *' (b₃ ` )) *' b₄) *' (((b₂ ` ) *' b₃) *' b₄) = Bot b₁ )

proof end;

theorem Th27: :: ROBBINS1:27

for b₁ being non empty join-commutative join-associative Huntington ComplLattStr
for b₂, b₃, b₄ being Element of b₁ holds (b₂ *' b₃) + (b₂ *' b₄) = (((b₂ *' b₃) *' b₄) + ((b₂ *' b₃) *' (b₄ ` ))) + ((b₂ *' (b₃ ` )) *' b₄)

proof end;

theorem Th28: :: ROBBINS1:28

for b₁ being non empty join-commutative join-associative Huntington ComplLattStr
for b₂, b₃, b₄ being Element of b₁ holds (b₂ *' (b₃ + b₄)) ` = (((((b₂ *' (b₃ ` )) *' (b₄ ` )) + (((b₂ ` ) *' b₃) *' b₄)) + (((b₂ ` ) *' b₃) *' (b₄ ` ))) + (((b₂ ` ) *' (b₃ ` )) *' b₄)) + (((b₂ ` ) *' (b₃ ` )) *' (b₄ ` ))

proof end;

theorem Th29: :: ROBBINS1:29

for b₁ being non empty join-commutative join-associative Huntington ComplLattStr
for b₂, b₃, b₄ being Element of b₁ holds ((b₂ *' b₃) + (b₂ *' b₄)) + ((b₂ *' (b₃ + b₄)) ` ) = Top b₁

proof end;

theorem Th30: :: ROBBINS1:30

for b₁ being non empty join-commutative join-associative Huntington ComplLattStr
for b₂, b₃, b₄ being Element of b₁ holds ((b₂ *' b₃) + (b₂ *' b₄)) *' ((b₂ *' (b₃ + b₄)) ` ) = Bot b₁

proof end;

theorem Th31: :: ROBBINS1:31

for b₁ being non empty join-commutative join-associative Huntington ComplLattStr
for b₂, b₃, b₄ being Element of b₁ holds b₂ *' (b₃ + b₄) = (b₂ *' b₃) + (b₂ *' b₄)

proof end;

theorem Th32: :: ROBBINS1:32

for b₁ being non empty join-commutative join-associative Huntington ComplLattStr
for b₂, b₃, b₄ being Element of b₁ holds b₂ + (b₃ *' b₄) = (b₂ + b₃) *' (b₂ + b₄)

proof end;

definition

let c₁ be non empty OrthoLattStr ;
attr a₁ is well-complemented means :Def10: :: ROBBINS1:def 10
for b₁ being Element of a₁ holds b₁ ` is_a_complement_of b₁;

end;

:: deftheorem Def10 defines well-complemented ROBBINS1:def 10 :

registration end;

definition

mode preOrthoLattice is non empty Lattice-like OrthoLattStr ;

end;

registration

cluster Boolean strict well-complemented OrthoLattStr ;
existence

proof end;

end;

theorem Th33: :: ROBBINS1:33

for b₁ being distributive well-complemented preOrthoLattice
for b₂ being Element of b₁ holds (b₂ ` ) ` = b₂

proof end;

theorem Th34: :: ROBBINS1:34

for b₁ being distributive bounded well-complemented preOrthoLattice
for b₂, b₃ being Element of b₁ holds b₂ "/\" b₃ = ((b₂ ` ) "\/" (b₃ ` )) `

proof end;

definition

let c₁ be non empty ComplLattStr ;
func CLatt c₁ -> strict OrthoLattStr means :Def11: :: ROBBINS1:def 11
( the carrier of a₂ = the carrier of a₁ & the L_join of a₂ = the L_join of a₁ & the Compl of a₂ = the Compl of a₁ & ( for b₁, b₂ being Element of a₁ holds the L_meet of a₂ . b₁,b₂ = b₁ *' b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines CLatt ROBBINS1:def 11 :

registration

let c₁ be non empty ComplLattStr ;
cluster CLatt a₁ -> non empty strict ;
coherence

proof end;

end;

registration

let c₁ be non empty join-commutative ComplLattStr ;
cluster CLatt a₁ -> non empty join-commutative strict ;
coherence

proof end;

end;

registration

let c₁ be non empty join-associative ComplLattStr ;
cluster CLatt a₁ -> non empty join-associative strict ;
coherence

proof end;

end;

registration

let c₁ be non empty join-commutative join-associative ComplLattStr ;
cluster CLatt a₁ -> non empty join-commutative join-associative meet-commutative strict ;
coherence

proof end;

end;

theorem Th35: :: ROBBINS1:35

for b₁ being non empty ComplLattStr
for b₂, b₃ being Element of b₁
for b₄, b₅ being Element of (CLatt b₁) st b₂ = b₄ & b₃ = b₅ holds
( b₂ *' b₃ = b₄ "/\" b₅ & b₂ + b₃ = b₄ "\/" b₅ & b₂ ` = b₄ ` ) by Def11;

registration

let c₁ be non empty join-commutative join-associative Huntington ComplLattStr ;
cluster CLatt a₁ -> non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing strict ;
coherence

proof end;

end;

registration

let c₁ be non empty Huntington ComplLattStr ;
cluster CLatt a₁ -> non empty strict Huntington ;
coherence

proof end;

end;

registration

proof end;

end;

theorem Th36: :: ROBBINS1:36

for b₁ being non empty join-commutative join-associative Huntington ComplLattStr holds Bot b₁ = Bottom (CLatt b₁)

proof end;

registration

proof end;

end;

notation

let c₁ be non empty ComplLattStr ;
let c₂ be Element of c₁;
synonym - c₂ for c₂ ` ;

end;

definition

let c₁ be non empty join-commutative ComplLattStr ;
redefine attr a₁ is Huntington means :Def12: :: ROBBINS1:def 12
for b₁, b₂ being Element of a₁ holds (- ((- b₁) + (- b₂))) + (- (b₁ + (- b₂))) = b₂;
compatibility

proof end;

end;

:: deftheorem Def12 defines Huntington ROBBINS1:def 12 :

definition

let c₁ be non empty ComplLattStr ;
attr a₁ is with_idempotent_element means :Def13: :: ROBBINS1:def 13
ex b₁ being Element of a₁ st b₁ + b₁ = b₁;
correctness ;

end;

:: deftheorem Def13 defines with_idempotent_element ROBBINS1:def 13 :

definition

let c₁ be non empty ComplLattStr ;
let c₂, c₃ be Element of c₁;
func \delta c₂,c₃ -> Element of a₁ equals :: ROBBINS1:def 14
- ((- a₂) + a₃);
coherence ;

end;

:: deftheorem Def14 defines \delta ROBBINS1:def 14 :

definition

let c₁ be non empty ComplLattStr ;
let c₂, c₃ be Element of c₁;
func Expand c₂,c₃ -> Element of a₁ equals :: ROBBINS1:def 15
\delta (a₂ + a₃),(\delta a₂,a₃);
coherence ;

end;

:: deftheorem Def15 defines Expand ROBBINS1:def 15 :

definition

let c₁ be non empty ComplLattStr ;
let c₂ be Element of c₁;
func c₂ _0 -> Element of a₁ equals :: ROBBINS1:def 16
- ((- a₂) + a₂);
coherence ;
func Double c₂ -> Element of a₁ equals :: ROBBINS1:def 17
a₂ + a₂;
coherence ;

end;

:: deftheorem Def16 defines _0 ROBBINS1:def 16 :

:: deftheorem Def17 defines Double ROBBINS1:def 17 :

definition

let c₁ be non empty ComplLattStr ;
let c₂ be Element of c₁;
func c₂ _1 -> Element of a₁ equals :: ROBBINS1:def 18
(a₂ _0 ) + a₂;
coherence ;
func c₂ _2 -> Element of a₁ equals :: ROBBINS1:def 19
(a₂ _0 ) + (Double a₂);
coherence ;
func c₂ _3 -> Element of a₁ equals :: ROBBINS1:def 20
(a₂ _0 ) + ((Double a₂) + a₂);
coherence ;
func c₂ _4 -> Element of a₁ equals :: ROBBINS1:def 21
(a₂ _0 ) + ((Double a₂) + (Double a₂));
coherence ;

end;

:: deftheorem Def18 defines _1 ROBBINS1:def 18 :

:: deftheorem Def19 defines _2 ROBBINS1:def 19 :

:: deftheorem Def20 defines _3 ROBBINS1:def 20 :

:: deftheorem Def21 defines _4 ROBBINS1:def 21 :

theorem Th37: :: ROBBINS1:37

for b₁ being non empty join-commutative join-associative Robbins ComplLattStr
for b₂, b₃ being Element of b₁ holds \delta (b₂ + b₃),(\delta b₂,b₃) = b₃

proof end;

theorem Th38: :: ROBBINS1:38

for b₁ being non empty join-commutative join-associative Robbins ComplLattStr
for b₂, b₃ being Element of b₁ holds Expand b₂,b₃ = b₃ by Th37;

theorem Th39: :: ROBBINS1:39

for b₁ being non empty join-commutative join-associative Robbins ComplLattStr
for b₂, b₃, b₄ being Element of b₁ holds \delta ((- b₂) + b₃),b₄ = - ((\delta b₂,b₃) + b₄) ;

theorem Th40: :: ROBBINS1:40

for b₁ being non empty join-commutative join-associative Robbins ComplLattStr
for b₂ being Element of b₁ holds \delta b₂,b₂ = b₂ _0 ;

theorem Th41: :: ROBBINS1:41

for b₁ being non empty join-commutative join-associative Robbins ComplLattStr
for b₂ being Element of b₁ holds \delta (Double b₂),(b₂ _0 ) = b₂

proof end;

theorem Th42: :: ROBBINS1:42

for b₁ being non empty join-commutative join-associative Robbins ComplLattStr
for b₂ being Element of b₁ holds \delta (b₂ _2 ),b₂ = b₂ _0

proof end;

theorem Th43: :: ROBBINS1:43

for b₁ being non empty join-commutative join-associative Robbins ComplLattStr
for b₂ being Element of b₁ holds (b₂ _2 ) + b₂ = b₂ _3 by LATTICES:def 5;

theorem Th44: :: ROBBINS1:44

for b₁ being non empty join-commutative join-associative Robbins ComplLattStr
for b₂ being Element of b₁ holds (b₂ _4 ) + (b₂ _0 ) = (b₂ _3 ) + (b₂ _1 )

proof end;

theorem Th45: :: ROBBINS1:45

for b₁ being non empty join-commutative join-associative Robbins ComplLattStr
for b₂ being Element of b₁ holds (b₂ _3 ) + (b₂ _0 ) = (b₂ _2 ) + (b₂ _1 )

proof end;

theorem Th46: :: ROBBINS1:46

for b₁ being non empty join-commutative join-associative Robbins ComplLattStr
for b₂ being Element of b₁ holds (b₂ _3 ) + b₂ = b₂ _4

proof end;

theorem Th47: :: ROBBINS1:47

for b₁ being non empty join-commutative join-associative Robbins ComplLattStr
for b₂ being Element of b₁ holds \delta (b₂ _3 ),(b₂ _0 ) = b₂

proof end;

theorem Th48: :: ROBBINS1:48

for b₁ being non empty join-commutative join-associative Robbins ComplLattStr
for b₂, b₃, b₄ being Element of b₁ st - b₂ = - b₃ holds
\delta b₂,b₄ = \delta b₃,b₄ ;

theorem Th49: :: ROBBINS1:49

for b₁ being non empty join-commutative join-associative Robbins ComplLattStr
for b₂, b₃ being Element of b₁ holds \delta b₂,(- b₃) = \delta b₃,(- b₂)

proof end;

theorem Th50: :: ROBBINS1:50

for b₁ being non empty join-commutative join-associative Robbins ComplLattStr
for b₂ being Element of b₁ holds \delta (b₂ _3 ),b₂ = b₂ _0

proof end;

theorem Th51: :: ROBBINS1:51

for b₁ being non empty join-commutative join-associative Robbins ComplLattStr
for b₂ being Element of b₁ holds \delta ((b₂ _1 ) + (b₂ _3 )),b₂ = b₂ _0

proof end;

theorem Th52: :: ROBBINS1:52

for b₁ being non empty join-commutative join-associative Robbins ComplLattStr
for b₂ being Element of b₁ holds \delta ((b₂ _1 ) + (b₂ _2 )),b₂ = b₂ _0

proof end;

theorem Th53: :: ROBBINS1:53

for b₁ being non empty join-commutative join-associative Robbins ComplLattStr
for b₂ being Element of b₁ holds \delta ((b₂ _1 ) + (b₂ _3 )),(b₂ _0 ) = b₂

proof end;

definition

let c₁ be non empty join-commutative join-associative Robbins ComplLattStr ;
let c₂ be Element of c₁;
func \beta c₂ -> Element of a₁ equals :: ROBBINS1:def 22
((- ((a₂ _1 ) + (a₂ _3 ))) + a₂) + (- (a₂ _3 ));
coherence ;

end;

:: deftheorem Def22 defines \beta ROBBINS1:def 22 :

theorem Th54: :: ROBBINS1:54

for b₁ being non empty join-commutative join-associative Robbins ComplLattStr
for b₂ being Element of b₁ holds \delta (\beta b₂),b₂ = - (b₂ _3 )

proof end;

theorem Th55: :: ROBBINS1:55

for b₁ being non empty join-commutative join-associative Robbins ComplLattStr
for b₂ being Element of b₁ holds \delta (\beta b₂),b₂ = - ((b₂ _1 ) + (b₂ _3 ))

proof end;

theorem Th56: :: ROBBINS1:56

for b₁ being non empty join-commutative join-associative Robbins ComplLattStr ex b₂, b₃ being Element of b₁ st - (b₂ + b₃) = - b₃

proof end;

theorem Th57: :: ROBBINS1:57

for b₁ being non empty join-commutative join-associative Robbins ComplLattStr st ( for b₂ being Element of b₁ holds - (- b₂) = b₂ ) holds
b₁ is Huntington

proof end;

theorem Th58: :: ROBBINS1:58

for b₁ being non empty join-commutative join-associative Robbins ComplLattStr st b₁ is with_idempotent_element holds
b₁ is Huntington

proof end;

registration

cluster TrivComplLat -> non empty join-commutative join-associative upper-bounded trivial strict Robbins Huntington join-idempotent with_idempotent_element ;
coherence

proof end;

end;

registration

cluster non empty join-commutative join-associative Robbins with_idempotent_element -> non empty join-commutative join-associative upper-bounded Robbins Huntington join-idempotent ComplLattStr ;
coherence by Th58;

end;

theorem Th59: :: ROBBINS1:59

for b₁ being non empty join-commutative join-associative Robbins ComplLattStr st ex b₂, b₃ being Element of b₁ st b₂ + b₃ = b₂ holds
b₁ is Huntington

proof end;

theorem Th60: :: ROBBINS1:60

for b₁ being non empty join-commutative join-associative Robbins ComplLattStr ex b₂, b₃ being Element of b₁ st b₂ + b₃ = b₃

proof end;

registration

cluster non empty join-commutative join-associative Robbins -> non empty join-commutative join-associative upper-bounded Huntington join-idempotent ComplLattStr ;
coherence

proof end;

end;

definition

let c₁ be non empty OrthoLattStr ;
attr a₁ is de_Morgan means :Def23: :: ROBBINS1:def 23
for b₁, b₂ being Element of a₁ holds b₁ "/\" b₂ = ((b₁ ` ) "\/" (b₂ ` )) ` ;

end;