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