let q, p 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, Th8; :: thesis: minreal . (maxreal . q,p),q = q
thus minreal . (maxreal . q,p),q = q by A2, Th8; :: thesis: verum