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 Th10; :: 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 Lm7
.= (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 Lm7
.= (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, Th21; :: 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, Th21; :: thesis: verum