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