theorem Th2: :: REAL_LAT:2

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