let L be non empty satisfying_DN_1 ComplLattStr ; :: thesis: for x being Element of L holds (x ` ) ` = x
let x be Element of L; :: thesis: (x ` ) ` = x
(x ` ) ` = (((((x + (x ` )) ` ) + x) ` ) + (x ` )) ` by Th22
.= x by Th19 ;
hence (x ` ) ` = x ; :: thesis: verum