:: by Wioletta Truszkowska and Adam Grabowski

::

:: Received June 28, 2003

:: Copyright (c) 2003-2016 Association of Mizar Users

:: deftheorem Def1 defines satisfying_DN_1 ROBBINS2:def 1 :

for L being non empty ComplLLattStr holds

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

for L being non empty ComplLLattStr holds

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

registration

coherence

TrivComplLat is satisfying_DN_1 by STRUCT_0:def 10;

coherence

TrivOrtLat is satisfying_DN_1 by STRUCT_0:def 10;

end;
TrivComplLat is satisfying_DN_1 by STRUCT_0:def 10;

coherence

TrivOrtLat is satisfying_DN_1 by STRUCT_0:def 10;

registration

existence

ex b_{1} being non empty ComplLLattStr st

( b_{1} is join-commutative & b_{1} is join-associative & b_{1} is satisfying_DN_1 )

end;
ex b

( b

proof end;

theorem Th1: :: ROBBINS2:1

for L being non empty satisfying_DN_1 ComplLLattStr

for x, y, z, u, v being Element of L holds (((x + y) `) + ((((((z + u) `) + x) `) + (((y `) + ((y + v) `)) `)) `)) ` = y

for x, y, z, u, v being Element of L holds (((x + y) `) + ((((((z + u) `) + x) `) + (((y `) + ((y + v) `)) `)) `)) ` = y

proof end;

theorem Th2: :: ROBBINS2:2

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th3: :: ROBBINS2:3

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th4: :: ROBBINS2:4

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th5: :: ROBBINS2:5

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th6: :: ROBBINS2:6

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th7: :: ROBBINS2:7

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th8: :: ROBBINS2:8

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th9: :: ROBBINS2:9

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th10: :: ROBBINS2:10

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th11: :: ROBBINS2:11

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th12: :: ROBBINS2:12

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th13: :: ROBBINS2:13

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th14: :: ROBBINS2:14

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th15: :: ROBBINS2:15

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th16: :: ROBBINS2:16

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th17: :: ROBBINS2:17

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th18: :: ROBBINS2:18

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th19: :: ROBBINS2:19

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th20: :: ROBBINS2:20

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th22: :: ROBBINS2:22

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th24: :: ROBBINS2:24

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th25: :: ROBBINS2:25

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th26: :: ROBBINS2:26

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

Lm1: for L being non empty satisfying_DN_1 ComplLLattStr holds L is join-commutative

proof end;

registration

coherence

for b_{1} being non empty ComplLLattStr st b_{1} is satisfying_DN_1 holds

b_{1} is join-commutative
by Lm1;

end;
for b

b

theorem Th28: :: ROBBINS2:28

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem :: ROBBINS2:29

theorem :: ROBBINS2:30

theorem Th31: :: ROBBINS2:31

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th32: :: ROBBINS2:32

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem :: ROBBINS2:33

theorem Th34: :: ROBBINS2:34

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th35: :: ROBBINS2:35

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th36: :: ROBBINS2:36

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th37: :: ROBBINS2:37

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th38: :: ROBBINS2:38

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem :: ROBBINS2:39

theorem Th40: :: ROBBINS2:40

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th41: :: ROBBINS2:41

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th42: :: ROBBINS2:42

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th43: :: ROBBINS2:43

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th44: :: ROBBINS2:44

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th45: :: ROBBINS2:45

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th46: :: ROBBINS2:46

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th47: :: ROBBINS2:47

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th48: :: ROBBINS2:48

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th49: :: ROBBINS2:49

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th50: :: ROBBINS2:50

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th51: :: ROBBINS2:51

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th52: :: ROBBINS2:52

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem Th53: :: ROBBINS2:53

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem :: ROBBINS2:54

theorem Th55: :: ROBBINS2:55

for L being non empty satisfying_DN_1 ComplLLattStr

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

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

proof end;

theorem :: ROBBINS2:56

for L being non empty satisfying_DN_1 ComplLLattStr

for x, y, z being Element of L holds x + (y + z) = y + (z + x) by Th55;

for x, y, z being Element of L holds x + (y + z) = y + (z + x) by Th55;

theorem :: ROBBINS2:57

for L being non empty satisfying_DN_1 ComplLLattStr

for x, y, z being Element of L holds (x + y) + z = x + (y + z) by Th55;

for x, y, z being Element of L holds (x + y) + z = x + (y + z) by Th55;

Lm2: for L being non empty satisfying_DN_1 ComplLLattStr holds L is join-associative

proof end;

Lm3: for L being non empty satisfying_DN_1 ComplLLattStr holds L is Robbins

proof end;

registration

coherence

for b_{1} being non empty ComplLLattStr st b_{1} is satisfying_DN_1 holds

b_{1} is join-associative
by Lm2;

coherence

for b_{1} being non empty ComplLLattStr st b_{1} is satisfying_DN_1 holds

b_{1} is Robbins
by Lm3;

end;
for b

b

coherence

for b

b

theorem Th58: :: ROBBINS2:58

for L being non empty ComplLLattStr

for x, z being Element of L st L is join-commutative & L is join-associative & L is Huntington holds

(z + x) *' (z + (x `)) = z

for x, z being Element of L st L is join-commutative & L is join-associative & L is Huntington holds

(z + x) *' (z + (x `)) = z

proof end;

theorem Th59: :: ROBBINS2:59

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

L is satisfying_DN_1

L is satisfying_DN_1

proof end;

registration

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

b_{1} is satisfying_DN_1
by Th59;

end;

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

coherence for b

b

registration

ex b_{1} being preOrthoLattice st

( b_{1} is satisfying_DN_1 & b_{1} is de_Morgan )
end;

cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like de_Morgan satisfying_DN_1 for OrthoLattStr ;

existence ex b

( b

proof end;

registration

coherence

for b_{1} being preOrthoLattice st b_{1} is satisfying_DN_1 & 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 satisfying_DN_1
;

end;
for b

b

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

coherence for b

b

definition

let L be non empty ComplLLattStr ;

end;
attr L is satisfying_MD_1 means :: ROBBINS2:def 2

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

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

:: deftheorem defines satisfying_MD_1 ROBBINS2:def 2 :

for L being non empty ComplLLattStr holds

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

for L being non empty ComplLLattStr holds

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

:: deftheorem defines satisfying_MD_2 ROBBINS2:def 3 :

for L being non empty ComplLLattStr holds

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

for L being non empty ComplLLattStr holds

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

Lm4: now :: thesis: for L being non empty ComplLLattStr st L is satisfying_MD_1 & L is satisfying_MD_2 holds

( L is join-commutative & L is Huntington & L is join-associative )

( L is join-commutative & L is Huntington & L is join-associative )

let L be non empty ComplLLattStr ; :: thesis: ( L is satisfying_MD_1 & L is satisfying_MD_2 implies ( L is join-commutative & L is Huntington & L is join-associative ) )

assume A1: ( L is satisfying_MD_1 & L is satisfying_MD_2 ) ; :: thesis: ( L is join-commutative & L is Huntington & L is join-associative )

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

A28: for x, y, z being Element of L holds (((((x `) + y) `) + z) `) + ((x `) + z) = z + ((x `) + y)

A32: for x, y, z being Element of L holds (x + y) + (y + z) = (x + y) + z

end;
assume A1: ( L is satisfying_MD_1 & L is satisfying_MD_2 ) ; :: thesis: ( L is join-commutative & L is Huntington & L is join-associative )

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

proof

A3:
for x, y being Element of L holds (((x `) + y) `) + y = y + x
let x, y be Element of L; :: thesis: (x `) + ((x `) + y) = (x `) + y

set X = (x `) + y;

(((x `) + y) `) + x = x by A1;

hence (x `) + ((x `) + y) = (x `) + y by A1; :: thesis: verum

end;
set X = (x `) + y;

(((x `) + y) `) + x = x by A1;

hence (x `) + ((x `) + y) = (x `) + y by A1; :: thesis: verum

proof

A5:
for x being Element of L holds x + x = x
let x, y be Element of L; :: thesis: (((x `) + y) `) + y = y + x

set X = (x `) + y;

A4: (((x `) + y) `) + ((((x `) + y) `) + y) = y + ((((x `) + y) `) + x) by A1;

(((x `) + y) `) + y = (((x `) + y) `) + ((((x `) + y) `) + y) by A2

.= y + x by A1, A4 ;

hence (((x `) + y) `) + y = y + x ; :: thesis: verum

end;
set X = (x `) + y;

A4: (((x `) + y) `) + ((((x `) + y) `) + y) = y + ((((x `) + y) `) + x) by A1;

(((x `) + y) `) + y = (((x `) + y) `) + ((((x `) + y) `) + y) by A2

.= y + x by A1, A4 ;

hence (((x `) + y) `) + y = y + x ; :: thesis: verum

proof

A6:
for x, y being Element of L holds x + (x + y) = x + y
let x be Element of L; :: thesis: x + x = x

x + x = (((x `) + x) `) + x by A3

.= x by A1 ;

hence x + x = x ; :: thesis: verum

end;
x + x = (((x `) + x) `) + x by A3

.= x by A1 ;

hence x + x = x ; :: thesis: verum

proof

A7:
for x, y being Element of L holds (x + y) + y = x + y
let x, y be Element of L; :: thesis: x + (x + y) = x + y

x + (x + y) = (((y `) + x) `) + (x + x) by A1

.= (((y `) + x) `) + x by A5

.= x + y by A3 ;

hence x + (x + y) = x + y ; :: thesis: verum

end;
x + (x + y) = (((y `) + x) `) + (x + x) by A1

.= (((y `) + x) `) + x by A5

.= x + y by A3 ;

hence x + (x + y) = x + y ; :: thesis: verum

proof

A8:
for x, y being Element of L holds (x + y) + x = x + y
let x, y be Element of L; :: thesis: (x + y) + y = x + y

set Y = x + y;

(x + y) + y = (((y `) + (x + y)) `) + (x + y) by A3

.= (((y `) + (x + y)) `) + (x + (x + y)) by A6

.= (x + y) + (x + y) by A1

.= x + y by A5 ;

hence (x + y) + y = x + y ; :: thesis: verum

end;
set Y = x + y;

(x + y) + y = (((y `) + (x + y)) `) + (x + y) by A3

.= (((y `) + (x + y)) `) + (x + (x + y)) by A6

.= (x + y) + (x + y) by A1

.= x + y by A5 ;

hence (x + y) + y = x + y ; :: thesis: verum

proof

A9:
for x, y being Element of L holds x + (y + (y + x)) = y + x
let x, y be Element of L; :: thesis: (x + y) + x = x + y

(x + y) + x = ((((y `) + x) `) + x) + x by A3

.= (((y `) + x) `) + x by A7

.= x + y by A3 ;

hence (x + y) + x = x + y ; :: thesis: verum

end;
(x + y) + x = ((((y `) + x) `) + x) + x by A3

.= (((y `) + x) `) + x by A7

.= x + y by A3 ;

hence (x + y) + x = x + y ; :: thesis: verum

proof

A10:
for x, y being Element of L holds x + (y + x) = y + x
let x, y be Element of L; :: thesis: x + (y + (y + x)) = y + x

set Z = y + x;

x + (y + (y + x)) = ((((y + x) `) + x) `) + (y + x) by A1

.= y + x by A1 ;

hence x + (y + (y + x)) = y + x ; :: thesis: verum

end;
set Z = y + x;

x + (y + (y + x)) = ((((y + x) `) + x) `) + (y + x) by A1

.= y + x by A1 ;

hence x + (y + (y + x)) = y + x ; :: thesis: verum

proof

A11:
for x, y being Element of L holds ((x + (y `)) `) + y = y
let x, y be Element of L; :: thesis: x + (y + x) = y + x

x + (y + x) = x + (y + (y + x)) by A6

.= y + x by A9 ;

hence x + (y + x) = y + x ; :: thesis: verum

end;
x + (y + x) = x + (y + (y + x)) by A6

.= y + x by A9 ;

hence x + (y + x) = y + x ; :: thesis: verum

proof

A12:
for x being Element of L holds ((x `) `) + x = x
let x, y be Element of L; :: thesis: ((x + (y `)) `) + y = y

((x + (y `)) `) + y = (((y `) + (x + (y `))) `) + y by A10

.= y by A1 ;

hence ((x + (y `)) `) + y = y ; :: thesis: verum

end;
((x + (y `)) `) + y = (((y `) + (x + (y `))) `) + y by A10

.= y by A1 ;

hence ((x + (y `)) `) + y = y ; :: thesis: verum

proof

A13:
for x being Element of L holds x + ((x `) `) = x
let x be Element of L; :: thesis: ((x `) `) + x = x

(((x `) + (x `)) `) + x = x by A1;

hence ((x `) `) + x = x by A5; :: thesis: verum

end;
(((x `) + (x `)) `) + x = x by A1;

hence ((x `) `) + x = x by A5; :: thesis: verum

proof

A14:
for x, y being Element of L holds x + (((x `) `) + y) = x + y
let x be Element of L; :: thesis: x + ((x `) `) = x

x + ((x `) `) = (((x `) `) + x) + ((x `) `) by A12

.= ((x `) `) + x by A8

.= x by A12 ;

hence x + ((x `) `) = x ; :: thesis: verum

end;
x + ((x `) `) = (((x `) `) + x) + ((x `) `) by A12

.= ((x `) `) + x by A8

.= x by A12 ;

hence x + ((x `) `) = x ; :: thesis: verum

proof

A15:
for x being Element of L holds x + ((((x `) `) `) `) = x
let x, y be Element of L; :: thesis: x + (((x `) `) + y) = x + y

x + (((x `) `) + y) = (((y `) + x) `) + (((x `) `) + x) by A1

.= (((y `) + x) `) + x by A12

.= x + y by A3 ;

hence x + (((x `) `) + y) = x + y ; :: thesis: verum

end;
x + (((x `) `) + y) = (((y `) + x) `) + (((x `) `) + x) by A1

.= (((y `) + x) `) + x by A12

.= x + y by A3 ;

hence x + (((x `) `) + y) = x + y ; :: thesis: verum

proof

A16:
for x being Element of L holds ((x `) `) ` = x `
let x be Element of L; :: thesis: x + ((((x `) `) `) `) = x

x + ((((x `) `) `) `) = x + (((x `) `) + ((((x `) `) `) `)) by A14

.= x + ((x `) `) by A13

.= x by A13 ;

hence x + ((((x `) `) `) `) = x ; :: thesis: verum

end;
x + ((((x `) `) `) `) = x + (((x `) `) + ((((x `) `) `) `)) by A14

.= x + ((x `) `) by A13

.= x by A13 ;

hence x + ((((x `) `) `) `) = x ; :: thesis: verum

proof

A17:
for x, y, z being Element of L holds (((x `) + y) `) + ((((x `) + z) `) + y) = y + x
let x be Element of L; :: thesis: ((x `) `) ` = x `

((x `) `) ` = ((x + ((((x `) `) `) `)) `) + (((x `) `) `) by A11

.= (x `) + (((x `) `) `) by A15

.= x ` by A13 ;

hence ((x `) `) ` = x ` ; :: thesis: verum

end;
((x `) `) ` = ((x + ((((x `) `) `) `)) `) + (((x `) `) `) by A11

.= (x `) + (((x `) `) `) by A15

.= x ` by A13 ;

hence ((x `) `) ` = x ` ; :: thesis: verum

proof

A18:
for x, y being Element of L holds x + ((y `) `) = x + y
let x, y, z be Element of L; :: thesis: (((x `) + y) `) + ((((x `) + z) `) + y) = y + x

(((x `) + y) `) + ((((x `) + z) `) + y) = y + ((((x `) + z) `) + x) by A1

.= y + x by A1 ;

hence (((x `) + y) `) + ((((x `) + z) `) + y) = y + x ; :: thesis: verum

end;
(((x `) + y) `) + ((((x `) + z) `) + y) = y + ((((x `) + z) `) + x) by A1

.= y + x by A1 ;

hence (((x `) + y) `) + ((((x `) + z) `) + y) = y + x ; :: thesis: verum

proof

A19:
for x being Element of L holds (x `) ` = x
let x, y be Element of L; :: thesis: x + ((y `) `) = x + y

x + y = (((y `) + x) `) + ((((y `) + x) `) + x) by A17

.= (((y `) + x) `) + ((((((y `) `) `) + x) `) + x) by A16

.= (((((y `) `) `) + x) `) + ((((((y `) `) `) + x) `) + x) by A16

.= x + ((y `) `) by A17 ;

hence x + ((y `) `) = x + y ; :: thesis: verum

end;
x + y = (((y `) + x) `) + ((((y `) + x) `) + x) by A17

.= (((y `) + x) `) + ((((((y `) `) `) + x) `) + x) by A16

.= (((((y `) `) `) + x) `) + ((((((y `) `) `) + x) `) + x) by A16

.= x + ((y `) `) by A17 ;

hence x + ((y `) `) = x + y ; :: thesis: verum

proof

A20:
for x, y, z being Element of L holds (((x `) + ((((y + x) `) + z) `)) `) + (y + ((((y + x) `) + z) `)) = y + x
let x be Element of L; :: thesis: (x `) ` = x

(x `) ` = (((((x `) `) `) + ((x `) `)) `) + ((x `) `) by A1

.= (((x `) + ((x `) `)) `) + ((x `) `) by A16

.= (((x `) + ((x `) `)) `) + x by A18

.= x by A1 ;

hence (x `) ` = x ; :: thesis: verum

end;
(x `) ` = (((((x `) `) `) + ((x `) `)) `) + ((x `) `) by A1

.= (((x `) + ((x `) `)) `) + ((x `) `) by A16

.= (((x `) + ((x `) `)) `) + x by A18

.= x by A1 ;

hence (x `) ` = x ; :: thesis: verum

proof

A21:
for x, y being Element of L holds (((x `) + ((x + y) `)) `) + ((y `) + ((x + y) `)) = (y `) + x
let x, y, z be Element of L; :: thesis: (((x `) + ((((y + x) `) + z) `)) `) + (y + ((((y + x) `) + z) `)) = y + x

set P = (((y + x) `) + z) ` ;

(((x `) + ((((y + x) `) + z) `)) `) + (y + ((((y + x) `) + z) `)) = ((((y + x) `) + z) `) + (y + x) by A1

.= y + x by A1 ;

hence (((x `) + ((((y + x) `) + z) `)) `) + (y + ((((y + x) `) + z) `)) = y + x ; :: thesis: verum

end;
set P = (((y + x) `) + z) ` ;

(((x `) + ((((y + x) `) + z) `)) `) + (y + ((((y + x) `) + z) `)) = ((((y + x) `) + z) `) + (y + x) by A1

.= y + x by A1 ;

hence (((x `) + ((((y + x) `) + z) `)) `) + (y + ((((y + x) `) + z) `)) = y + x ; :: thesis: verum

proof

A22:
for x, y being Element of L holds x + (((x `) + y) `) = x
let x, y be Element of L; :: thesis: (((x `) + ((x + y) `)) `) + ((y `) + ((x + y) `)) = (y `) + x

(((x `) + ((x + y) `)) `) + ((y `) + ((x + y) `)) = (((x `) + ((x + y) `)) `) + ((y `) + (((((y `) + x) `) + x) `)) by A3

.= (((x `) + (((((y `) + x) `) + x) `)) `) + ((y `) + (((((y `) + x) `) + x) `)) by A3

.= (y `) + x by A20 ;

hence (((x `) + ((x + y) `)) `) + ((y `) + ((x + y) `)) = (y `) + x ; :: thesis: verum

end;
(((x `) + ((x + y) `)) `) + ((y `) + ((x + y) `)) = (((x `) + ((x + y) `)) `) + ((y `) + (((((y `) + x) `) + x) `)) by A3

.= (((x `) + (((((y `) + x) `) + x) `)) `) + ((y `) + (((((y `) + x) `) + x) `)) by A3

.= (y `) + x by A20 ;

hence (((x `) + ((x + y) `)) `) + ((y `) + ((x + y) `)) = (y `) + x ; :: thesis: verum

proof

A23:
for x, y being Element of L holds (x `) + ((x + y) `) = x `
let x, y be Element of L; :: thesis: x + (((x `) + y) `) = x

x + (((x `) + y) `) = ((((x `) + y) `) + x) + (((x `) + y) `) by A1

.= (((x `) + y) `) + x by A8

.= x by A1 ;

hence x + (((x `) + y) `) = x ; :: thesis: verum

end;
x + (((x `) + y) `) = ((((x `) + y) `) + x) + (((x `) + y) `) by A1

.= (((x `) + y) `) + x by A8

.= x by A1 ;

hence x + (((x `) + y) `) = x ; :: thesis: verum

proof

A24:
for x, y being Element of L holds x + ((y + (x `)) `) = x
let x, y be Element of L; :: thesis: (x `) + ((x + y) `) = x `

x ` = (x `) + ((((x `) `) + y) `) by A22

.= (x `) + ((x + y) `) by A19 ;

hence (x `) + ((x + y) `) = x ` ; :: thesis: verum

end;
x ` = (x `) + ((((x `) `) + y) `) by A22

.= (x `) + ((x + y) `) by A19 ;

hence (x `) + ((x + y) `) = x ` ; :: thesis: verum

proof

A25:
for x, y being Element of L holds (x `) + ((y + x) `) = x `
let x, y be Element of L; :: thesis: x + ((y + (x `)) `) = x

x + ((y + (x `)) `) = (((y + (x `)) `) + x) + ((y + (x `)) `) by A11

.= ((y + (x `)) `) + x by A8

.= x by A11 ;

hence x + ((y + (x `)) `) = x ; :: thesis: verum

end;
x + ((y + (x `)) `) = (((y + (x `)) `) + x) + ((y + (x `)) `) by A11

.= ((y + (x `)) `) + x by A8

.= x by A11 ;

hence x + ((y + (x `)) `) = x ; :: thesis: verum

proof

A26:
for x, y being Element of L holds x + (y `) = (y `) + x
let x, y be Element of L; :: thesis: (x `) + ((y + x) `) = x `

x ` = (x `) + ((y + ((x `) `)) `) by A24

.= (x `) + ((y + x) `) by A19 ;

hence (x `) + ((y + x) `) = x ` ; :: thesis: verum

end;
x ` = (x `) + ((y + ((x `) `)) `) by A24

.= (x `) + ((y + x) `) by A19 ;

hence (x `) + ((y + x) `) = x ` ; :: thesis: verum

proof

A27:
for x, y being Element of L holds x + y = y + x
let x, y be Element of L; :: thesis: x + (y `) = (y `) + x

(y `) + x = (((x `) + ((x + y) `)) `) + ((y `) + ((x + y) `)) by A21

.= ((x `) `) + ((y `) + ((x + y) `)) by A23

.= ((x `) `) + (y `) by A25

.= x + (y `) by A19 ;

hence x + (y `) = (y `) + x ; :: thesis: verum

end;
(y `) + x = (((x `) + ((x + y) `)) `) + ((y `) + ((x + y) `)) by A21

.= ((x `) `) + ((y `) + ((x + y) `)) by A23

.= ((x `) `) + (y `) by A25

.= x + (y `) by A19 ;

hence x + (y `) = (y `) + x ; :: thesis: verum

proof

hence
L is join-commutative
by LATTICES:def 4; :: thesis: ( L is Huntington & L is join-associative )
let x, y be Element of L; :: thesis: x + y = y + x

(y `) ` = y by A19;

hence x + y = y + x by A26; :: thesis: verum

end;
(y `) ` = y by A19;

hence x + y = y + x by A26; :: thesis: verum

A28: for x, y, z being Element of L holds (((((x `) + y) `) + z) `) + ((x `) + z) = z + ((x `) + y)

proof

A29:
for x, y being Element of L holds x + ((y `) + x) = (y `) + x
let x, y, z be Element of L; :: thesis: (((((x `) + y) `) + z) `) + ((x `) + z) = z + ((x `) + y)

(((((x `) + y) `) + z) `) + ((x `) + z) = z + ((x `) + ((x `) + y)) by A1

.= z + ((x `) + y) by A2 ;

hence (((((x `) + y) `) + z) `) + ((x `) + z) = z + ((x `) + y) ; :: thesis: verum

end;
(((((x `) + y) `) + z) `) + ((x `) + z) = z + ((x `) + ((x `) + y)) by A1

.= z + ((x `) + y) by A2 ;

hence (((((x `) + y) `) + z) `) + ((x `) + z) = z + ((x `) + y) ; :: thesis: verum

proof

A30:
for x, y being Element of L holds ((x + y) `) + x = (y `) + x
let x, y be Element of L; :: thesis: x + ((y `) + x) = (y `) + x

x + ((y `) + x) = (((((y `) + x) `) + x) `) + ((y `) + x) by A28

.= (y `) + x by A1 ;

hence x + ((y `) + x) = (y `) + x ; :: thesis: verum

end;
x + ((y `) + x) = (((((y `) + x) `) + x) `) + ((y `) + x) by A28

.= (y `) + x by A1 ;

hence x + ((y `) + x) = (y `) + x ; :: thesis: verum

proof

A31:
for x, y being Element of L holds ((x + y) `) + (((y `) + x) `) = (x `) + (((y `) + x) `)
let x, y be Element of L; :: thesis: ((x + y) `) + x = (y `) + x

set Y = (y `) + x;

(y `) + x = x + ((y `) + x) by A29

.= (((((y `) + x) `) + x) `) + x by A3

.= ((x + y) `) + x by A3 ;

hence ((x + y) `) + x = (y `) + x ; :: thesis: verum

end;
set Y = (y `) + x;

(y `) + x = x + ((y `) + x) by A29

.= (((((y `) + x) `) + x) `) + x by A3

.= ((x + y) `) + x by A3 ;

hence ((x + y) `) + x = (y `) + x ; :: thesis: verum

proof

for x, y being Element of L holds (((x `) + (y `)) `) + (((x `) + y) `) = x
let x, y be Element of L; :: thesis: ((x + y) `) + (((y `) + x) `) = (x `) + (((y `) + x) `)

((x + y) `) + (((y `) + x) `) = (((((y `) + x) `) + x) `) + (((y `) + x) `) by A3

.= (x `) + (((y `) + x) `) by A30 ;

hence ((x + y) `) + (((y `) + x) `) = (x `) + (((y `) + x) `) ; :: thesis: verum

end;
((x + y) `) + (((y `) + x) `) = (((((y `) + x) `) + x) `) + (((y `) + x) `) by A3

.= (x `) + (((y `) + x) `) by A30 ;

hence ((x + y) `) + (((y `) + x) `) = (x `) + (((y `) + x) `) ; :: thesis: verum

proof

hence
L is Huntington
by ROBBINS1:def 6; :: thesis: L is join-associative
let x, y be Element of L; :: thesis: (((x `) + (y `)) `) + (((x `) + y) `) = x

(((x `) + (y `)) `) + (((x `) + y) `) = (((y `) + (x `)) `) + (((x `) + y) `) by A27

.= (((x `) + y) `) + (((y `) + (x `)) `) by A27

.= ((x `) `) + (((y `) + (x `)) `) by A31

.= x + (((y `) + (x `)) `) by A19

.= x by A24 ;

hence (((x `) + (y `)) `) + (((x `) + y) `) = x ; :: thesis: verum

end;
(((x `) + (y `)) `) + (((x `) + y) `) = (((y `) + (x `)) `) + (((x `) + y) `) by A27

.= (((x `) + y) `) + (((y `) + (x `)) `) by A27

.= ((x `) `) + (((y `) + (x `)) `) by A31

.= x + (((y `) + (x `)) `) by A19

.= x by A24 ;

hence (((x `) + (y `)) `) + (((x `) + y) `) = x ; :: thesis: verum

A32: for x, y, z being Element of L holds (x + y) + (y + z) = (x + y) + z

proof

for x, y, z being Element of L holds (x + y) + z = x + (y + z)
let x, y, z be Element of L; :: thesis: (x + y) + (y + z) = (x + y) + z

set Y = x + y;

(x + y) + z = (((z `) + (x + y)) `) + (x + y) by A3

.= (((z `) + (x + y)) `) + (y + (x + y)) by A10

.= (x + y) + (y + z) by A1 ;

hence (x + y) + (y + z) = (x + y) + z ; :: thesis: verum

end;
set Y = x + y;

(x + y) + z = (((z `) + (x + y)) `) + (x + y) by A3

.= (((z `) + (x + y)) `) + (y + (x + y)) by A10

.= (x + y) + (y + z) by A1 ;

hence (x + y) + (y + z) = (x + y) + z ; :: thesis: verum

proof

hence
L is join-associative
by LATTICES:def 5; :: thesis: verum
let x, y, z be Element of L; :: thesis: (x + y) + z = x + (y + z)

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

then A33: (x + y) + (z + y) = x + (y + z) by A27;

(x + y) + z = (x + y) + (y + z) by A32

.= x + (y + z) by A27, A33 ;

hence (x + y) + z = x + (y + z) ; :: thesis: verum

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

proof

then
(y + x) + (z + y) = x + (y + z)
;
let x, y, z be Element of L; :: thesis: (x + y) + (z + x) = y + (x + z)

(x + y) + (z + x) = (z + x) + (x + y) by A27

.= (z + x) + y by A32

.= (x + z) + y by A27

.= y + (x + z) by A27 ;

hence (x + y) + (z + x) = y + (x + z) ; :: thesis: verum

end;
(x + y) + (z + x) = (z + x) + (x + y) by A27

.= (z + x) + y by A32

.= (x + z) + y by A27

.= y + (x + z) by A27 ;

hence (x + y) + (z + x) = y + (x + z) ; :: thesis: verum

then A33: (x + y) + (z + y) = x + (y + z) by A27;

(x + y) + z = (x + y) + (y + z) by A32

.= x + (y + z) by A27, A33 ;

hence (x + y) + z = x + (y + z) ; :: thesis: verum

registration

for b_{1} being non empty ComplLLattStr st b_{1} is satisfying_MD_1 & b_{1} is satisfying_MD_2 holds

( b_{1} is join-commutative & b_{1} is join-associative & b_{1} is Huntington )
by Lm4;

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 satisfying_MD_1 & b_{1} is satisfying_MD_2 )
end;

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

coherence for b

( b

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

coherence for b

( b

proof end;

registration

ex b_{1} being preOrthoLattice st

( b_{1} is satisfying_MD_1 & b_{1} is satisfying_MD_2 & b_{1} is satisfying_DN_1 & b_{1} is de_Morgan )
end;

cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like de_Morgan satisfying_DN_1 satisfying_MD_1 satisfying_MD_2 for OrthoLattStr ;

existence ex b

( b

proof end;

registration

for b_{1} being preOrthoLattice st b_{1} is satisfying_MD_1 & b_{1} is satisfying_MD_2 & 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 satisfying_MD_1 & b_{1} is satisfying_MD_2 )
;

end;

cluster non empty Lattice-like de_Morgan satisfying_MD_1 satisfying_MD_2 -> Boolean for OrthoLattStr ;

coherence for b

b

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

coherence for b

( b