let p, q, r be Element of Nat_Lattice; :: thesis: hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (p,q)),r)
set s = q "/\" r;
thus hcflat . (p,(hcflat . (q,r))) = p "/\" (q "/\" r)
.= (p "/\" q) "/\" r by NEWTON:48
.= hcflat . ((hcflat . (p,q)),r) ; :: thesis: verum