let p, q be Element of Real_Lattice; :: thesis: ( minreal . (q,(maxreal . (q,p))) = q & minreal . ((maxreal . (p,q)),q) = q & minreal . (q,(maxreal . (p,q))) = q & minreal . ((maxreal . (q,p)),q) = q )
set s = q "\/" p;
thus A1: minreal . (q,(maxreal . (q,p))) = q "/\" (q "\/" p)
.= q by XXREAL_0:35 ; :: thesis: ( minreal . ((maxreal . (p,q)),q) = q & minreal . (q,(maxreal . (p,q))) = q & minreal . ((maxreal . (q,p)),q) = q )
thus A2: minreal . ((maxreal . (p,q)),q) = minreal . ((p "\/" q),q)
.= q "/\" (q "\/" p) by LATTICES:def 2
.= q by XXREAL_0:35 ; :: thesis: ( minreal . (q,(maxreal . (p,q))) = q & minreal . ((maxreal . (q,p)),q) = q )
thus minreal . (q,(maxreal . (p,q))) = q by A1, Th1; :: thesis: minreal . ((maxreal . (q,p)),q) = q
thus minreal . ((maxreal . (q,p)),q) = q by A2, Th1; :: thesis: verum