let L be non empty satisfying_DN_1 ComplLLattStr ; :: thesis: for x being Element of L holds (((x + (x ` )) ` ) + x) ` = x `
let x be Element of L; :: thesis: (((x + (x ` )) ` ) + x) ` = x `
consider y, u being Element of L;
set V = (x + u) ` ;
(((x + (x ` )) ` ) + ((((((((x ` ) ` ) + y) ` ) + x) ` ) + ((((x ` ) ` ) + (((x ` ) + ((x + u) ` )) ` )) ` )) ` )) ` = x ` by Th1;
hence (((x + (x ` )) ` ) + x) ` = x ` by Def1; :: thesis: verum