let p, q, r be Element of Real_Lattice; ( 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)
; ( 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)
; ( 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)
; ( 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)
; ( 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; maxreal . (p,(maxreal . (q,r))) = maxreal . ((maxreal . (p,r)),q)
thus
maxreal . (p,(maxreal . (q,r))) = maxreal . ((maxreal . (p,r)),q)
by A2, Th1; verum