let A be non empty set ; :: thesis: for p, q being Element of (RealFunc_Lattice A) holds (maxfuncreal A) . (p,q) = (maxfuncreal A) . (q,p)
let p, q be Element of (RealFunc_Lattice A); :: thesis: (maxfuncreal A) . (p,q) = (maxfuncreal A) . (q,p)
thus (maxfuncreal A) . (p,q) = q "\/" p by LATTICES:def 1
.= (maxfuncreal A) . (q,p) ; :: thesis: verum