let p, q be Element of Real_Lattice; :: thesis: minreal . (p,q) = minreal . (q,p)
thus minreal . (p,q) = q "/\" p by LATTICES:def 2
.= minreal . (q,p) ; :: thesis: verum