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