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:61
.= hcflat . (hcflat . p,q),r ; :: thesis: verum