theorem Th3:
for
p,
q,
r being
Element of
Real_Lattice holds
(
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) )