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