let a, b, c be real number ; :: 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