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