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