let p,

q,

r be

Element of

Nat_Lattice;

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)
;

verum