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