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, Th9 ;
hence a ` = b by A1, Th22; :: thesis: verum