theorem Th1: :: REAL_LAT:1

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