let A be non empty set ; :: thesis: for p, q being Element of (RealFunc_Lattice A) holds
( (minfuncreal A) . (q,((maxfuncreal A) . (q,p))) = q & (minfuncreal A) . (((maxfuncreal A) . (p,q)),q) = q & (minfuncreal A) . (q,((maxfuncreal A) . (p,q))) = q & (minfuncreal A) . (((maxfuncreal A) . (q,p)),q) = q )
let p, q be Element of (RealFunc_Lattice A); :: thesis: ( (minfuncreal A) . (q,((maxfuncreal A) . (q,p))) = q & (minfuncreal A) . (((maxfuncreal A) . (p,q)),q) = q & (minfuncreal A) . (q,((maxfuncreal A) . (p,q))) = q & (minfuncreal A) . (((maxfuncreal A) . (q,p)),q) = q )
thus A1: (minfuncreal A) . (q,((maxfuncreal A) . (q,p))) = q by Th16; :: thesis: ( (minfuncreal A) . (((maxfuncreal A) . (p,q)),q) = q & (minfuncreal A) . (q,((maxfuncreal A) . (p,q))) = q & (minfuncreal A) . (((maxfuncreal A) . (q,p)),q) = q )
thus A2: (minfuncreal A) . (((maxfuncreal A) . (p,q)),q) = (minfuncreal A) . ((p "\/" q),q)
.= q "/\" (q "\/" p) by LATTICES:def 2
.= q by Th16 ; :: thesis: ( (minfuncreal A) . (q,((maxfuncreal A) . (p,q))) = q & (minfuncreal A) . (((maxfuncreal A) . (q,p)),q) = q )
thus (minfuncreal A) . (q,((maxfuncreal A) . (p,q))) = q by A1, Th21; :: thesis: (minfuncreal A) . (((maxfuncreal A) . (q,p)),q) = q
thus (minfuncreal A) . (((maxfuncreal A) . (q,p)),q) = q by A2, Th21; :: thesis: verum