let L be non empty join-commutative join-associative Huntington ComplLLattStr ; :: thesis: for a, b being Element of L st a + b = Top L & a *' b = Bot L holds
a ` = b
let a, b be Element of L; :: thesis: ( a + b = Top L & a *' b = Bot L implies a ` = b )
assume a + b = Top L ; :: thesis: ( not a *' b = Bot L or a ` = b )
then A1: ((a ` ) ` ) + b = Top L by Th3;
assume A2: a *' b = Bot L ; :: thesis: a ` = b
(b ` ) + (a ` ) = (((a ` ) + (b ` )) ` ) ` by Th3
.= Top L by A2, Th10 ;
hence a ` = b by A1, Th23; :: thesis: verum