now

let r1, r2 be Element of 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:70;
assume A3: r1 < r2 ; :: thesis: (h | X) . r1 > (h | X) . r2
( r1 in dom h & r2 in dom h ) by A1, RELAT_1:86;
hence (h | X) . r1 > (h | X) . r2 by A2, A3, Def3; :: thesis: verum

end;

hence for b₁ being PartFunc of REAL ,REAL st b₁ = h | X holds
b₁ is decreasing by Def3; :: thesis: verum