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, Th8; maxreal . p,(maxreal . q,r) = maxreal . (maxreal . p,r),q
thus
maxreal . p,(maxreal . q,r) = maxreal . (maxreal . p,r),q
by A2, Th8; verum