let q, p, r be Element of Real_Lattice ; :: thesis: 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) ; :: thesis: verum