theorem Th7: :: REAL_LAT:7

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