let a, b, c be Real; ( a <= b & b <= c implies ( (#) (a,b) = (#) (a,c) & (b,c) (#) = (a,c) (#) ) )
assume that
A1:
a <= b
and
A2:
b <= c
; ( (#) (a,b) = (#) (a,c) & (b,c) (#) = (a,c) (#) )
thus (#) (a,b) =
a
by A1, Def1
.=
(#) (a,c)
by A1, A2, Def1, XXREAL_0:2
; (b,c) (#) = (a,c) (#)
thus (b,c) (#) =
c
by A2, Def2
.=
(a,c) (#)
by A1, A2, Def2, XXREAL_0:2
; verum