let L be non empty satisfying_DN_1 ComplLLattStr ; :: 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