theorem :: REAL_LAT:27

for A being non empty set
for p, q, r being Element of (RealFunc_Lattice A) holds (minfuncreal A) . (q,((maxfuncreal A) . (p,r))) = (maxfuncreal A) . (((minfuncreal A) . (q,p)),((minfuncreal A) . (q,r))) by Th20;