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