now :: thesis: for r1, r2 being Real st r1 in dom (h | X) & r2 in dom (h | X) & r1 < r2 holds

(h | X) . r1 <= (h | X) . r2

hence
for b(h | X) . r1 <= (h | X) . r2

let r1, r2 be Real; :: thesis: ( r1 in dom (h | X) & r2 in dom (h | X) & r1 < r2 implies (h | X) . r1 <= (h | X) . r2 )

assume A1: ( r1 in dom (h | X) & r2 in dom (h | X) ) ; :: thesis: ( r1 < r2 implies (h | X) . r1 <= (h | X) . r2 )

then A2: ( h . r1 = (h | X) . r1 & h . r2 = (h | X) . r2 ) by FUNCT_1:47;

assume A3: r1 < r2 ; :: thesis: (h | X) . r1 <= (h | X) . r2

( r1 in dom h & r2 in dom h ) by A1, RELAT_1:57;

hence (h | X) . r1 <= (h | X) . r2 by A2, A3, Def3; :: thesis: verum

end;assume A1: ( r1 in dom (h | X) & r2 in dom (h | X) ) ; :: thesis: ( r1 < r2 implies (h | X) . r1 <= (h | X) . r2 )

then A2: ( h . r1 = (h | X) . r1 & h . r2 = (h | X) . r2 ) by FUNCT_1:47;

assume A3: r1 < r2 ; :: thesis: (h | X) . r1 <= (h | X) . r2

( r1 in dom h & r2 in dom h ) by A1, RELAT_1:57;

hence (h | X) . r1 <= (h | X) . r2 by A2, A3, Def3; :: thesis: verum

b