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 Th26; :: 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 Th26 ; :: 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 Th26 ; :: thesis: (maxfuncreal A) . ((minfuncreal A) . q,p),q = q
thus (maxfuncreal A) . ((minfuncreal A) . q,p),q = q by A1, Th41; :: thesis: verum