let L be non empty join-commutative join-associative Huntington ComplLattStr ; :: thesis: for a, b, c being Element of L holds
( (a *' c) *' (b *' (c ` )) = Bot L & ((a *' b) *' c) *' (((a ` ) *' b) *' c) = Bot L & ((a *' (b ` )) *' c) *' (((a ` ) *' b) *' c) = Bot L & ((a *' b) *' c) *' (((a ` ) *' (b ` )) *' c) = Bot L & ((a *' b) *' (c ` )) *' (((a ` ) *' (b ` )) *' (c ` )) = Bot L )
let a, b, c be Element of L; :: thesis: ( (a *' c) *' (b *' (c ` )) = Bot L & ((a *' b) *' c) *' (((a ` ) *' b) *' c) = Bot L & ((a *' (b ` )) *' c) *' (((a ` ) *' b) *' c) = Bot L & ((a *' b) *' c) *' (((a ` ) *' (b ` )) *' c) = Bot L & ((a *' b) *' (c ` )) *' (((a ` ) *' (b ` )) *' (c ` )) = Bot L )
A1: for a, b, c being Element of L holds (a *' c) *' (b *' (c ` )) = Bot L

proof

let a, b, c be Element of L; :: thesis: (a *' c) *' (b *' (c ` )) = Bot L
thus (a *' c) *' (b *' (c ` )) = ((a *' c) *' (c ` )) *' b by Th17
.= (a *' (c *' (c ` ))) *' b by Th17
.= (a *' (Bot L)) *' b by Th16
.= (Bot L) *' b by Def9
.= Bot L by Def9 ; :: thesis: verum

end;

hence (a *' c) *' (b *' (c ` )) = Bot L ; :: thesis: ( ((a *' b) *' c) *' (((a ` ) *' b) *' c) = Bot L & ((a *' (b ` )) *' c) *' (((a ` ) *' b) *' c) = Bot L & ((a *' b) *' c) *' (((a ` ) *' (b ` )) *' c) = Bot L & ((a *' b) *' (c ` )) *' (((a ` ) *' (b ` )) *' (c ` )) = Bot L )
thus ((a *' b) *' c) *' (((a ` ) *' b) *' c) = (a *' (b *' c)) *' (((a ` ) *' b) *' c) by Th17
.= (((b *' c) *' a) *' ((a ` ) *' b)) *' c by Th17
.= ((((b *' c) *' a) *' (a ` )) *' b) *' c by Th17
.= (((b *' c) *' (a *' (a ` ))) *' b) *' c by Th17
.= ((b *' c) *' (a *' (a ` ))) *' (b *' c) by Th17
.= ((b *' c) *' (Bot L)) *' (b *' c) by Th16
.= (Bot L) *' (b *' c) by Def9
.= Bot L by Def9 ; :: thesis: ( ((a *' (b ` )) *' c) *' (((a ` ) *' b) *' c) = Bot L & ((a *' b) *' c) *' (((a ` ) *' (b ` )) *' c) = Bot L & ((a *' b) *' (c ` )) *' (((a ` ) *' (b ` )) *' (c ` )) = Bot L )
thus ((a *' (b ` )) *' c) *' (((a ` ) *' b) *' c) = (a *' ((b ` ) *' c)) *' (((a ` ) *' b) *' c) by Th17
.= (((b ` ) *' c) *' a) *' ((a ` ) *' (b *' c)) by Th17
.= ((((b ` ) *' c) *' a) *' (a ` )) *' (b *' c) by Th17
.= (((b ` ) *' c) *' (a *' (a ` ))) *' (b *' c) by Th17
.= (((b ` ) *' c) *' (Bot L)) *' (b *' c) by Th16
.= (Bot L) *' (b *' c) by Def9
.= Bot L by Def9 ; :: thesis: ( ((a *' b) *' c) *' (((a ` ) *' (b ` )) *' c) = Bot L & ((a *' b) *' (c ` )) *' (((a ` ) *' (b ` )) *' (c ` )) = Bot L )
thus ((a *' b) *' c) *' (((a ` ) *' (b ` )) *' c) = (a *' (b *' c)) *' (((a ` ) *' (b ` )) *' c) by Th17
.= (a *' (b *' c)) *' ((a ` ) *' ((b ` ) *' c)) by Th17
.= Bot L by A1 ; :: thesis: ((a *' b) *' (c ` )) *' (((a ` ) *' (b ` )) *' (c ` )) = Bot L
thus ((a *' b) *' (c ` )) *' (((a ` ) *' (b ` )) *' (c ` )) = (a *' (b *' (c ` ))) *' (((a ` ) *' (b ` )) *' (c ` )) by Th17
.= (a *' (b *' (c ` ))) *' ((a ` ) *' ((b ` ) *' (c ` ))) by Th17
.= Bot L by A1 ; :: thesis: verum