:: ROBBINS2 semantic presentation begin definition let L be non empty ComplLLattStr ; attrL 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 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 cluster TrivComplLat -> satisfying_DN_1 ; coherence TrivComplLat is satisfying_DN_1 proof let x, y, z, u be Element of TrivComplLat; :: according to ROBBINS2:def_1 ::_thesis: (((((x + y) `) + z) `) + ((x + (((z `) + ((z + u) `)) `)) `)) ` = z thus (((((x + y) `) + z) `) + ((x + (((z `) + ((z + u) `)) `)) `)) ` = z by STRUCT_0:def_10; ::_thesis: verum end; cluster TrivOrtLat -> satisfying_DN_1 ; coherence TrivOrtLat is satisfying_DN_1 proof let x, y, z, u be Element of TrivOrtLat; :: according to ROBBINS2:def_1 ::_thesis: (((((x + y) `) + z) `) + ((x + (((z `) + ((z + u) `)) `)) `)) ` = z thus (((((x + y) `) + z) `) + ((x + (((z `) + ((z + u) `)) `)) `)) ` = z by STRUCT_0:def_10; ::_thesis: verum end; end; registration cluster non empty join-commutative join-associative satisfying_DN_1 for ComplLLattStr ; existence ex b1 being non empty ComplLLattStr st ( b1 is join-commutative & b1 is join-associative & b1 is satisfying_DN_1 ) proof take TrivComplLat ; ::_thesis: ( TrivComplLat is join-commutative & TrivComplLat is join-associative & TrivComplLat is satisfying_DN_1 ) thus ( TrivComplLat is join-commutative & TrivComplLat is join-associative & TrivComplLat is satisfying_DN_1 ) ; ::_thesis: verum end; 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 proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z, u, v being Element of L holds (((x + y) `) + ((((((z + u) `) + x) `) + (((y `) + ((y + v) `)) `)) `)) ` = y let x, y, z, u, v be Element of L; ::_thesis: (((x + y) `) + ((((((z + u) `) + x) `) + (((y `) + ((y + v) `)) `)) `)) ` = y set X = (((z + u) `) + x) ` ; set Y = (z + (((x `) + ((x + u) `)) `)) ` ; set Z = y; set U = v; (((((((((z + u) `) + x) `) + ((z + (((x `) + ((x + u) `)) `)) `)) `) + y) `) + ((((((z + u) `) + x) `) + (((y `) + ((y + v) `)) `)) `)) ` = y by Def1; hence (((x + y) `) + ((((((z + u) `) + x) `) + (((y `) + ((y + v) `)) `)) `)) ` = y by Def1; ::_thesis: verum 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 proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z, u being Element of L holds (((x + y) `) + ((((z + x) `) + (((y `) + ((y + u) `)) `)) `)) ` = y let x, y, z, u be Element of L; ::_thesis: (((x + y) `) + ((((z + x) `) + (((y `) + ((y + u) `)) `)) `)) ` = y set v = the Element of L; (((x + z) `) + ((((((y + u) `) + x) `) + (((z `) + ((z + the Element of L) `)) `)) `)) ` = z by Th1; hence (((x + y) `) + ((((z + x) `) + (((y `) + ((y + u) `)) `)) `)) ` = y by Th1; ::_thesis: verum 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 ` proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x being Element of L holds (((x + (x `)) `) + x) ` = x ` let x be Element of L; ::_thesis: (((x + (x `)) `) + x) ` = x ` set y = the Element of L; set V = (x + the Element of L) ` ; (((x + (x `)) `) + ((((((((x `) `) + the Element of L) `) + x) `) + ((((x `) `) + (((x `) + ((x + the Element of L) `)) `)) `)) `)) ` = x ` by Th1; hence (((x + (x `)) `) + x) ` = x ` by Def1; ::_thesis: verum 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 proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z, u being Element of L holds (((x + y) `) + ((((z + x) `) + ((((((y + (y `)) `) + y) `) + ((y + u) `)) `)) `)) ` = y let x, y, z, u be Element of L; ::_thesis: (((x + y) `) + ((((z + x) `) + ((((((y + (y `)) `) + y) `) + ((y + u) `)) `)) `)) ` = y (((y + (y `)) `) + y) ` = y ` by Th3; hence (((x + y) `) + ((((z + x) `) + ((((((y + (y `)) `) + y) `) + ((y + u) `)) `)) `)) ` = y by Th2; ::_thesis: verum 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 proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds (((x + y) `) + ((((z + x) `) + y) `)) ` = y let x, y, z be Element of L; ::_thesis: (((x + y) `) + ((((z + x) `) + y) `)) ` = y set u = the Element of L; set U = ((y `) + ((y + the Element of L) `)) ` ; (((x + y) `) + ((((z + x) `) + ((((((y + (y `)) `) + y) `) + ((y + (((y `) + ((y + the Element of L) `)) `)) `)) `)) `)) ` = y by Th4; hence (((x + y) `) + ((((z + x) `) + y) `)) ` = y by Def1; ::_thesis: verum 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 proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds (((x + y) `) + (((x `) + y) `)) ` = y let x, y be Element of L; ::_thesis: (((x + y) `) + (((x `) + y) `)) ` = y set Z = (x + (x `)) ` ; (((x + y) `) + ((((((x + (x `)) `) + x) `) + y) `)) ` = y by Th5; hence (((x + y) `) + (((x `) + y) `)) ` = y by Th3; ::_thesis: verum 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 proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds (((((x + y) `) + x) `) + ((x + y) `)) ` = x let x, y be Element of L; ::_thesis: (((((x + y) `) + x) `) + ((x + y) `)) ` = x set X = (x + y) ` ; (((((x + y) `) + x) `) + ((((x + ((x + y) `)) `) + ((((((x + (x `)) `) + x) `) + ((x + y) `)) `)) `)) ` = x by Th4; hence (((((x + y) `) + x) `) + ((x + y) `)) ` = x by Th5; ::_thesis: verum 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) ` proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds (x + ((((x + y) `) + x) `)) ` = (x + y) ` let x, y be Element of L; ::_thesis: (x + ((((x + y) `) + x) `)) ` = (x + y) ` set X = (x + y) ` ; set Y = x; (((((((x + y) `) + x) `) + ((x + y) `)) `) + ((((x + y) `) + x) `)) ` = (x + y) ` by Th7; hence (x + ((((x + y) `) + x) `)) ` = (x + y) ` by Th7; ::_thesis: verum 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 proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds (((((x + y) `) + z) `) + ((x + z) `)) ` = z let x, y, z be Element of L; ::_thesis: (((((x + y) `) + z) `) + ((x + z) `)) ` = z set X = (x + y) ` ; set Y = z; set Z = (((x + y) `) + x) ` ; (((((x + y) `) + z) `) + ((((((((x + y) `) + x) `) + ((x + y) `)) `) + z) `)) ` = z by Th5; hence (((((x + y) `) + z) `) + ((x + z) `)) ` = z by Th7; ::_thesis: verum 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) ` proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds (x + ((((y + z) `) + ((y + x) `)) `)) ` = (y + x) ` let x, y, z be Element of L; ::_thesis: (x + ((((y + z) `) + ((y + x) `)) `)) ` = (y + x) ` set Z = (y + x) ` ; set X = (y + z) ` ; set Y = x; (((((((y + z) `) + x) `) + ((y + x) `)) `) + ((((y + z) `) + ((y + x) `)) `)) ` = (y + x) ` by Th9; hence (x + ((((y + z) `) + ((y + x) `)) `)) ` = (y + x) ` by Th9; ::_thesis: verum 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) ` proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds (((((((x + y) `) + z) `) + (((x `) + y) `)) `) + y) ` = ((x `) + y) ` let x, y, z be Element of L; ::_thesis: (((((((x + y) `) + z) `) + (((x `) + y) `)) `) + y) ` = ((x `) + y) ` set X = (x + y) ` ; set Z = ((x `) + y) ` ; set Y = z; (((((((x + y) `) + z) `) + (((x `) + y) `)) `) + ((((x + y) `) + (((x `) + y) `)) `)) ` = ((x `) + y) ` by Th9; hence (((((((x + y) `) + z) `) + (((x `) + y) `)) `) + y) ` = ((x `) + y) ` by Th6; ::_thesis: verum 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) ` proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds (x + ((((y + z) `) + ((z + x) `)) `)) ` = (z + x) ` let x, y, z be Element of L; ::_thesis: (x + ((((y + z) `) + ((z + x) `)) `)) ` = (z + x) ` set Y = z; set Z = (((y + x) `) + ((y + z) `)) ` ; (x + ((((z + ((((y + x) `) + ((y + z) `)) `)) `) + ((z + x) `)) `)) ` = (z + x) ` by Th10; hence (x + ((((y + z) `) + ((z + x) `)) `)) ` = (z + x) ` by Th10; ::_thesis: verum 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 proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z, u being Element of L holds (((x + y) `) + ((((z + x) `) + (((y `) + ((u + y) `)) `)) `)) ` = y let x, y, z, u be Element of L; ::_thesis: (((x + y) `) + ((((z + x) `) + (((y `) + ((u + y) `)) `)) `)) ` = y set U = (((u + z) `) + ((u + y) `)) ` ; (((x + y) `) + ((((z + x) `) + (((y `) + ((y + ((((u + z) `) + ((u + y) `)) `)) `)) `)) `)) ` = y by Th2; hence (((x + y) `) + ((((z + x) `) + (((y `) + ((u + y) `)) `)) `)) ` = y by Th10; ::_thesis: verum 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) ` proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds (x + y) ` = (y + x) ` let x, y be Element of L; ::_thesis: (x + y) ` = (y + x) ` set Z = y; set X = x; set Y = (y + x) ` ; (((((y + x) `) + y) `) + ((y + x) `)) ` = y by Th7; hence (x + y) ` = (y + x) ` by Th12; ::_thesis: verum 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) ` proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds (((((x + y) `) + ((y + z) `)) `) + z) ` = (y + z) ` let x, y, z be Element of L; ::_thesis: (((((x + y) `) + ((y + z) `)) `) + z) ` = (y + z) ` set Y = (((x + y) `) + ((y + z) `)) ` ; (z + ((((x + y) `) + ((y + z) `)) `)) ` = (((((x + y) `) + ((y + z) `)) `) + z) ` by Th14; hence (((((x + y) `) + ((y + z) `)) `) + z) ` = (y + z) ` by Th12; ::_thesis: verum 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) ` proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds (((x + ((((x + y) `) + z) `)) `) + z) ` = (((x + y) `) + z) ` let x, y, z be Element of L; ::_thesis: (((x + ((((x + y) `) + z) `)) `) + z) ` = (((x + y) `) + z) ` set X = (((x + y) `) + x) ` ; set Y = (x + y) ` ; (((((x + y) `) + x) `) + ((x + y) `)) ` = x by Th7; hence (((x + ((((x + y) `) + z) `)) `) + z) ` = (((x + y) `) + z) ` by Th15; ::_thesis: verum 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) ` proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds (((((x + y) `) + x) `) + y) ` = (y + y) ` let x, y be Element of L; ::_thesis: (((((x + y) `) + x) `) + y) ` = (y + y) ` set X = (x + y) ` ; (((x + y) `) + ((((((x + y) `) + x) `) + y) `)) ` = y by Th5; hence (((((x + y) `) + x) `) + y) ` = (y + y) ` by Th16; ::_thesis: verum 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 proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds ((x `) + ((y + x) `)) ` = x let x, y be Element of L; ::_thesis: ((x `) + ((y + x) `)) ` = x set X = (y + x) ` ; (((y + x) `) + (((((x `) + y) `) + (((x `) + ((y + x) `)) `)) `)) ` = x by Th13; hence ((x `) + ((y + x) `)) ` = x by Th10; ::_thesis: verum 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 proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds (((x + y) `) + (y `)) ` = y let x, y be Element of L; ::_thesis: (((x + y) `) + (y `)) ` = y ((y `) + ((x + y) `)) ` = y by Th18; hence (((x + y) `) + (y `)) ` = y by Th14; ::_thesis: verum 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 ` proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds (x + ((y + (x `)) `)) ` = x ` let x, y be Element of L; ::_thesis: (x + ((y + (x `)) `)) ` = x ` set Z = x ` ; set X = y; set Y = x; (((((y + x) `) + (x `)) `) + ((y + (x `)) `)) ` = x ` by Th9; hence (x + ((y + (x `)) `)) ` = x ` by Th19; ::_thesis: verum end; theorem Th21: :: ROBBINS2:21 for L being non empty satisfying_DN_1 ComplLLattStr for x being Element of L holds (x + x) ` = x ` proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x being Element of L holds (x + x) ` = x ` let x be Element of L; ::_thesis: (x + x) ` = x ` set y = the Element of L; set Y = ( the Element of L + x) ` ; (x + (((( the Element of L + x) `) + (x `)) `)) ` = x ` by Th20; hence (x + x) ` = x ` by Th19; ::_thesis: verum 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 ` proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds (((((x + y) `) + x) `) + y) ` = y ` let x, y be Element of L; ::_thesis: (((((x + y) `) + x) `) + y) ` = y ` y ` = (y + y) ` by Th21 .= (((((x + y) `) + x) `) + y) ` by Th17 ; hence (((((x + y) `) + x) `) + y) ` = y ` ; ::_thesis: verum end; theorem Th23: :: ROBBINS2:23 for L being non empty satisfying_DN_1 ComplLLattStr for x being Element of L holds (x `) ` = x proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x being Element of L holds (x `) ` = x let x be Element of L; ::_thesis: (x `) ` = x (x `) ` = (((((x + (x `)) `) + x) `) + (x `)) ` by Th22 .= x by Th19 ; hence (x `) ` = x ; ::_thesis: verum 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 `) ` proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds ((((x + y) `) + x) `) + y = (y `) ` let x, y be Element of L; ::_thesis: ((((x + y) `) + x) `) + y = (y `) ` ((((((x + y) `) + x) `) + y) `) ` = (y `) ` by Th22; hence ((((x + y) `) + x) `) + y = (y `) ` by Th23; ::_thesis: verum 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 proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds ((x + y) `) ` = y + x let x, y be Element of L; ::_thesis: ((x + y) `) ` = y + x ((x + y) `) ` = ((y + x) `) ` by Th14 .= y + x by Th23 ; hence ((x + y) `) ` = y + x ; ::_thesis: verum 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) `) ` proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds x + ((((y + z) `) + ((y + x) `)) `) = ((y + x) `) ` let x, y, z be Element of L; ::_thesis: x + ((((y + z) `) + ((y + x) `)) `) = ((y + x) `) ` ((x + ((((y + z) `) + ((y + x) `)) `)) `) ` = ((y + x) `) ` by Th10; hence x + ((((y + z) `) + ((y + x) `)) `) = ((y + x) `) ` by Th23; ::_thesis: verum end; theorem Th27: :: ROBBINS2:27 for L being non empty satisfying_DN_1 ComplLLattStr for x, y being Element of L holds x + y = y + x proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds x + y = y + x let x, y be Element of L; ::_thesis: x + y = y + x x + y = ((x + y) `) ` by Th23 .= y + x by Th25 ; hence x + y = y + x ; ::_thesis: verum end; Lm1: for L being non empty satisfying_DN_1 ComplLLattStr holds L is join-commutative proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: L is join-commutative for x, y being Element of L holds x + y = y + x by Th27; hence L is join-commutative by LATTICES:def_4; ::_thesis: verum end; registration cluster non empty satisfying_DN_1 -> non empty join-commutative for ComplLLattStr ; coherence for b1 being non empty ComplLLattStr st b1 is satisfying_DN_1 holds b1 is join-commutative by Lm1; end; 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 proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds ((((x + y) `) + x) `) + y = y let x, y be Element of L; ::_thesis: ((((x + y) `) + x) `) + y = y ((((x + y) `) + x) `) + y = (y `) ` by Th24; hence ((((x + y) `) + x) `) + y = y by Th23; ::_thesis: verum end; theorem :: ROBBINS2:29 for L being non empty satisfying_DN_1 ComplLLattStr for x, y being Element of L holds ((((x + y) `) + y) `) + x = x by Th28; theorem :: ROBBINS2:30 for L being non empty satisfying_DN_1 ComplLLattStr for x, y being Element of L holds x + ((((y + x) `) + y) `) = x by Th28; 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 `)) ` proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds ((x + (y `)) `) + (((y `) + y) `) = (x + (y `)) ` let x, y be Element of L; ::_thesis: ((x + (y `)) `) + (((y `) + y) `) = (x + (y `)) ` set X = (x + (y `)) ` ; ((x + (y `)) `) + ((((y + ((x + (y `)) `)) `) + y) `) = (x + (y `)) ` by Th28; hence ((x + (y `)) `) + (((y `) + y) `) = (x + (y `)) ` by Th20; ::_thesis: verum 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) ` proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds ((x + y) `) + ((y + (y `)) `) = (x + y) ` let x, y be Element of L; ::_thesis: ((x + y) `) + ((y + (y `)) `) = (x + y) ` set X = (x + y) ` ; set Y = y ` ; ((x + y) `) + (((((y `) + ((x + y) `)) `) + (y `)) `) = (x + y) ` by Th28; hence ((x + y) `) + ((y + (y `)) `) = (x + y) ` by Th18; ::_thesis: verum end; theorem :: ROBBINS2:33 for L being non empty satisfying_DN_1 ComplLLattStr for x, y being Element of L holds ((x + y) `) + (((y `) + y) `) = (x + y) ` by Th32; 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) ` proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds ((((x + (y `)) `) `) + y) ` = ((y `) + y) ` let x, y be Element of L; ::_thesis: ((((x + (y `)) `) `) + y) ` = ((y `) + y) ` set Y = y ` ; set Z = y; (((((x + (y `)) `) + (((y `) + y) `)) `) + y) ` = ((y `) + y) ` by Th15; hence ((((x + (y `)) `) `) + y) ` = ((y `) + y) ` by Th31; ::_thesis: verum 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) ` proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds ((x + (y `)) + y) ` = ((y `) + y) ` let x, y be Element of L; ::_thesis: ((x + (y `)) + y) ` = ((y `) + y) ` ((((x + (y `)) `) `) + y) ` = ((y `) + y) ` by Th34; hence ((x + (y `)) + y) ` = ((y `) + y) ` by Th23; ::_thesis: verum 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 proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds ((((((x + (y `)) + z) `) + y) `) + (((y `) + y) `)) ` = y let x, y, z be Element of L; ::_thesis: ((((((x + (y `)) + z) `) + y) `) + (((y `) + y) `)) ` = y ((x + (y `)) + y) ` = ((y `) + y) ` by Th35; hence ((((((x + (y `)) + z) `) + y) `) + (((y `) + y) `)) ` = y by Th9; ::_thesis: verum 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 proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds x + ((((y + z) `) + ((y + x) `)) `) = y + x let x, y, z be Element of L; ::_thesis: x + ((((y + z) `) + ((y + x) `)) `) = y + x x + ((((y + z) `) + ((y + x) `)) `) = ((y + x) `) ` by Th26; hence x + ((((y + z) `) + ((y + x) `)) `) = y + x by Th23; ::_thesis: verum 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 proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds x + ((y + ((((z + y) `) + x) `)) `) = ((z + y) `) + x let x, y, z be Element of L; ::_thesis: x + ((y + ((((z + y) `) + x) `)) `) = ((z + y) `) + x set Y = (z + y) ` ; set Z = y ` ; x + ((((((z + y) `) + (y `)) `) + ((((z + y) `) + x) `)) `) = ((z + y) `) + x by Th37; hence x + ((y + ((((z + y) `) + x) `)) `) = ((z + y) `) + x by Th19; ::_thesis: verum end; theorem :: ROBBINS2:39 for L being non empty satisfying_DN_1 ComplLLattStr for x, y, z being Element of L holds x + ((((y + x) `) + ((y + z) `)) `) = y + x by Th37; 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 proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds ((((x + y) `) + ((((x + y) `) + ((x + z) `)) `)) `) + y = y let x, y, z be Element of L; ::_thesis: ((((x + y) `) + ((((x + y) `) + ((x + z) `)) `)) `) + y = y set Y = (((x + y) `) + ((x + z) `)) ` ; ((((y + ((((x + y) `) + ((x + z) `)) `)) `) + ((((x + y) `) + ((x + z) `)) `)) `) + y = y by Th28; hence ((((x + y) `) + ((((x + y) `) + ((x + z) `)) `)) `) + y = y by Th37; ::_thesis: verum 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 proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds (((((x + (y `)) + z) `) + y) `) ` = y let x, y, z be Element of L; ::_thesis: (((((x + (y `)) + z) `) + y) `) ` = y (((((x + (y `)) + z) `) + y) `) + (((y `) + y) `) = ((((x + (y `)) + z) `) + y) ` by Th32; hence (((((x + (y `)) + z) `) + y) `) ` = y by Th36; ::_thesis: verum 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 proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds x + (((y + (x `)) + z) `) = x let x, y, z be Element of L; ::_thesis: x + (((y + (x `)) + z) `) = x (((((y + (x `)) + z) `) + x) `) ` = x by Th41; hence x + (((y + (x `)) + z) `) = x by Th25; ::_thesis: verum 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 ` proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds (x `) + (((y + x) + z) `) = x ` let x, y, z be Element of L; ::_thesis: (x `) + (((y + x) + z) `) = x ` set X = x ` ; (x `) + (((y + ((x `) `)) + z) `) = x ` by Th42; hence (x `) + (((y + x) + z) `) = x ` by Th23; ::_thesis: verum 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 `) proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds ((x + y) `) + x = x + (y `) let x, y be Element of L; ::_thesis: ((x + y) `) + x = x + (y `) set Z = x; x + ((y + ((((x + y) `) + x) `)) `) = ((x + y) `) + x by Th38; hence ((x + y) `) + x = x + (y `) by Th28; ::_thesis: verum 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) ` proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y being Element of L holds (x + ((x + (y `)) `)) ` = (x + y) ` let x, y be Element of L; ::_thesis: (x + ((x + (y `)) `)) ` = (x + y) ` (x + ((((x + y) `) + x) `)) ` = (x + y) ` by Th8; hence (x + ((x + (y `)) `)) ` = (x + y) ` by Th44; ::_thesis: verum 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 proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds ((((x + y) `) + (x + z)) `) + y = y let x, y, z be Element of L; ::_thesis: ((((x + y) `) + (x + z)) `) + y = y (((x + y) `) + ((((x + y) `) + ((x + z) `)) `)) ` = (((x + y) `) + (x + z)) ` by Th45; hence ((((x + y) `) + (x + z)) `) + y = y by Th40; ::_thesis: verum 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) `) ` proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds ((((((x + y) `) + z) `) + (((x `) + y) `)) `) + y = (((x `) + y) `) ` let x, y, z be Element of L; ::_thesis: ((((((x + y) `) + z) `) + (((x `) + y) `)) `) + y = (((x `) + y) `) ` ((((((((x + y) `) + z) `) + (((x `) + y) `)) `) + y) `) ` = (((x `) + y) `) ` by Th11; hence ((((((x + y) `) + z) `) + (((x `) + y) `)) `) + y = (((x `) + y) `) ` by Th23; ::_thesis: verum 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 proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds ((((((x + y) `) + z) `) + (((x `) + y) `)) `) + y = (x `) + y let x, y, z be Element of L; ::_thesis: ((((((x + y) `) + z) `) + (((x `) + y) `)) `) + y = (x `) + y ((((((x + y) `) + z) `) + (((x `) + y) `)) `) + y = (((x `) + y) `) ` by Th47; hence ((((((x + y) `) + z) `) + (((x `) + y) `)) `) + y = (x `) + y by Th23; ::_thesis: verum 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) proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds (((x `) + (((((y + x) `) `) + (y + z)) `)) `) + (y + z) = (((y + x) `) `) + (y + z) let x, y, z be Element of L; ::_thesis: (((x `) + (((((y + x) `) `) + (y + z)) `)) `) + (y + z) = (((y + x) `) `) + (y + z) set X = (y + x) ` ; set Y = y + z; set Z = x; ((((((((y + x) `) + (y + z)) `) + x) `) + (((((y + x) `) `) + (y + z)) `)) `) + (y + z) = (((y + x) `) `) + (y + z) by Th48; hence (((x `) + (((((y + x) `) `) + (y + z)) `)) `) + (y + z) = (((y + x) `) `) + (y + z) by Th46; ::_thesis: verum 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) proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds (((x `) + (((y + x) + (y + z)) `)) `) + (y + z) = (((y + x) `) `) + (y + z) let x, y, z be Element of L; ::_thesis: (((x `) + (((y + x) + (y + z)) `)) `) + (y + z) = (((y + x) `) `) + (y + z) (((x `) + (((((y + x) `) `) + (y + z)) `)) `) + (y + z) = (((y + x) `) `) + (y + z) by Th49; hence (((x `) + (((y + x) + (y + z)) `)) `) + (y + z) = (((y + x) `) `) + (y + z) by Th23; ::_thesis: verum 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) proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds (((x `) + (((y + x) + (y + z)) `)) `) + (y + z) = (y + x) + (y + z) let x, y, z be Element of L; ::_thesis: (((x `) + (((y + x) + (y + z)) `)) `) + (y + z) = (y + x) + (y + z) (((x `) + (((y + x) + (y + z)) `)) `) + (y + z) = (((y + x) `) `) + (y + z) by Th50; hence (((x `) + (((y + x) + (y + z)) `)) `) + (y + z) = (y + x) + (y + z) by Th23; ::_thesis: verum 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) proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds ((x `) `) + (y + z) = (y + x) + (y + z) let x, y, z be Element of L; ::_thesis: ((x `) `) + (y + z) = (y + x) + (y + z) (x `) + (((y + x) + (y + z)) `) = x ` by Th43; hence ((x `) `) + (y + z) = (y + x) + (y + z) by Th51; ::_thesis: verum 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) proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds (x + y) + (x + z) = y + (x + z) let x, y, z be Element of L; ::_thesis: (x + y) + (x + z) = y + (x + z) set Y = x; set X = y; ((y `) `) + (x + z) = (x + y) + (x + z) by Th52; hence (x + y) + (x + z) = y + (x + z) by Th23; ::_thesis: verum end; theorem :: ROBBINS2:54 for L being non empty satisfying_DN_1 ComplLLattStr for x, y, z being Element of L holds (x + y) + (x + z) = z + (x + y) by Th53; 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) proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: for x, y, z being Element of L holds x + (y + z) = z + (y + x) let x, y, z be Element of L; ::_thesis: x + (y + z) = z + (y + x) (y + x) + (y + z) = z + (y + x) by Th53; hence x + (y + z) = z + (y + x) by Th53; ::_thesis: verum 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; 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; Lm2: for L being non empty satisfying_DN_1 ComplLLattStr holds L is join-associative proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: L is join-associative for x, y, z being Element of L holds (x + y) + z = x + (y + z) by Th55; hence L is join-associative by LATTICES:def_5; ::_thesis: verum end; Lm3: for L being non empty satisfying_DN_1 ComplLLattStr holds L is Robbins proof let L be non empty satisfying_DN_1 ComplLLattStr ; ::_thesis: L is Robbins for x, y being Element of L holds (((x + y) `) + ((x + (y `)) `)) ` = x by Th6; hence L is Robbins by ROBBINS1:def_5; ::_thesis: verum end; registration cluster non empty satisfying_DN_1 -> non empty join-associative for ComplLLattStr ; coherence for b1 being non empty ComplLLattStr st b1 is satisfying_DN_1 holds b1 is join-associative by Lm2; cluster non empty satisfying_DN_1 -> non empty Robbins for ComplLLattStr ; coherence for b1 being non empty ComplLLattStr st b1 is satisfying_DN_1 holds b1 is Robbins by Lm3; end; 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 proof let L be non empty ComplLLattStr ; ::_thesis: 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 let x, z be Element of L; ::_thesis: ( L is join-commutative & L is join-associative & L is Huntington implies (z + x) *' (z + (x `)) = z ) assume ( L is join-commutative & L is join-associative & L is Huntington ) ; ::_thesis: (z + x) *' (z + (x `)) = z then reconsider L9 = L as non empty join-commutative join-associative Huntington ComplLLattStr ; reconsider z9 = z, x9 = x as Element of L9 ; (z9 + x9) *' (z9 + (x9 `)) = z9 + (x9 *' (x9 `)) by ROBBINS1:31 .= z9 + (Bot L9) by ROBBINS1:15 .= z9 by ROBBINS1:13 ; hence (z + x) *' (z + (x `)) = z ; ::_thesis: verum 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 proof let L be non empty join-commutative join-associative ComplLLattStr ; ::_thesis: ( L is Robbins implies L is satisfying_DN_1 ) assume L is Robbins ; ::_thesis: L is satisfying_DN_1 then reconsider L9 = L as non empty join-commutative join-associative Robbins ComplLLattStr ; let x, y, z, u be Element of L; :: according to ROBBINS2:def_1 ::_thesis: (((((x + y) `) + z) `) + ((x + (((z `) + ((z + u) `)) `)) `)) ` = z A1: L9 is Huntington ; then A2: (z + x) *' (z + (x `)) = z by Th58; A3: (((x + y) `) + z) *' z = (z + ((x + y) `)) *' z .= z *' (z + ((x + y) `)) .= z by A1, ROBBINS1:21 ; A4: ((((x + y) `) + z) *' x) + z = z + ((((x + y) `) + z) *' x) .= (z + (((x + y) `) + z)) *' (z + x) by A1, ROBBINS1:31 .= ((((x + y) `) + z) + z) *' (z + x) .= (((x + y) `) + (z + z)) *' (z + x) by LATTICES:def_5 .= (((x + y) `) + z) *' (z + x) by A1, ROBBINS1:12 .= (((((x `) *' (y `)) `) `) + z) *' (z + x) by A1, ROBBINS1:17 .= (((x `) *' (y `)) + z) *' (z + x) by A1, ROBBINS1:3 .= (z + ((x `) *' (y `))) *' (z + x) .= ((z + (x `)) *' (z + (y `))) *' (z + x) by A1, ROBBINS1:31 .= (z + x) *' ((z + (x `)) *' (z + (y `))) .= (z + x) *' (((x `) + z) *' (z + (y `))) .= (z + x) *' (((x `) + z) *' ((y `) + z)) .= ((z + x) *' ((x `) + z)) *' ((y `) + z) by A1, ROBBINS1:16 .= ((z + x) *' (z + (x `))) *' ((y `) + z) .= z *' (z + (y `)) by A2 .= z by A1, ROBBINS1:21 ; (((((x + y) `) + z) `) + ((x + (((z `) + ((z + u) `)) `)) `)) ` = (((((((x + y) `) + z) `) `) *' (((x + (((z `) + ((z + u) `)) `)) `) `)) `) ` by A1, ROBBINS1:17 .= (((((x + y) `) + z) `) `) *' (((x + (((z `) + ((z + u) `)) `)) `) `) by A1, ROBBINS1:3 .= (((((x + y) `) + z) `) `) *' (x + (((z `) + ((z + u) `)) `)) by A1, ROBBINS1:3 .= (((x + y) `) + z) *' (x + (((z `) + ((z + u) `)) `)) by A1, ROBBINS1:3 .= (((((x + y) `) `) *' (z `)) `) *' (x + (((z `) + ((z + u) `)) `)) by A1, ROBBINS1:17 .= (((x + y) *' (z `)) `) *' (x + (((z `) + ((z + u) `)) `)) by A1, ROBBINS1:3 .= (((x + y) *' (z `)) `) *' (x + (((((z `) `) *' (((z + u) `) `)) `) `)) by A1, ROBBINS1:17 .= (((x + y) *' (z `)) `) *' (x + (((z *' (((z + u) `) `)) `) `)) by A1, ROBBINS1:3 .= (((x + y) *' (z `)) `) *' (x + (z *' (((z + u) `) `))) by A1, ROBBINS1:3 .= (((x + y) *' (z `)) `) *' (x + (z *' (z + u))) by A1, ROBBINS1:3 .= (((x + y) *' (z `)) `) *' (x + z) by A1, ROBBINS1:21 .= ((((x + y) *' (z `)) `) *' x) + ((((x + y) *' (z `)) `) *' z) by A1, ROBBINS1:30 .= ((((((x + y) `) `) *' (z `)) `) *' x) + ((((x + y) *' (z `)) `) *' z) by A1, ROBBINS1:3 .= ((((x + y) `) + z) *' x) + ((((x + y) *' (z `)) `) *' z) by A1, ROBBINS1:17 .= ((((x + y) `) + z) *' x) + ((((((x + y) `) `) *' (z `)) `) *' z) by A1, ROBBINS1:3 .= z by A1, A3, A4, ROBBINS1:17 ; hence (((((x + y) `) + z) `) + ((x + (((z `) + ((z + u) `)) `)) `)) ` = z ; ::_thesis: verum end; registration cluster non empty join-commutative join-associative Robbins -> non empty satisfying_DN_1 for ComplLLattStr ; coherence for b1 being non empty ComplLLattStr st b1 is join-commutative & b1 is join-associative & b1 is Robbins holds b1 is satisfying_DN_1 by Th59; end; registration 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 b1 being preOrthoLattice st ( b1 is satisfying_DN_1 & b1 is de_Morgan ) proof take TrivOrtLat ; ::_thesis: ( TrivOrtLat is satisfying_DN_1 & TrivOrtLat is de_Morgan ) thus ( TrivOrtLat is satisfying_DN_1 & TrivOrtLat is de_Morgan ) ; ::_thesis: verum end; end; registration cluster non empty Lattice-like de_Morgan satisfying_DN_1 -> Boolean for OrthoLattStr ; coherence for b1 being preOrthoLattice st b1 is satisfying_DN_1 & b1 is de_Morgan holds b1 is Boolean ; cluster non empty Lattice-like Boolean well-complemented -> well-complemented satisfying_DN_1 for OrthoLattStr ; coherence for b1 being well-complemented preOrthoLattice st b1 is Boolean holds b1 is satisfying_DN_1 ; end; begin definition let L be non empty ComplLLattStr ; attrL is satisfying_MD_1 means :Def2: :: ROBBINS2:def 2 for x, y being Element of L holds (((x `) + y) `) + x = x; attrL 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 ComplLLattStr 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 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_) 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 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 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; A4: (((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, A4, Def2 ; hence (((x `) + y) `) + y = y + x ; ::_thesis: verum end; A5: 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 A3 .= x by A1, Def2 ; hence x + x = x ; ::_thesis: verum end; A6: 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 A5 .= x + y by A3 ; hence x + (x + y) = x + y ; ::_thesis: verum end; A7: 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 A3 .= (((y `) + (x + y)) `) + (x + (x + y)) by A6 .= (x + y) + (x + y) by A1, Def3 .= x + y by A5 ; hence (x + y) + y = x + y ; ::_thesis: verum end; A8: 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 A3 .= (((y `) + x) `) + x by A7 .= x + y by A3 ; hence (x + y) + x = x + y ; ::_thesis: verum end; A9: 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; A10: 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 A6 .= y + x by A9 ; hence x + (y + x) = y + x ; ::_thesis: verum end; A11: 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 A10 .= y by A1, Def2 ; hence ((x + (y `)) `) + y = y ; ::_thesis: verum end; A12: 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 A5; ::_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) + ((x `) `) by A12 .= ((x `) `) + x by A8 .= x by A12 ; hence x + ((x `) `) = x ; ::_thesis: verum end; A14: 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 A12 .= x + y by A3 ; hence x + (((x `) `) + y) = x + y ; ::_thesis: verum end; A15: 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 A14 .= x + ((x `) `) by A13 .= x by A13 ; hence x + ((((x `) `) `) `) = x ; ::_thesis: verum end; A16: for x being Element of L holds ((x `) `) ` = x ` proof 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; A17: 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; A18: 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 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; A19: 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 A16 .= (((x `) + ((x `) `)) `) + x by A18 .= x by A1, Def2 ; hence (x `) ` = x ; ::_thesis: verum end; A20: 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; A21: 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 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; A22: 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 A8 .= x by A1, Def2 ; hence x + (((x `) + y) `) = x ; ::_thesis: verum end; A23: 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 A22 .= (x `) + ((x + y) `) by A19 ; hence (x `) + ((x + y) `) = x ` ; ::_thesis: verum end; A24: 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 A11 .= ((y + (x `)) `) + x by A8 .= x by A11 ; hence x + ((y + (x `)) `) = x ; ::_thesis: verum end; A25: 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 A24 .= (x `) + ((y + x) `) by A19 ; hence (x `) + ((y + x) `) = x ` ; ::_thesis: verum end; A26: 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 A21 .= ((x `) `) + ((y `) + ((x + y) `)) by A23 .= ((x `) `) + (y `) by A25 .= x + (y `) by A19 ; hence x + (y `) = (y `) + x ; ::_thesis: verum end; A27: 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 A19; hence x + y = y + x by A26; ::_thesis: verum end; hence L is join-commutative by LATTICES:def_4; ::_thesis: ( L is Huntington & L is join-associative ) A28: 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; A29: 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 A28 .= (y `) + x by A1, Def2 ; hence x + ((y `) + x) = (y `) + x ; ::_thesis: verum end; A30: 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 A29 .= (((((y `) + x) `) + x) `) + x by A3 .= ((x + y) `) + x by A3 ; hence ((x + y) `) + x = (y `) + x ; ::_thesis: verum end; A31: 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 A3 .= (x `) + (((y `) + x) `) by A30 ; hence ((x + y) `) + (((y `) + x) `) = (x `) + (((y `) + x) `) ; ::_thesis: verum end; 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 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; hence L is Huntington by ROBBINS1:def_6; ::_thesis: L is join-associative A32: 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 A3 .= (((z `) + (x + y)) `) + (y + (x + y)) by A10 .= (x + y) + (y + z) by A1, Def3 ; hence (x + y) + (y + z) = (x + y) + z ; ::_thesis: verum end; 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 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; then (y + x) + (z + y) = x + (y + 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; 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 for ComplLLattStr ; coherence for b1 being non empty ComplLLattStr 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 for ComplLLattStr ; coherence for b1 being non empty ComplLLattStr st b1 is join-commutative & b1 is join-associative & b1 is Huntington holds ( b1 is satisfying_MD_1 & b1 is satisfying_MD_2 ) proof let L be non empty ComplLLattStr ; ::_thesis: ( L is join-commutative & L is join-associative & L is Huntington implies ( L is satisfying_MD_1 & L is satisfying_MD_2 ) ) assume ( L is join-commutative & L is join-associative & L is Huntington ) ; ::_thesis: ( L is satisfying_MD_1 & L is satisfying_MD_2 ) then reconsider L9 = L as non empty join-commutative join-associative Huntington ComplLLattStr ; A1: L9 is satisfying_MD_2 proof let x, y, z be Element of L9; :: according to ROBBINS2:def_3 ::_thesis: (((x `) + y) `) + (z + y) = y + (z + x) set Z = z + y; A2: (z + y) + (y `) = z + (y + (y `)) by LATTICES:def_5 .= z + (Top L9) by ROBBINS1:def_8 .= Top L9 by ROBBINS1:19 ; (((x `) + y) `) + (z + y) = (((x `) + ((y `) `)) `) + (z + y) by ROBBINS1:3 .= (x *' (y `)) + (z + y) by ROBBINS1:def_4 .= ((z + y) + x) *' ((z + y) + (y `)) by ROBBINS1:31 .= (z + y) + x by A2, ROBBINS1:14 .= y + (z + x) by LATTICES:def_5 ; hence (((x `) + y) `) + (z + y) = y + (z + x) ; ::_thesis: verum end; L9 is satisfying_MD_1 proof let x, y be Element of L9; :: according to ROBBINS2:def_2 ::_thesis: (((x `) + y) `) + x = x (((x `) + y) `) + x = (((x `) + ((y `) `)) `) + x by ROBBINS1:3 .= (x *' (y `)) + x by ROBBINS1:def_4 .= x by ROBBINS1:20 ; hence (((x `) + y) `) + x = x ; ::_thesis: verum end; hence ( L is satisfying_MD_1 & L is satisfying_MD_2 ) by A1; ::_thesis: verum end; end; registration 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 b1 being preOrthoLattice st ( b1 is satisfying_MD_1 & b1 is satisfying_MD_2 & b1 is satisfying_DN_1 & b1 is de_Morgan ) proof take TrivOrtLat ; ::_thesis: ( TrivOrtLat is satisfying_MD_1 & TrivOrtLat is satisfying_MD_2 & TrivOrtLat is satisfying_DN_1 & TrivOrtLat is de_Morgan ) thus ( TrivOrtLat is satisfying_MD_1 & TrivOrtLat is satisfying_MD_2 & TrivOrtLat is satisfying_DN_1 & TrivOrtLat is de_Morgan ) ; ::_thesis: verum end; end; registration cluster non empty Lattice-like de_Morgan satisfying_MD_1 satisfying_MD_2 -> Boolean for 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 ; cluster non empty Lattice-like Boolean well-complemented -> well-complemented satisfying_MD_1 satisfying_MD_2 for OrthoLattStr ; coherence for b1 being well-complemented preOrthoLattice st b1 is Boolean holds ( b1 is satisfying_MD_1 & b1 is satisfying_MD_2 ) ; end;