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