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