let A be non empty set ; 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); ( (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; ( (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
; ( (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; (minfuncreal A) . (((maxfuncreal A) . (q,p)),q) = q
thus
(minfuncreal A) . (((maxfuncreal A) . (q,p)),q) = q
by A2, Th21; verum