let L be non empty join-commutative join-associative Huntington ComplLattStr ; :: thesis: for a, b being Element of L st (a ` ) + b = Top L & (b ` ) + a = Top L holds
a = b
let a, b be Element of L; :: thesis: ( (a ` ) + b = Top L & (b ` ) + a = Top L implies a = b )
assume A1: ( (a ` ) + b = Top L & (b ` ) + a = Top L ) ; :: thesis: a = b
thus a = (((a ` ) + (b ` )) ` ) + (((a ` ) + b) ` ) by Def6
.= b by A1, Def6 ; :: thesis: verum