let L be non empty join-commutative join-associative Huntington join-idempotent ComplLattStr ; :: thesis: ( (Top L) ` = Bot L & Top L = (Bot L) ` )
consider a being Element of L;
thus (Top L) ` = (a + (a ` )) ` by Def8
.= Bot L by Th9 ; :: thesis: Top L = (Bot L) `
hence Top L = (Bot L) ` by Th3; :: thesis: verum