let W be WA-Lattice; :: thesis: for a, b, c being Element of W holds ((a "/\" c) "\/" (b "/\" c)) "\/" c = c
let a, b, c be Element of W; :: thesis: ((a "/\" c) "\/" (b "/\" c)) "\/" c = c
(a "/\" c) "\/" c = c by LemmaX1;
then A1: a "/\" c <= c by Lemat0;
(b "/\" c) "\/" c = c by LemmaX1;
then b "/\" c <= c by Lemat0;
then (a "/\" c) "\/" (b "/\" c) <= c by LatWal1, A1;
hence ((a "/\" c) "\/" (b "/\" c)) "\/" c = c by Lemat0; :: thesis: verum