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