theorem Th9: :: NAT_LAT:9

for p, q, r being Element of Nat_Lattice holds hcflat . (p,(hcflat . (q,r))) = hcflat . ((hcflat . (p,q)),r)