let p, q, r be Element of Real_Lattice; :: thesis: ( maxreal . (p,(maxreal . (q,r))) = maxreal . ((maxreal . (q,r)),p) & maxreal . (p,(maxreal . (q,r))) = maxreal . ((maxreal . (p,q)),r) & maxreal . (p,(maxreal . (q,r))) = maxreal . ((maxreal . (q,p)),r) & maxreal . (p,(maxreal . (q,r))) = maxreal . ((maxreal . (r,p)),q) & maxreal . (p,(maxreal . (q,r))) = maxreal . ((maxreal . (r,q)),p) & maxreal . (p,(maxreal . (q,r))) = maxreal . ((maxreal . (p,r)),q) )
set s = q "\/" r;
thus A1: maxreal . (p,(maxreal . (q,r))) = (q "\/" r) "\/" p by LATTICES:def 1
.= maxreal . ((maxreal . (q,r)),p) ; :: thesis: ( maxreal . (p,(maxreal . (q,r))) = maxreal . ((maxreal . (p,q)),r) & maxreal . (p,(maxreal . (q,r))) = maxreal . ((maxreal . (q,p)),r) & maxreal . (p,(maxreal . (q,r))) = maxreal . ((maxreal . (r,p)),q) & maxreal . (p,(maxreal . (q,r))) = maxreal . ((maxreal . (r,q)),p) & maxreal . (p,(maxreal . (q,r))) = maxreal . ((maxreal . (p,r)),q) )
thus maxreal . (p,(maxreal . (q,r))) = p "\/" (q "\/" r)
.= (p "\/" q) "\/" r by XXREAL_0:34
.= maxreal . ((maxreal . (p,q)),r) ; :: thesis: ( maxreal . (p,(maxreal . (q,r))) = maxreal . ((maxreal . (q,p)),r) & maxreal . (p,(maxreal . (q,r))) = maxreal . ((maxreal . (r,p)),q) & maxreal . (p,(maxreal . (q,r))) = maxreal . ((maxreal . (r,q)),p) & maxreal . (p,(maxreal . (q,r))) = maxreal . ((maxreal . (p,r)),q) )
thus maxreal . (p,(maxreal . (q,r))) = p "\/" (q "\/" r)
.= (q "\/" p) "\/" r by XXREAL_0:34
.= maxreal . ((maxreal . (q,p)),r) ; :: thesis: ( maxreal . (p,(maxreal . (q,r))) = maxreal . ((maxreal . (r,p)),q) & maxreal . (p,(maxreal . (q,r))) = maxreal . ((maxreal . (r,q)),p) & maxreal . (p,(maxreal . (q,r))) = maxreal . ((maxreal . (p,r)),q) )
thus A2: maxreal . (p,(maxreal . (q,r))) = p "\/" (q "\/" r)
.= (r "\/" p) "\/" q by XXREAL_0:34
.= maxreal . ((maxreal . (r,p)),q) ; :: thesis: ( maxreal . (p,(maxreal . (q,r))) = maxreal . ((maxreal . (r,q)),p) & maxreal . (p,(maxreal . (q,r))) = maxreal . ((maxreal . (p,r)),q) )
thus maxreal . (p,(maxreal . (q,r))) = maxreal . ((maxreal . (r,q)),p) by A1, Th1; :: thesis: maxreal . (p,(maxreal . (q,r))) = maxreal . ((maxreal . (p,r)),q)
thus maxreal . (p,(maxreal . (q,r))) = maxreal . ((maxreal . (p,r)),q) by A2, Th1; :: thesis: verum