let L be non empty join-commutative join-associative Huntington ComplLLattStr ; :: 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