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, Th9; :: thesis: verum