let p, q, r be Element of Real_Lattice; minreal . (q,(maxreal . (p,r))) = maxreal . ((minreal . (q,p)),(minreal . (q,r)))
set s = p "\/" r;
thus minreal . (q,(maxreal . (p,r))) =
q "/\" (p "\/" r)
.=
(q "/\" p) "\/" (q "/\" r)
by XXREAL_0:38
.=
maxreal . ((minreal . (q,p)),(minreal . (q,r)))
; verum