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