:: ROBBINS2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let L be non empty ComplLattStr ;
attr L is satisfying_DN_1 means :Def1: :: ROBBINS2:def 1
for x, y, z, u being Element of L holds (((((x + y) ` ) + z) ` ) + ((x + (((z ` ) + ((z + u) ` )) ` )) ` )) ` = z;
end;

:: deftheorem Def1 defines satisfying_DN_1 ROBBINS2:def 1 :
for L being non empty ComplLattStr 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
cluster TrivComplLat -> satisfying_DN_1 ;
coherence
TrivComplLat is satisfying_DN_1
proof end;
cluster TrivOrtLat -> satisfying_DN_1 ;
coherence
TrivOrtLat is satisfying_DN_1
proof end;
end;

registration
cluster non empty join-commutative join-associative satisfying_DN_1 ComplLattStr ;
existence
ex b1 being non empty ComplLattStr st
( b1 is join-commutative & b1 is join-associative & b1 is satisfying_DN_1 )
proof end;
end;

theorem Th1: :: ROBBINS2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y, z, u being Element of L holds (((x + y) ` ) + ((((z + x) ` ) + (((y ` ) + ((y + u) ` )) ` )) ` )) ` = y
proof end;

theorem Th3: :: ROBBINS2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x being Element of L holds (((x + (x ` )) ` ) + x) ` = x `
proof end;

theorem Th4: :: ROBBINS2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y, z being Element of L holds (((x + y) ` ) + ((((z + x) ` ) + y) ` )) ` = y
proof end;

theorem Th6: :: ROBBINS2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y being Element of L holds (((x + y) ` ) + (((x ` ) + y) ` )) ` = y
proof end;

theorem Th7: :: ROBBINS2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y being Element of L holds (((((x + y) ` ) + x) ` ) + ((x + y) ` )) ` = x
proof end;

theorem Th8: :: ROBBINS2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y being Element of L holds (x + ((((x + y) ` ) + x) ` )) ` = (x + y) `
proof end;

theorem Th9: :: ROBBINS2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y, z being Element of L holds (((((x + y) ` ) + z) ` ) + ((x + z) ` )) ` = z
proof end;

theorem Th10: :: ROBBINS2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y, z being Element of L holds (x + ((((y + z) ` ) + ((y + x) ` )) ` )) ` = (y + x) `
proof end;

theorem Th11: :: ROBBINS2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y, z being Element of L holds (((((((x + y) ` ) + z) ` ) + (((x ` ) + y) ` )) ` ) + y) ` = ((x ` ) + y) `
proof end;

theorem Th12: :: ROBBINS2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y, z being Element of L holds (x + ((((y + z) ` ) + ((z + x) ` )) ` )) ` = (z + x) `
proof end;

theorem Th13: :: ROBBINS2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y, z, u being Element of L holds (((x + y) ` ) + ((((z + x) ` ) + (((y ` ) + ((u + y) ` )) ` )) ` )) ` = y
proof end;

theorem Th14: :: ROBBINS2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y being Element of L holds (x + y) ` = (y + x) `
proof end;

theorem Th15: :: ROBBINS2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y, z being Element of L holds (((((x + y) ` ) + ((y + z) ` )) ` ) + z) ` = (y + z) `
proof end;

theorem Th16: :: ROBBINS2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y, z being Element of L holds (((x + ((((x + y) ` ) + z) ` )) ` ) + z) ` = (((x + y) ` ) + z) `
proof end;

theorem Th17: :: ROBBINS2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y being Element of L holds (((((x + y) ` ) + x) ` ) + y) ` = (y + y) `
proof end;

theorem Th18: :: ROBBINS2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y being Element of L holds ((x ` ) + ((y + x) ` )) ` = x
proof end;

theorem Th19: :: ROBBINS2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y being Element of L holds (((x + y) ` ) + (y ` )) ` = y
proof end;

theorem Th20: :: ROBBINS2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y being Element of L holds (x + ((y + (x ` )) ` )) ` = x `
proof end;

theorem Th21: :: ROBBINS2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x being Element of L holds (x + x) ` = x `
proof end;

theorem Th22: :: ROBBINS2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y being Element of L holds (((((x + y) ` ) + x) ` ) + y) ` = y `
proof end;

theorem Th23: :: ROBBINS2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x being Element of L holds (x ` ) ` = x
proof end;

theorem Th24: :: ROBBINS2:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y being Element of L holds ((((x + y) ` ) + x) ` ) + y = (y ` ) `
proof end;

theorem Th25: :: ROBBINS2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y being Element of L holds ((x + y) ` ) ` = y + x
proof end;

theorem Th26: :: ROBBINS2:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y, z being Element of L holds x + ((((y + z) ` ) + ((y + x) ` )) ` ) = ((y + x) ` ) `
proof end;

theorem Th27: :: ROBBINS2:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y being Element of L holds x + y = y + x
proof end;

Lm1: for L being non empty satisfying_DN_1 ComplLattStr holds L is join-commutative
proof end;

registration
cluster non empty satisfying_DN_1 -> non empty join-commutative ComplLattStr ;
coherence
for b1 being non empty ComplLattStr st b1 is satisfying_DN_1 holds
b1 is join-commutative by Lm1;
end;

theorem Th28: :: ROBBINS2:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y being Element of L holds ((((x + y) ` ) + x) ` ) + y = y
proof end;

theorem :: ROBBINS2:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y being Element of L holds ((((x + y) ` ) + y) ` ) + x = x by Th28;

theorem :: ROBBINS2:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y being Element of L holds x + ((((y + x) ` ) + y) ` ) = x by Th28;

theorem Th31: :: ROBBINS2:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y being Element of L holds ((x + (y ` )) ` ) + (((y ` ) + y) ` ) = (x + (y ` )) `
proof end;

theorem Th32: :: ROBBINS2:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y being Element of L holds ((x + y) ` ) + ((y + (y ` )) ` ) = (x + y) `
proof end;

theorem :: ROBBINS2:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y being Element of L holds ((x + y) ` ) + (((y ` ) + y) ` ) = (x + y) ` by Th32;

theorem Th34: :: ROBBINS2:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y being Element of L holds ((((x + (y ` )) ` ) ` ) + y) ` = ((y ` ) + y) `
proof end;

theorem Th35: :: ROBBINS2:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y being Element of L holds ((x + (y ` )) + y) ` = ((y ` ) + y) `
proof end;

theorem Th36: :: ROBBINS2:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y, z being Element of L holds ((((((x + (y ` )) + z) ` ) + y) ` ) + (((y ` ) + y) ` )) ` = y
proof end;

theorem Th37: :: ROBBINS2:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y, z being Element of L holds x + ((((y + z) ` ) + ((y + x) ` )) ` ) = y + x
proof end;

theorem Th38: :: ROBBINS2:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y, z being Element of L holds x + ((y + ((((z + y) ` ) + x) ` )) ` ) = ((z + y) ` ) + x
proof end;

theorem :: ROBBINS2:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y, z being Element of L holds x + ((((y + x) ` ) + ((y + z) ` )) ` ) = y + x by Th37;

theorem Th40: :: ROBBINS2:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y, z being Element of L holds ((((x + y) ` ) + ((((x + y) ` ) + ((x + z) ` )) ` )) ` ) + y = y
proof end;

theorem Th41: :: ROBBINS2:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y, z being Element of L holds (((((x + (y ` )) + z) ` ) + y) ` ) ` = y
proof end;

theorem Th42: :: ROBBINS2:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y, z being Element of L holds x + (((y + (x ` )) + z) ` ) = x
proof end;

theorem Th43: :: ROBBINS2:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y, z being Element of L holds (x ` ) + (((y + x) + z) ` ) = x `
proof end;

theorem Th44: :: ROBBINS2:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y being Element of L holds ((x + y) ` ) + x = x + (y ` )
proof end;

theorem Th45: :: ROBBINS2:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y being Element of L holds (x + ((x + (y ` )) ` )) ` = (x + y) `
proof end;

theorem Th46: :: ROBBINS2:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y, z being Element of L holds ((((x + y) ` ) + (x + z)) ` ) + y = y
proof end;

theorem Th47: :: ROBBINS2:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y, z being Element of L holds ((((((x + y) ` ) + z) ` ) + (((x ` ) + y) ` )) ` ) + y = (((x ` ) + y) ` ) `
proof end;

theorem Th48: :: ROBBINS2:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y, z being Element of L holds ((((((x + y) ` ) + z) ` ) + (((x ` ) + y) ` )) ` ) + y = (x ` ) + y
proof end;

theorem Th49: :: ROBBINS2:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y, z being Element of L holds ((x ` ) ` ) + (y + z) = (y + x) + (y + z)
proof end;

theorem Th53: :: ROBBINS2:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y, z being Element of L holds (x + y) + (x + z) = y + (x + z)
proof end;

theorem :: ROBBINS2:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y, z being Element of L holds (x + y) + (x + z) = z + (x + y) by Th53;

theorem Th55: :: ROBBINS2:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y, z being Element of L holds x + (y + z) = z + (y + x)
proof end;

theorem :: ROBBINS2:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
for x, y, z being Element of L holds x + (y + z) = y + (z + x) by Th55;

theorem :: ROBBINS2:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty satisfying_DN_1 ComplLattStr
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 ComplLattStr holds L is join-associative
proof end;

Lm3: for L being non empty satisfying_DN_1 ComplLattStr holds L is Robbins
proof end;

registration
cluster non empty satisfying_DN_1 -> non empty join-associative ComplLattStr ;
coherence
for b1 being non empty ComplLattStr st b1 is satisfying_DN_1 holds
b1 is join-associative by Lm2;
cluster non empty satisfying_DN_1 -> non empty Robbins ComplLattStr ;
coherence
for b1 being non empty ComplLattStr st b1 is satisfying_DN_1 holds
b1 is Robbins by Lm3;
end;

theorem Th58: :: ROBBINS2:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty ComplLattStr
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being non empty ComplLattStr st L is join-commutative & L is join-associative & L is Robbins holds
L is satisfying_DN_1
proof end;

registration
cluster non empty join-commutative join-associative Robbins -> non empty join-commutative join-associative Robbins satisfying_DN_1 ComplLattStr ;
coherence
for b1 being non empty ComplLattStr st b1 is join-commutative & b1 is join-associative & b1 is Robbins holds
b1 is satisfying_DN_1 by Th59;
end;

registration
cluster join-commutative join-associative Robbins de_Morgan satisfying_DN_1 OrthoLattStr ;
existence
ex b1 being preOrthoLattice st
( b1 is satisfying_DN_1 & b1 is de_Morgan )
proof end;
end;

registration
cluster de_Morgan satisfying_DN_1 -> Boolean OrthoLattStr ;
coherence
for b1 being preOrthoLattice st b1 is satisfying_DN_1 & b1 is de_Morgan holds
b1 is Boolean
proof end;
cluster Boolean well-complemented -> join-commutative join-associative Robbins well-complemented satisfying_DN_1 OrthoLattStr ;
coherence
for b1 being well-complemented preOrthoLattice st b1 is Boolean holds
b1 is satisfying_DN_1
proof end;
end;

definition
let L be non empty ComplLattStr ;
attr L is satisfying_MD_1 means :Def2: :: ROBBINS2:def 2
for x, y being Element of L holds (((x ` ) + y) ` ) + x = x;
attr L is satisfying_MD_2 means :Def3: :: ROBBINS2:def 3
for x, y, z being Element of L holds (((x ` ) + y) ` ) + (z + y) = y + (z + x);
end;

:: deftheorem Def2 defines satisfying_MD_1 ROBBINS2:def 2 :
for L being non empty ComplLattStr holds
( L is satisfying_MD_1 iff for x, y being Element of L holds (((x ` ) + y) ` ) + x = x );

:: deftheorem Def3 defines satisfying_MD_2 ROBBINS2:def 3 :
for L being non empty ComplLattStr 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
let L be non empty ComplLattStr ; :: 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
proof
let x, y be Element of L; :: thesis: (x ` ) + ((x ` ) + y) = (x ` ) + y
set X = (x ` ) + y;
(((x ` ) + y) ` ) + x = x by A1, Def2;
hence (x ` ) + ((x ` ) + y) = (x ` ) + y by A1, Def2; :: thesis: verum
end;
A3: for x, y, z being Element of L holds (((((x ` ) + y) ` ) + z) ` ) + ((x ` ) + z) = z + ((x ` ) + y)
proof
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, Def3
.= z + ((x ` ) + y) by A2 ;
hence (((((x ` ) + y) ` ) + z) ` ) + ((x ` ) + z) = z + ((x ` ) + y) ; :: thesis: verum
end;
A4: for x, y, z being Element of L holds (((x ` ) + y) ` ) + ((((x ` ) + z) ` ) + y) = y + x
proof
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, Def3
.= y + x by A1, Def2 ;
hence (((x ` ) + y) ` ) + ((((x ` ) + z) ` ) + y) = y + x ; :: thesis: verum
end;
A5: for x, y, z being Element of L holds (((x ` ) + ((((y + x) ` ) + z) ` )) ` ) + (y + ((((y + x) ` ) + z) ` )) = y + x
proof
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, Def3
.= y + x by A1, Def2 ;
hence (((x ` ) + ((((y + x) ` ) + z) ` )) ` ) + (y + ((((y + x) ` ) + z) ` )) = y + x ; :: thesis: verum
end;
A6: for x, y being Element of L holds (((x ` ) + y) ` ) + y = y + x
proof
let x, y be Element of L; :: thesis: (((x ` ) + y) ` ) + y = y + x
set X = (x ` ) + y;
A7: (((x ` ) + y) ` ) + ((((x ` ) + y) ` ) + y) = y + ((((x ` ) + y) ` ) + x) by A1, Def3;
(((x ` ) + y) ` ) + y = (((x ` ) + y) ` ) + ((((x ` ) + y) ` ) + y) by A2
.= y + x by A1, A7, Def2 ;
hence (((x ` ) + y) ` ) + y = y + x ; :: thesis: verum
end;
A8: for x, y being Element of L holds x + (y + (y + x)) = y + x
proof
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, Def3
.= y + x by A1, Def2 ;
hence x + (y + (y + x)) = y + x ; :: thesis: verum
end;
A9: for x, y being Element of L holds x + ((y ` ) + x) = (y ` ) + x
proof
let x, y be Element of L; :: thesis: x + ((y ` ) + x) = (y ` ) + x
x + ((y ` ) + x) = (((((y ` ) + x) ` ) + x) ` ) + ((y ` ) + x) by A3
.= (y ` ) + x by A1, Def2 ;
hence x + ((y ` ) + x) = (y ` ) + x ; :: thesis: verum
end;
A10: for x being Element of L holds x + x = x
proof
let x be Element of L; :: thesis: x + x = x
x + x = (((x ` ) + x) ` ) + x by A6
.= x by A1, Def2 ;
hence x + x = x ; :: thesis: verum
end;
A11: for x, y being Element of L holds x + (x + y) = x + y
proof
let x, y be Element of L; :: thesis: x + (x + y) = x + y
x + (x + y) = (((y ` ) + x) ` ) + (x + x) by A1, Def3
.= (((y ` ) + x) ` ) + x by A10
.= x + y by A6 ;
hence x + (x + y) = x + y ; :: thesis: verum
end;
A12: for x, y being Element of L holds (x + y) + y = x + y
proof
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 A6
.= (((y ` ) + (x + y)) ` ) + (x + (x + y)) by A11
.= (x + y) + (x + y) by A1, Def3
.= x + y by A10 ;
hence (x + y) + y = x + y ; :: thesis: verum
end;
A13: for x being Element of L holds ((x ` ) ` ) + x = x
proof
let x be Element of L; :: thesis: ((x ` ) ` ) + x = x
(((x ` ) + (x ` )) ` ) + x = x by A1, Def2;
hence ((x ` ) ` ) + x = x by A10; :: thesis: verum
end;
A14: for x, y being Element of L holds x + (y + x) = y + x
proof
let x, y be Element of L; :: thesis: x + (y + x) = y + x
x + (y + x) = x + (y + (y + x)) by A11
.= y + x by A8 ;
hence x + (y + x) = y + x ; :: thesis: verum
end;
A15: for x, y being Element of L holds x + (((x ` ) ` ) + y) = x + y
proof
let x, y be Element of L; :: thesis: x + (((x ` ) ` ) + y) = x + y
x + (((x ` ) ` ) + y) = (((y ` ) + x) ` ) + (((x ` ) ` ) + x) by A1, Def3
.= (((y ` ) + x) ` ) + x by A13
.= x + y by A6 ;
hence x + (((x ` ) ` ) + y) = x + y ; :: thesis: verum
end;
A16: for x, y being Element of L holds (x + y) + x = x + y
proof
let x, y be Element of L; :: thesis: (x + y) + x = x + y
(x + y) + x = ((((y ` ) + x) ` ) + x) + x by A6
.= (((y ` ) + x) ` ) + x by A12
.= x + y by A6 ;
hence (x + y) + x = x + y ; :: thesis: verum
end;
A17: for x, y, z being Element of L holds (x + y) + (y + z) = (x + y) + z
proof
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 A6
.= (((z ` ) + (x + y)) ` ) + (y + (x + y)) by A14
.= (x + y) + (y + z) by A1, Def3 ;
hence (x + y) + (y + z) = (x + y) + z ; :: thesis: verum
end;
A18: for x, y being Element of L holds ((x + (y ` )) ` ) + y = y
proof
let x, y be Element of L; :: thesis: ((x + (y ` )) ` ) + y = y
((x + (y ` )) ` ) + y = (((y ` ) + (x + (y ` ))) ` ) + y by A14
.= y by A1, Def2 ;
hence ((x + (y ` )) ` ) + y = y ; :: thesis: verum
end;
A19: for x being Element of L holds x + ((x ` ) ` ) = x
proof
let x be Element of L; :: thesis: x + ((x ` ) ` ) = x
x + ((x ` ) ` ) = (((x ` ) ` ) + x) + ((x ` ) ` ) by A13
.= ((x ` ) ` ) + x by A16
.= x by A13 ;
hence x + ((x ` ) ` ) = x ; :: thesis: verum
end;
A20: for x, y being Element of L holds x + (((x ` ) + y) ` ) = x
proof
let x, y be Element of L; :: thesis: x + (((x ` ) + y) ` ) = x
x + (((x ` ) + y) ` ) = ((((x ` ) + y) ` ) + x) + (((x ` ) + y) ` ) by A1, Def2
.= (((x ` ) + y) ` ) + x by A16
.= x by A1, Def2 ;
hence x + (((x ` ) + y) ` ) = x ; :: thesis: verum
end;
A21: for x, y being Element of L holds x + ((y + (x ` )) ` ) = x
proof
let x, y be Element of L; :: thesis: x + ((y + (x ` )) ` ) = x
x + ((y + (x ` )) ` ) = (((y + (x ` )) ` ) + x) + ((y + (x ` )) ` ) by A18
.= ((y + (x ` )) ` ) + x by A16
.= x by A18 ;
hence x + ((y + (x ` )) ` ) = x ; :: thesis: verum
end;
A22: for x, y being Element of L holds (((x ` ) + ((x + y) ` )) ` ) + ((y ` ) + ((x + y) ` )) = (y ` ) + x
proof
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 A6
.= (((x ` ) + (((((y ` ) + x) ` ) + x) ` )) ` ) + ((y ` ) + (((((y ` ) + x) ` ) + x) ` )) by A6
.= (y ` ) + x by A5 ;
hence (((x ` ) + ((x + y) ` )) ` ) + ((y ` ) + ((x + y) ` )) = (y ` ) + x ; :: thesis: verum
end;
A23: for x, y being Element of L holds ((x + y) ` ) + x = (y ` ) + x
proof
let x, y be Element of L; :: thesis: ((x + y) ` ) + x = (y ` ) + x
set Y = (y ` ) + x;
(y ` ) + x = x + ((y ` ) + x) by A9
.= (((((y ` ) + x) ` ) + x) ` ) + x by A6
.= ((x + y) ` ) + x by A6 ;
hence ((x + y) ` ) + x = (y ` ) + x ; :: thesis: verum
end;
A24: for x, y being Element of L holds ((x + y) ` ) + (((y ` ) + x) ` ) = (x ` ) + (((y ` ) + x) ` )
proof
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 A6
.= (x ` ) + (((y ` ) + x) ` ) by A23 ;
hence ((x + y) ` ) + (((y ` ) + x) ` ) = (x ` ) + (((y ` ) + x) ` ) ; :: thesis: verum
end;
A25: for x being Element of L holds x + ((((x ` ) ` ) ` ) ` ) = x
proof
let x be Element of L; :: thesis: x + ((((x ` ) ` ) ` ) ` ) = x
x + ((((x ` ) ` ) ` ) ` ) = x + (((x ` ) ` ) + ((((x ` ) ` ) ` ) ` )) by A15
.= x + ((x ` ) ` ) by A19
.= x by A19 ;
hence x + ((((x ` ) ` ) ` ) ` ) = x ; :: thesis: verum
end;
A26: for x being Element of L holds ((x ` ) ` ) ` = x `
proof
let x be Element of L; :: thesis: ((x ` ) ` ) ` = x `
((x ` ) ` ) ` = ((x + ((((x ` ) ` ) ` ) ` )) ` ) + (((x ` ) ` ) ` ) by A18
.= (x ` ) + (((x ` ) ` ) ` ) by A25
.= x ` by A19 ;
hence ((x ` ) ` ) ` = x ` ; :: thesis: verum
end;
A27: for x, y being Element of L holds x + ((y ` ) ` ) = x + y
proof
let x, y be Element of L; :: thesis: x + ((y ` ) ` ) = x + y
x + y = (((y ` ) + x) ` ) + ((((y ` ) + x) ` ) + x) by A4
.= (((y ` ) + x) ` ) + ((((((y ` ) ` ) ` ) + x) ` ) + x) by A26
.= (((((y ` ) ` ) ` ) + x) ` ) + ((((((y ` ) ` ) ` ) + x) ` ) + x) by A26
.= x + ((y ` ) ` ) by A4 ;
hence x + ((y ` ) ` ) = x + y ; :: thesis: verum
end;
A28: for x being Element of L holds (x ` ) ` = x
proof
let x be Element of L; :: thesis: (x ` ) ` = x
(x ` ) ` = (((((x ` ) ` ) ` ) + ((x ` ) ` )) ` ) + ((x ` ) ` ) by A1, Def2
.= (((x ` ) + ((x ` ) ` )) ` ) + ((x ` ) ` ) by A26
.= (((x ` ) + ((x ` ) ` )) ` ) + x by A27
.= x by A1, Def2 ;
hence (x ` ) ` = x ; :: thesis: verum
end;
A29: for x, y being Element of L holds (x ` ) + ((y + x) ` ) = x `
proof
let x, y be Element of L; :: thesis: (x ` ) + ((y + x) ` ) = x `
x ` = (x ` ) + ((y + ((x ` ) ` )) ` ) by A21
.= (x ` ) + ((y + x) ` ) by A28 ;
hence (x ` ) + ((y + x) ` ) = x ` ; :: thesis: verum
end;
A30: for x, y being Element of L holds (x ` ) + ((x + y) ` ) = x `
proof
let x, y be Element of L; :: thesis: (x ` ) + ((x + y) ` ) = x `
x ` = (x ` ) + ((((x ` ) ` ) + y) ` ) by A20
.= (x ` ) + ((x + y) ` ) by A28 ;
hence (x ` ) + ((x + y) ` ) = x ` ; :: thesis: verum
end;
A31: for x, y being Element of L holds x + (y ` ) = (y ` ) + x
proof
let x, y be Element of L; :: thesis: x + (y ` ) = (y ` ) + x
(y ` ) + x = (((x ` ) + ((x + y) ` )) ` ) + ((y ` ) + ((x + y) ` )) by A22
.= ((x ` ) ` ) + ((y ` ) + ((x + y) ` )) by A30
.= ((x ` ) ` ) + (y ` ) by A29
.= x + (y ` ) by A28 ;
hence x + (y ` ) = (y ` ) + x ; :: thesis: verum
end;
A32: for x, y being Element of L holds x + y = y + x
proof
let x, y be Element of L; :: thesis: x + y = y + x
(y ` ) ` = y by A28;
hence x + y = y + x by A31; :: thesis: verum
end;
hence L is join-commutative by LATTICES:def 4; :: thesis: ( L is Huntington & L is join-associative )
for x, y being Element of L holds (((x ` ) + (y ` )) ` ) + (((x ` ) + y) ` ) = x
proof
let x, y be Element of L; :: thesis: (((x ` ) + (y ` )) ` ) + (((x ` ) + y) ` ) = x
(((x ` ) + (y ` )) ` ) + (((x ` ) + y) ` ) = (((y ` ) + (x ` )) ` ) + (((x ` ) + y) ` ) by A32
.= (((x ` ) + y) ` ) + (((y ` ) + (x ` )) ` ) by A32
.= ((x ` ) ` ) + (((y ` ) + (x ` )) ` ) by A24
.= x + (((y ` ) + (x ` )) ` ) by A28
.= x by A21 ;
hence (((x ` ) + (y ` )) ` ) + (((x ` ) + y) ` ) = x ; :: thesis: verum
end;
hence L is Huntington by ROBBINS1:def 6; :: thesis: L is join-associative
for x, y, z being Element of L holds (x + y) + z = x + (y + z)
proof
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)
proof
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 A32
.= (z + x) + y by A17
.= (x + z) + y by A32
.= y + (x + z) by A32 ;
hence (x + y) + (z + x) = y + (x + z) ; :: thesis: verum
end;
then (y + x) + (z + y) = x + (y + z) ;
then A33: (x + y) + (z + y) = x + (y + z) by A32;
(x + y) + z = (x + y) + (y + z) by A17
.= x + (y + z) by A32, A33 ;
hence (x + y) + z = x + (y + z) ; :: thesis: verum
end;
hence L is join-associative by LATTICES:def 5; :: thesis: verum
end;

registration
cluster non empty satisfying_MD_1 satisfying_MD_2 -> non empty join-commutative join-associative Huntington ComplLattStr ;
coherence
for b1 being non empty ComplLattStr st b1 is satisfying_MD_1 & b1 is satisfying_MD_2 holds
( b1 is join-commutative & b1 is join-associative & b1 is Huntington ) by Lm4;
cluster non empty join-commutative join-associative Huntington -> non empty satisfying_MD_1 satisfying_MD_2 ComplLattStr ;
coherence
for b1 being non empty ComplLattStr st b1 is join-commutative & b1 is join-associative & b1 is Huntington holds
( b1 is satisfying_MD_1 & b1 is satisfying_MD_2 )
proof end;
end;

registration
cluster join-commutative join-associative Boolean Robbins Huntington de_Morgan satisfying_DN_1 satisfying_MD_1 satisfying_MD_2 OrthoLattStr ;
existence
ex b1 being preOrthoLattice st
( b1 is satisfying_MD_1 & b1 is satisfying_MD_2 & b1 is satisfying_DN_1 & b1 is de_Morgan )
proof end;
end;

registration
cluster de_Morgan satisfying_MD_1 satisfying_MD_2 -> Boolean OrthoLattStr ;
coherence
for b1 being preOrthoLattice st b1 is satisfying_MD_1 & b1 is satisfying_MD_2 & b1 is de_Morgan holds
b1 is Boolean
proof end;
cluster Boolean well-complemented -> join-commutative join-associative Huntington well-complemented satisfying_MD_1 satisfying_MD_2 OrthoLattStr ;
coherence
for b1 being well-complemented preOrthoLattice st b1 is Boolean holds
( b1 is satisfying_MD_1 & b1 is satisfying_MD_2 )
proof end;
end;