:: by Adam Grabowski

::

:: Received June 12, 2001

:: Copyright (c) 2001-2012 Association of Mizar Users

begin

definition

attr c_{1} is strict ;

struct ComplStr -> 1-sorted ;

aggr ComplStr(# carrier, Compl #) -> ComplStr ;

sel Compl c_{1} -> UnOp of the carrier of c_{1};

end;
struct ComplStr -> 1-sorted ;

aggr ComplStr(# carrier, Compl #) -> ComplStr ;

sel Compl c

definition

attr c_{1} is strict ;

struct ComplLLattStr -> \/-SemiLattStr , ComplStr ;

aggr ComplLLattStr(# carrier, L_join, Compl #) -> ComplLLattStr ;

end;
struct ComplLLattStr -> \/-SemiLattStr , ComplStr ;

aggr ComplLLattStr(# carrier, L_join, Compl #) -> ComplLLattStr ;

definition

attr c_{1} is strict ;

struct ComplULattStr -> /\-SemiLattStr , ComplStr ;

aggr ComplULattStr(# carrier, L_meet, Compl #) -> ComplULattStr ;

end;
struct ComplULattStr -> /\-SemiLattStr , ComplStr ;

aggr ComplULattStr(# carrier, L_meet, Compl #) -> ComplULattStr ;

definition

attr c_{1} is strict ;

struct OrthoLattStr -> ComplLLattStr , LattStr ;

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

end;
struct OrthoLattStr -> ComplLLattStr , LattStr ;

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

registration
end;

registration

existence

ex b_{1} being OrthoLattStr st

( b_{1} is strict & b_{1} is 1 -element )

ex b_{1} being ComplLLattStr st

( b_{1} is strict & b_{1} is 1 -element )

end;
ex b

( b

proof end;

existence ex b

( b

proof end;

registration

let L be 1 -element ComplLLattStr ;

coherence

ComplStr(# the carrier of L, the Compl of L #) is 1 -element

end;
coherence

ComplStr(# the carrier of L, the Compl of L #) is 1 -element

proof end;

registration
end;

definition
end;

:: deftheorem defines ` ROBBINS1:def 3 :

for L being non empty ComplStr

for x being Element of L holds x ` = the Compl of L . x;

for L being non empty ComplStr

for x being Element of L holds x ` = the Compl of L . x;

notation
end;

definition

let L be non empty ComplLLattStr ;

let x, y be Element of L;

coherence

((x `) "\/" (y `)) ` is Element of L ;

end;
let x, y be Element of L;

coherence

((x `) "\/" (y `)) ` is Element of L ;

:: deftheorem defines *' ROBBINS1:def 4 :

for L being non empty ComplLLattStr

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

for L being non empty ComplLLattStr

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

definition

let L be non empty ComplLLattStr ;

end;
attr L is Robbins means :Def5: :: ROBBINS1:def 5

for x, y being Element of L holds (((x + y) `) + ((x + (y `)) `)) ` = x;

for x, y being Element of L holds (((x + y) `) + ((x + (y `)) `)) ` = x;

:: deftheorem Def5 defines Robbins ROBBINS1:def 5 :

for L being non empty ComplLLattStr holds

( L is Robbins iff for x, y being Element of L holds (((x + y) `) + ((x + (y `)) `)) ` = x );

for L being non empty ComplLLattStr holds

( L is Robbins iff for x, y being Element of L holds (((x + y) `) + ((x + (y `)) `)) ` = x );

:: deftheorem Def6 defines Huntington ROBBINS1:def 6 :

for L being non empty ComplLLattStr holds

( L is Huntington iff for x, y being Element of L holds (((x `) + (y `)) `) + (((x `) + y) `) = x );

for L being non empty ComplLLattStr holds

( L is Huntington iff for x, y being Element of L holds (((x `) + (y `)) `) + (((x `) + y) `) = x );

definition

let G be non empty \/-SemiLattStr ;

end;
attr G is join-idempotent means :Def7: :: ROBBINS1:def 7

for x being Element of G holds x "\/" x = x;

for x being Element of G holds x "\/" x = x;

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

for G being non empty \/-SemiLattStr holds

( G is join-idempotent iff for x being Element of G holds x "\/" x = x );

for G being non empty \/-SemiLattStr holds

( G is join-idempotent iff for x being Element of G holds x "\/" x = x );

registration

( TrivComplLat is join-commutative & TrivComplLat is join-associative & TrivComplLat is Robbins & TrivComplLat is Huntington & TrivComplLat is join-idempotent )

( TrivOrtLat is join-commutative & TrivOrtLat is join-associative & TrivOrtLat is Huntington & TrivOrtLat is Robbins )
end;

cluster TrivComplLat -> join-commutative join-associative strict Robbins Huntington join-idempotent ;

coherence ( TrivComplLat is join-commutative & TrivComplLat is join-associative & TrivComplLat is Robbins & TrivComplLat is Huntington & TrivComplLat is join-idempotent )

proof end;

coherence ( TrivOrtLat is join-commutative & TrivOrtLat is join-associative & TrivOrtLat is Huntington & TrivOrtLat is Robbins )

proof end;

registration

coherence

( TrivOrtLat is meet-commutative & TrivOrtLat is meet-associative & TrivOrtLat is meet-absorbing & TrivOrtLat is join-absorbing )

end;
( TrivOrtLat is meet-commutative & TrivOrtLat is meet-associative & TrivOrtLat is meet-absorbing & TrivOrtLat is join-absorbing )

proof end;

registration

ex b_{1} being non empty ComplLLattStr st

( b_{1} is strict & b_{1} is join-associative & b_{1} is join-commutative & b_{1} is Robbins & b_{1} is join-idempotent & b_{1} is Huntington )
end;

cluster non empty join-commutative join-associative strict Robbins Huntington join-idempotent for ComplLLattStr ;

existence ex b

( b

proof end;

registration

existence

ex b_{1} being non empty OrthoLattStr st

( b_{1} is strict & b_{1} is Lattice-like & b_{1} is Robbins & b_{1} is Huntington )

end;
ex b

( b

proof end;

definition

let L be non empty join-commutative ComplLLattStr ;

let x, y be Element of L;

:: original: +

redefine func x + y -> M2( the carrier of L);

commutativity

for x, y being Element of L holds x + y = y + x by LATTICES:def 4;

end;
let x, y be Element of L;

:: original: +

redefine func x + y -> M2( the carrier of L);

commutativity

for x, y being Element of L holds x + y = y + x by LATTICES:def 4;

theorem Th1: :: ROBBINS1:1

for L being non empty join-commutative join-associative Huntington ComplLLattStr

for a, b being Element of L holds (a *' b) + (a *' (b `)) = a by Def6;

for a, b being Element of L holds (a *' b) + (a *' (b `)) = a by Def6;

theorem Th2: :: ROBBINS1:2

for L being non empty join-commutative join-associative Huntington ComplLLattStr

for a being Element of L holds a + (a `) = (a `) + ((a `) `)

for a being Element of L holds a + (a `) = (a `) + ((a `) `)

proof end;

theorem Th3: :: ROBBINS1:3

for L being non empty join-commutative join-associative Huntington ComplLLattStr

for x being Element of L holds (x `) ` = x

for x being Element of L holds (x `) ` = x

proof end;

theorem Th4: :: ROBBINS1:4

for L being non empty join-commutative join-associative Huntington ComplLLattStr

for a, b being Element of L holds a + (a `) = b + (b `)

for a, b being Element of L holds a + (a `) = b + (b `)

proof end;

theorem Th5: :: ROBBINS1:5

for L being non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr ex c being Element of L st

for a being Element of L holds

( c + a = c & a + (a `) = c )

for a being Element of L holds

( c + a = c & a + (a `) = c )

proof end;

theorem Th6: :: ROBBINS1:6

for L being non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr holds L is upper-bounded

proof end;

registration

for b_{1} being non empty ComplLLattStr st b_{1} is join-commutative & b_{1} is join-associative & b_{1} is join-idempotent & b_{1} is Huntington holds

b_{1} is upper-bounded
by Th6;

end;

cluster non empty join-commutative join-associative Huntington join-idempotent -> non empty upper-bounded for ComplLLattStr ;

coherence for b

b

definition

let L be non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr ;

compatibility

for b_{1} being M2( the carrier of L) holds

( b_{1} = Top L iff ex a being Element of L st b_{1} = a + (a `) )

end;
compatibility

for b

( b

proof end;

:: deftheorem Def8 defines Top ROBBINS1:def 8 :

for L being non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr

for b_{2} being M2( the carrier of b_{1}) holds

( b_{2} = Top L iff ex a being Element of L st b_{2} = a + (a `) );

for L being non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr

for b

( b

theorem Th7: :: ROBBINS1:7

for L being non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr ex c being Element of L st

for a being Element of L holds

( c *' a = c & (a + (a `)) ` = c )

for a being Element of L holds

( c *' a = c & (a + (a `)) ` = c )

proof end;

definition

let L be non empty join-commutative join-associative ComplLLattStr ;

let x, y be Element of L;

:: original: *'

redefine func x *' y -> Element of L;

commutativity

for x, y being Element of L holds x *' y = y *' x

end;
let x, y be Element of L;

:: original: *'

redefine func x *' y -> Element of L;

commutativity

for x, y being Element of L holds x *' y = y *' x

proof end;

definition

let L be non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr ;

ex b_{1} being Element of L st

for a being Element of L holds b_{1} *' a = b_{1}

for b_{1}, b_{2} being Element of L st ( for a being Element of L holds b_{1} *' a = b_{1} ) & ( for a being Element of L holds b_{2} *' a = b_{2} ) holds

b_{1} = b_{2}

end;
func Bot L -> Element of L means :Def9: :: ROBBINS1:def 9

for a being Element of L holds it *' a = it;

existence for a being Element of L holds it *' a = it;

ex b

for a being Element of L holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def9 defines Bot ROBBINS1:def 9 :

for L being non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr

for b_{2} being Element of L holds

( b_{2} = Bot L iff for a being Element of L holds b_{2} *' a = b_{2} );

for L being non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr

for b

( b

theorem Th8: :: ROBBINS1:8

for L being non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr

for a being Element of L holds Bot L = (a + (a `)) `

for a being Element of L holds Bot L = (a + (a `)) `

proof end;

theorem Th9: :: ROBBINS1:9

for L being non empty join-commutative join-associative Huntington join-idempotent ComplLLattStr holds

( (Top L) ` = Bot L & Top L = (Bot L) ` )

( (Top L) ` = Bot L & Top L = (Bot L) ` )

proof end;

theorem Th10: :: ROBBINS1:10

for L being non empty join-commutative join-associative Huntington ComplLLattStr

for a, b being Element of L st a ` = b ` holds

a = b

for a, b being Element of L st a ` = b ` holds

a = b

proof end;

theorem Th11: :: ROBBINS1:11

for L being non empty join-commutative join-associative Huntington ComplLLattStr

for a, b being Element of L holds a + ((b + (b `)) `) = a

for a, b being Element of L holds a + ((b + (b `)) `) = a

proof end;

theorem Th12: :: ROBBINS1:12

for L being non empty join-commutative join-associative Huntington ComplLLattStr

for a being Element of L holds a + a = a

for a being Element of L holds a + a = a

proof end;

registration

for b_{1} being non empty ComplLLattStr st b_{1} is join-commutative & b_{1} is join-associative & b_{1} is Huntington holds

b_{1} is join-idempotent
end;

cluster non empty join-commutative join-associative Huntington -> non empty join-idempotent for ComplLLattStr ;

coherence for b

b

proof end;

theorem Th13: :: ROBBINS1:13

for L being non empty join-commutative join-associative Huntington ComplLLattStr

for a being Element of L holds a + (Bot L) = a

for a being Element of L holds a + (Bot L) = a

proof end;

theorem :: ROBBINS1:14

for L being non empty join-commutative join-associative Huntington ComplLLattStr

for a being Element of L holds a *' (Top L) = a

for a being Element of L holds a *' (Top L) = a

proof end;

theorem Th15: :: ROBBINS1:15

for L being non empty join-commutative join-associative Huntington ComplLLattStr

for a being Element of L holds a *' (a `) = Bot L

for a being Element of L holds a *' (a `) = Bot L

proof end;

theorem Th16: :: ROBBINS1:16

for L being non empty join-commutative join-associative Huntington ComplLLattStr

for a, b, c being Element of L holds a *' (b *' c) = (a *' b) *' c

for a, b, c being Element of L holds a *' (b *' c) = (a *' b) *' c

proof end;

theorem Th17: :: ROBBINS1:17

for L being non empty join-commutative join-associative Huntington ComplLLattStr

for a, b being Element of L holds a + b = ((a `) *' (b `)) `

for a, b being Element of L holds a + b = ((a `) *' (b `)) `

proof end;

theorem :: ROBBINS1:18

for L being non empty join-commutative join-associative Huntington ComplLLattStr

for a being Element of L holds a *' a = a

for a being Element of L holds a *' a = a

proof end;

theorem :: ROBBINS1:19

for L being non empty join-commutative join-associative Huntington ComplLLattStr

for a being Element of L holds a + (Top L) = Top L

for a being Element of L holds a + (Top L) = Top L

proof end;

theorem Th20: :: ROBBINS1:20

for L being non empty join-commutative join-associative Huntington ComplLLattStr

for a, b being Element of L holds a + (a *' b) = a

for a, b being Element of L holds a + (a *' b) = a

proof end;

theorem Th21: :: ROBBINS1:21

for L being non empty join-commutative join-associative Huntington ComplLLattStr

for a, b being Element of L holds a *' (a + b) = a

for a, b being Element of L holds a *' (a + b) = a

proof end;

theorem Th22: :: ROBBINS1:22

for L being non empty join-commutative join-associative Huntington ComplLLattStr

for a, b being Element of L st (a `) + b = Top L & (b `) + a = Top L holds

a = b

for a, b being Element of L st (a `) + b = Top L & (b `) + a = Top L holds

a = b

proof end;

theorem Th23: :: ROBBINS1:23

for L being non empty join-commutative join-associative Huntington ComplLLattStr

for a, b being Element of L st a + b = Top L & a *' b = Bot L holds

a ` = b

for a, b being Element of L st a + b = Top L & a *' b = Bot L holds

a ` = b

proof end;

theorem Th24: :: ROBBINS1:24

for L being non empty join-commutative join-associative Huntington ComplLLattStr

for a, b, c being Element of L holds ((((((((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c)) + ((a *' (b `)) *' (c `))) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)) = Top L

for a, b, c being Element of L holds ((((((((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c)) + ((a *' (b `)) *' (c `))) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `)) = Top L

proof end;

theorem Th25: :: ROBBINS1:25

for L being non empty join-commutative join-associative Huntington ComplLLattStr

for a, b, c being Element of L holds

( (a *' c) *' (b *' (c `)) = Bot L & ((a *' b) *' c) *' (((a `) *' b) *' c) = Bot L & ((a *' (b `)) *' c) *' (((a `) *' b) *' c) = Bot L & ((a *' b) *' c) *' (((a `) *' (b `)) *' c) = Bot L & ((a *' b) *' (c `)) *' (((a `) *' (b `)) *' (c `)) = Bot L )

for a, b, c being Element of L holds

( (a *' c) *' (b *' (c `)) = Bot L & ((a *' b) *' c) *' (((a `) *' b) *' c) = Bot L & ((a *' (b `)) *' c) *' (((a `) *' b) *' c) = Bot L & ((a *' b) *' c) *' (((a `) *' (b `)) *' c) = Bot L & ((a *' b) *' (c `)) *' (((a `) *' (b `)) *' (c `)) = Bot L )

proof end;

theorem Th26: :: ROBBINS1:26

for L being non empty join-commutative join-associative Huntington ComplLLattStr

for a, b, c being Element of L holds (a *' b) + (a *' c) = (((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c)

for a, b, c being Element of L holds (a *' b) + (a *' c) = (((a *' b) *' c) + ((a *' b) *' (c `))) + ((a *' (b `)) *' c)

proof end;

theorem Th27: :: ROBBINS1:27

for L being non empty join-commutative join-associative Huntington ComplLLattStr

for a, b, c being Element of L holds (a *' (b + c)) ` = (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `))

for a, b, c being Element of L holds (a *' (b + c)) ` = (((((a *' (b `)) *' (c `)) + (((a `) *' b) *' c)) + (((a `) *' b) *' (c `))) + (((a `) *' (b `)) *' c)) + (((a `) *' (b `)) *' (c `))

proof end;

theorem Th28: :: ROBBINS1:28

for L being non empty join-commutative join-associative Huntington ComplLLattStr

for a, b, c being Element of L holds ((a *' b) + (a *' c)) + ((a *' (b + c)) `) = Top L

for a, b, c being Element of L holds ((a *' b) + (a *' c)) + ((a *' (b + c)) `) = Top L

proof end;

theorem Th29: :: ROBBINS1:29

for L being non empty join-commutative join-associative Huntington ComplLLattStr

for a, b, c being Element of L holds ((a *' b) + (a *' c)) *' ((a *' (b + c)) `) = Bot L

for a, b, c being Element of L holds ((a *' b) + (a *' c)) *' ((a *' (b + c)) `) = Bot L

proof end;

theorem Th30: :: ROBBINS1:30

for L being non empty join-commutative join-associative Huntington ComplLLattStr

for a, b, c being Element of L holds a *' (b + c) = (a *' b) + (a *' c)

for a, b, c being Element of L holds a *' (b + c) = (a *' b) + (a *' c)

proof end;

theorem :: ROBBINS1:31

for L being non empty join-commutative join-associative Huntington ComplLLattStr

for a, b, c being Element of L holds a + (b *' c) = (a + b) *' (a + c)

for a, b, c being Element of L holds a + (b *' c) = (a + b) *' (a + c)

proof end;

begin

definition

let L be non empty OrthoLattStr ;

end;
attr L is well-complemented means :Def10: :: ROBBINS1:def 10

for a being Element of L holds a ` is_a_complement_of a;

for a being Element of L holds a ` is_a_complement_of a;

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

for L being non empty OrthoLattStr holds

( L is well-complemented iff for a being Element of L holds a ` is_a_complement_of a );

for L being non empty OrthoLattStr holds

( L is well-complemented iff for a being Element of L holds a ` is_a_complement_of a );

registration

ex b_{1} being preOrthoLattice st

( b_{1} is strict & b_{1} is Boolean & b_{1} is well-complemented )
end;

cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like Boolean strict well-complemented for OrthoLattStr ;

existence ex b

( b

proof end;

theorem Th32: :: ROBBINS1:32

for L being distributive well-complemented preOrthoLattice

for x being Element of L holds (x `) ` = x

for x being Element of L holds (x `) ` = x

proof end;

theorem Th33: :: ROBBINS1:33

for L being distributive bounded well-complemented preOrthoLattice

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;

begin

:: according to the definition given in \cite{LATTICES.ABS}

definition

let L be non empty ComplLLattStr ;

ex b_{1} being strict OrthoLattStr st

( the carrier of b_{1} = the carrier of L & the L_join of b_{1} = the L_join of L & the Compl of b_{1} = the Compl of L & ( for a, b being Element of L holds the L_meet of b_{1} . (a,b) = a *' b ) )

for b_{1}, b_{2} being strict OrthoLattStr st the carrier of b_{1} = the carrier of L & the L_join of b_{1} = the L_join of L & the Compl of b_{1} = the Compl of L & ( for a, b being Element of L holds the L_meet of b_{1} . (a,b) = a *' b ) & the carrier of b_{2} = the carrier of L & the L_join of b_{2} = the L_join of L & the Compl of b_{2} = the Compl of L & ( for a, b being Element of L holds the L_meet of b_{2} . (a,b) = a *' b ) holds

b_{1} = b_{2}

end;
func CLatt L -> strict OrthoLattStr means :Def11: :: ROBBINS1:def 11

( the carrier of it = the carrier of L & the L_join of it = the L_join of L & the Compl of it = the Compl of L & ( for a, b being Element of L holds the L_meet of it . (a,b) = a *' b ) );

existence ( the carrier of it = the carrier of L & the L_join of it = the L_join of L & the Compl of it = the Compl of L & ( for a, b being Element of L holds the L_meet of it . (a,b) = a *' b ) );

ex b

( the carrier of b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def11 defines CLatt ROBBINS1:def 11 :

for L being non empty ComplLLattStr

for b_{2} being strict OrthoLattStr holds

( b_{2} = CLatt L iff ( the carrier of b_{2} = the carrier of L & the L_join of b_{2} = the L_join of L & the Compl of b_{2} = the Compl of L & ( for a, b being Element of L holds the L_meet of b_{2} . (a,b) = a *' b ) ) );

for L being non empty ComplLLattStr

for b

( b

registration

let L be non empty join-commutative ComplLLattStr ;

coherence

CLatt L is join-commutative

end;
coherence

CLatt L is join-commutative

proof end;

registration

let L be non empty join-associative ComplLLattStr ;

coherence

CLatt L is join-associative

end;
coherence

CLatt L is join-associative

proof end;

registration

let L be non empty join-commutative join-associative ComplLLattStr ;

coherence

CLatt L is meet-commutative

end;
coherence

CLatt L is meet-commutative

proof end;

theorem :: ROBBINS1:34

registration

let L be non empty join-commutative join-associative Huntington ComplLLattStr ;

coherence

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

end;
coherence

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

proof end;

registration
end;

registration

let L be non empty join-commutative join-associative Huntington ComplLLattStr ;

coherence

CLatt L is lower-bounded

end;
coherence

CLatt L is lower-bounded

proof end;

theorem Th35: :: ROBBINS1:35

for L being non empty join-commutative join-associative Huntington ComplLLattStr holds Bot L = Bottom (CLatt L)

proof end;

registration

let L be non empty join-commutative join-associative Huntington ComplLLattStr ;

coherence

( CLatt L is complemented & CLatt L is distributive & CLatt L is bounded )

end;
coherence

( CLatt L is complemented & CLatt L is distributive & CLatt L is bounded )

proof end;

begin

definition

let G be non empty join-commutative ComplLLattStr ;

( G is Huntington iff for x, y being Element of G holds (- ((- x) + (- y))) + (- (x + (- y))) = y )

end;
redefine attr G is Huntington means :Def12: :: ROBBINS1:def 12

for x, y being Element of G holds (- ((- x) + (- y))) + (- (x + (- y))) = y;

compatibility for x, y being Element of G holds (- ((- x) + (- y))) + (- (x + (- y))) = y;

( G is Huntington iff for x, y being Element of G holds (- ((- x) + (- y))) + (- (x + (- y))) = y )

proof end;

:: deftheorem Def12 defines Huntington ROBBINS1:def 12 :

for G being non empty join-commutative ComplLLattStr holds

( G is Huntington iff for x, y being Element of G holds (- ((- x) + (- y))) + (- (x + (- y))) = y );

for G being non empty join-commutative ComplLLattStr holds

( G is Huntington iff for x, y being Element of G holds (- ((- x) + (- y))) + (- (x + (- y))) = y );

definition

let G be non empty ComplLLattStr ;

;

end;
attr G is with_idempotent_element means :Def13: :: ROBBINS1:def 13

ex x being Element of G st x + x = x;

correctness ex x being Element of G st x + x = x;

;

:: deftheorem Def13 defines with_idempotent_element ROBBINS1:def 13 :

for G being non empty ComplLLattStr holds

( G is with_idempotent_element iff ex x being Element of G st x + x = x );

for G being non empty ComplLLattStr holds

( G is with_idempotent_element iff ex x being Element of G st x + x = x );

definition

let G be non empty ComplLLattStr ;

let x, y be Element of G;

coherence

- ((- x) + y) is Element of G ;

end;
let x, y be Element of G;

coherence

- ((- x) + y) is Element of G ;

:: deftheorem defines \delta ROBBINS1:def 14 :

for G being non empty ComplLLattStr

for x, y being Element of G holds \delta (x,y) = - ((- x) + y);

for G being non empty ComplLLattStr

for x, y being Element of G holds \delta (x,y) = - ((- x) + y);

definition

let G be non empty ComplLLattStr ;

let x, y be Element of G;

coherence

\delta ((x + y),(\delta (x,y))) is Element of G ;

end;
let x, y be Element of G;

coherence

\delta ((x + y),(\delta (x,y))) is Element of G ;

:: deftheorem defines Expand ROBBINS1:def 15 :

for G being non empty ComplLLattStr

for x, y being Element of G holds Expand (x,y) = \delta ((x + y),(\delta (x,y)));

for G being non empty ComplLLattStr

for x, y being Element of G holds Expand (x,y) = \delta ((x + y),(\delta (x,y)));

definition

let G be non empty ComplLLattStr ;

let x be Element of G;

coherence

- ((- x) + x) is Element of G ;

coherence

x + x is Element of G ;

end;
let x be Element of G;

coherence

- ((- x) + x) is Element of G ;

coherence

x + x is Element of G ;

:: deftheorem defines _0 ROBBINS1:def 16 :

for G being non empty ComplLLattStr

for x being Element of G holds x _0 = - ((- x) + x);

for G being non empty ComplLLattStr

for x being Element of G holds x _0 = - ((- x) + x);

:: deftheorem defines Double ROBBINS1:def 17 :

for G being non empty ComplLLattStr

for x being Element of G holds Double x = x + x;

for G being non empty ComplLLattStr

for x being Element of G holds Double x = x + x;

definition

let G be non empty ComplLLattStr ;

let x be Element of G;

coherence

(x _0) + x is Element of G ;

coherence

(x _0) + (Double x) is Element of G ;

coherence

(x _0) + ((Double x) + x) is Element of G ;

coherence

(x _0) + ((Double x) + (Double x)) is Element of G ;

end;
let x be Element of G;

coherence

(x _0) + x is Element of G ;

coherence

(x _0) + (Double x) is Element of G ;

coherence

(x _0) + ((Double x) + x) is Element of G ;

coherence

(x _0) + ((Double x) + (Double x)) is Element of G ;

:: deftheorem defines _1 ROBBINS1:def 18 :

for G being non empty ComplLLattStr

for x being Element of G holds x _1 = (x _0) + x;

for G being non empty ComplLLattStr

for x being Element of G holds x _1 = (x _0) + x;

:: deftheorem defines _2 ROBBINS1:def 19 :

for G being non empty ComplLLattStr

for x being Element of G holds x _2 = (x _0) + (Double x);

for G being non empty ComplLLattStr

for x being Element of G holds x _2 = (x _0) + (Double x);

:: deftheorem defines _3 ROBBINS1:def 20 :

for G being non empty ComplLLattStr

for x being Element of G holds x _3 = (x _0) + ((Double x) + x);

for G being non empty ComplLLattStr

for x being Element of G holds x _3 = (x _0) + ((Double x) + x);

:: deftheorem defines _4 ROBBINS1:def 21 :

for G being non empty ComplLLattStr

for x being Element of G holds x _4 = (x _0) + ((Double x) + (Double x));

for G being non empty ComplLLattStr

for x being Element of G holds x _4 = (x _0) + ((Double x) + (Double x));

theorem Th36: :: ROBBINS1:36

for G being non empty join-commutative join-associative Robbins ComplLLattStr

for x, y being Element of G holds \delta ((x + y),(\delta (x,y))) = y

for x, y being Element of G holds \delta ((x + y),(\delta (x,y))) = y

proof end;

theorem :: ROBBINS1:37

for G being non empty join-commutative join-associative Robbins ComplLLattStr

for x, y being Element of G holds Expand (x,y) = y by Th36;

for x, y being Element of G holds Expand (x,y) = y by Th36;

theorem :: ROBBINS1:38

for G being non empty join-commutative join-associative Robbins ComplLLattStr

for x, y, z being Element of G holds \delta (((- x) + y),z) = - ((\delta (x,y)) + z) ;

for x, y, z being Element of G holds \delta (((- x) + y),z) = - ((\delta (x,y)) + z) ;

theorem :: ROBBINS1:39

for G being non empty join-commutative join-associative Robbins ComplLLattStr

for x being Element of G holds \delta (x,x) = x _0 ;

for x being Element of G holds \delta (x,x) = x _0 ;

theorem Th40: :: ROBBINS1:40

for G being non empty join-commutative join-associative Robbins ComplLLattStr

for x being Element of G holds \delta ((Double x),(x _0)) = x

for x being Element of G holds \delta ((Double x),(x _0)) = x

proof end;

theorem Th41: :: ROBBINS1:41

for G being non empty join-commutative join-associative Robbins ComplLLattStr

for x being Element of G holds \delta ((x _2),x) = x _0

for x being Element of G holds \delta ((x _2),x) = x _0

proof end;

theorem Th42: :: ROBBINS1:42

for G being non empty join-commutative join-associative Robbins ComplLLattStr

for x being Element of G holds (x _4) + (x _0) = (x _3) + (x _1)

for x being Element of G holds (x _4) + (x _0) = (x _3) + (x _1)

proof end;

theorem Th43: :: ROBBINS1:43

for G being non empty join-commutative join-associative Robbins ComplLLattStr

for x being Element of G holds (x _3) + (x _0) = (x _2) + (x _1)

for x being Element of G holds (x _3) + (x _0) = (x _2) + (x _1)

proof end;

theorem Th44: :: ROBBINS1:44

for G being non empty join-commutative join-associative Robbins ComplLLattStr

for x being Element of G holds (x _3) + x = x _4

for x being Element of G holds (x _3) + x = x _4

proof end;

theorem Th45: :: ROBBINS1:45

for G being non empty join-commutative join-associative Robbins ComplLLattStr

for x being Element of G holds \delta ((x _3),(x _0)) = x

for x being Element of G holds \delta ((x _3),(x _0)) = x

proof end;

theorem :: ROBBINS1:46

for G being non empty join-commutative join-associative Robbins ComplLLattStr

for x, y, z being Element of G st - x = - y holds

\delta (x,z) = \delta (y,z) ;

for x, y, z being Element of G st - x = - y holds

\delta (x,z) = \delta (y,z) ;

theorem Th47: :: ROBBINS1:47

for G being non empty join-commutative join-associative Robbins ComplLLattStr

for x, y being Element of G holds \delta (x,(- y)) = \delta (y,(- x))

for x, y being Element of G holds \delta (x,(- y)) = \delta (y,(- x))

proof end;

theorem Th48: :: ROBBINS1:48

for G being non empty join-commutative join-associative Robbins ComplLLattStr

for x being Element of G holds \delta ((x _3),x) = x _0

for x being Element of G holds \delta ((x _3),x) = x _0

proof end;

theorem Th49: :: ROBBINS1:49

for G being non empty join-commutative join-associative Robbins ComplLLattStr

for x being Element of G holds \delta (((x _1) + (x _3)),x) = x _0

for x being Element of G holds \delta (((x _1) + (x _3)),x) = x _0

proof end;

theorem Th50: :: ROBBINS1:50

for G being non empty join-commutative join-associative Robbins ComplLLattStr

for x being Element of G holds \delta (((x _1) + (x _2)),x) = x _0

for x being Element of G holds \delta (((x _1) + (x _2)),x) = x _0

proof end;

theorem Th51: :: ROBBINS1:51

for G being non empty join-commutative join-associative Robbins ComplLLattStr

for x being Element of G holds \delta (((x _1) + (x _3)),(x _0)) = x

for x being Element of G holds \delta (((x _1) + (x _3)),(x _0)) = x

proof end;

definition

let G be non empty join-commutative join-associative Robbins ComplLLattStr ;

let x be Element of G;

coherence

((- ((x _1) + (x _3))) + x) + (- (x _3)) is Element of G ;

end;
let x be Element of G;

coherence

((- ((x _1) + (x _3))) + x) + (- (x _3)) is Element of G ;

:: deftheorem defines \beta ROBBINS1:def 22 :

for G being non empty join-commutative join-associative Robbins ComplLLattStr

for x being Element of G holds \beta x = ((- ((x _1) + (x _3))) + x) + (- (x _3));

for G being non empty join-commutative join-associative Robbins ComplLLattStr

for x being Element of G holds \beta x = ((- ((x _1) + (x _3))) + x) + (- (x _3));

theorem Th52: :: ROBBINS1:52

for G being non empty join-commutative join-associative Robbins ComplLLattStr

for x being Element of G holds \delta ((\beta x),x) = - (x _3)

for x being Element of G holds \delta ((\beta x),x) = - (x _3)

proof end;

theorem Th53: :: ROBBINS1:53

for G being non empty join-commutative join-associative Robbins ComplLLattStr

for x being Element of G holds \delta ((\beta x),x) = - ((x _1) + (x _3))

for x being Element of G holds \delta ((\beta x),x) = - ((x _1) + (x _3))

proof end;

theorem :: ROBBINS1:54

for G being non empty join-commutative join-associative Robbins ComplLLattStr ex y, z being Element of G st - (y + z) = - z

proof end;

begin

theorem :: ROBBINS1:55

for G being non empty join-commutative join-associative Robbins ComplLLattStr st ( for z being Element of G holds - (- z) = z ) holds

G is Huntington

G is Huntington

proof end;

theorem Th56: :: ROBBINS1:56

for G being non empty join-commutative join-associative Robbins ComplLLattStr st G is with_idempotent_element holds

G is Huntington

G is Huntington

proof end;

registration

for b_{1} being non empty join-commutative join-associative Robbins ComplLLattStr st b_{1} is with_idempotent_element holds

b_{1} is Huntington
by Th56;

end;

cluster non empty join-commutative join-associative Robbins with_idempotent_element -> non empty join-commutative join-associative Robbins Huntington for ComplLLattStr ;

coherence for b

b

theorem Th57: :: ROBBINS1:57

for G being non empty join-commutative join-associative Robbins ComplLLattStr st ex c, d being Element of G st c + d = c holds

G is Huntington

G is Huntington

proof end;

theorem Th58: :: ROBBINS1:58

for G being non empty join-commutative join-associative Robbins ComplLLattStr ex y, z being Element of G st y + z = z

proof end;

registration

for b_{1} being non empty join-commutative join-associative ComplLLattStr st b_{1} is Robbins holds

b_{1} is Huntington
end;

cluster non empty join-commutative join-associative Robbins -> non empty join-commutative join-associative Huntington for ComplLLattStr ;

coherence for b

b

proof end;

:: deftheorem Def23 defines de_Morgan ROBBINS1:def 23 :

for L being non empty OrthoLattStr holds

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

for L being non empty OrthoLattStr holds

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

theorem Th59: :: ROBBINS1:59

for L being non empty join-commutative meet-commutative well-complemented OrthoLattStr

for x being Element of L holds

( x + (x `) = Top L & x "/\" (x `) = Bottom L )

for x being Element of L holds

( x + (x `) = Top L & x "/\" (x `) = Bottom L )

proof end;

registration
end;

registration

ex b_{1} being preOrthoLattice st

( b_{1} is strict & b_{1} is de_Morgan & b_{1} is Boolean & b_{1} is Robbins & b_{1} is Huntington )
end;

cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like Boolean strict Robbins Huntington de_Morgan for OrthoLattStr ;

existence ex b

( b

proof end;

registration

for b_{1} being non empty OrthoLattStr st b_{1} is join-associative & b_{1} is join-commutative & b_{1} is de_Morgan holds

b_{1} is meet-commutative
end;

cluster non empty join-commutative join-associative de_Morgan -> non empty meet-commutative for OrthoLattStr ;

coherence for b

b

proof end;

registration

for b_{1} being well-complemented preOrthoLattice st b_{1} is Boolean holds

b_{1} is Huntington
end;

cluster non empty Lattice-like Boolean well-complemented -> Huntington well-complemented for OrthoLattStr ;

coherence for b

b

proof end;

registration

coherence

for b_{1} being de_Morgan preOrthoLattice st b_{1} is Huntington holds

b_{1} is Boolean

end;
for b

b

proof end;

registration

coherence

for b_{1} being preOrthoLattice st b_{1} is Robbins & b_{1} is de_Morgan holds

b_{1} is Boolean
;

for b_{1} being well-complemented preOrthoLattice st b_{1} is Boolean holds

b_{1} is Robbins

end;
for b

b

cluster non empty Lattice-like Boolean well-complemented -> Robbins well-complemented for OrthoLattStr ;

coherence for b

b

proof end;