theorem Th6: :: NAT_LAT:6

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