for p, q being Element of Real_Lattice holds minreal . (p,q) = minreal . (q,p)