let L be non empty join-commutative join-associative Huntington ComplLLattStr ; :: 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 Th16
.= (a *' (c *' (c `))) *' b by Th16
.= (a *' (Bot L)) *' b by Th15
.= (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 Th16
.= (((b *' c) *' a) *' ((a `) *' b)) *' c by Th16
.= ((((b *' c) *' a) *' (a `)) *' b) *' c by Th16
.= (((b *' c) *' (a *' (a `))) *' b) *' c by Th16
.= ((b *' c) *' (a *' (a `))) *' (b *' c) by Th16
.= ((b *' c) *' (Bot L)) *' (b *' c) by Th15
.= (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 Th16
.= (((b `) *' c) *' a) *' ((a `) *' (b *' c)) by Th16
.= ((((b `) *' c) *' a) *' (a `)) *' (b *' c) by Th16
.= (((b `) *' c) *' (a *' (a `))) *' (b *' c) by Th16
.= (((b `) *' c) *' (Bot L)) *' (b *' c) by Th15
.= (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 Th16
.= (a *' (b *' c)) *' ((a `) *' ((b `) *' c)) by Th16
.= 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 Th16
.= (a *' (b *' (c `))) *' ((a `) *' ((b `) *' (c `))) by Th16
.= Bot L by A1 ; :: thesis: verum