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