let a, b, c be real number ; :: thesis: ( a <= b & b <= c implies ( (#) a,b = (#) a,c & b,c (#) = a,c (#) ) )
assume A1: ( a <= b & b <= c ) ; :: thesis: ( (#) a,b = (#) a,c & b,c (#) = a,c (#) )
hence (#) a,b = a by Def1
.= (#) a,c by A1, Def1, XXREAL_0:2 ;
:: thesis: b,c (#) = a,c (#)
thus b,c (#) = c by A1, Def2
.= a,c (#) by A1, Def2, XXREAL_0:2 ; :: thesis: verum