let L be non empty join-commutative join-associative Huntington ComplLLattStr ; :: thesis: for x being Element of L holds (x `) ` = x
let x be Element of L; :: thesis: (x `) ` = x
set y = x ` ;
( (((((x `) `) `) + ((x `) `)) `) + (((((x `) `) `) + (x `)) `) = (x `) ` & (((x `) + (((x `) `) `)) `) + (((x `) + ((x `) `)) `) = x ) by Def6;
hence (x `) ` = x by Th2; :: thesis: verum