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