let L be non empty satisfying_DN_1 ComplLLattStr ; :: thesis: for x, y, z being Element of L holds (((x ` ) + (((((y + x) ` ) ` ) + (y + z)) ` )) ` ) + (y + z) = (((y + x) ` ) ` ) + (y + z)
let x, y, z be Element of L; :: thesis: (((x ` ) + (((((y + x) ` ) ` ) + (y + z)) ` )) ` ) + (y + z) = (((y + x) ` ) ` ) + (y + z)
set X = (y + x) ` ;
set Y = y + z;
set Z = x;
((((((((y + x) ` ) + (y + z)) ` ) + x) ` ) + (((((y + x) ` ) ` ) + (y + z)) ` )) ` ) + (y + z) = (((y + x) ` ) ` ) + (y + z) by Th48;
hence (((x ` ) + (((((y + x) ` ) ` ) + (y + z)) ` )) ` ) + (y + z) = (((y + x) ` ) ` ) + (y + z) by Th46; :: thesis: verum