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 Z: ( r1 in dom (h | X) & r2 in dom (h | X) ) ; :: thesis: ( r1 < r2 implies (h | X) . r1 > (h | X) . r2 )
then A: ( r1 in dom h & r2 in dom h ) by RELAT_1:86;
B: ( h . r1 = (h | X) . r1 & h . r2 = (h | X) . r2 ) by Z, FUNCT_1:70;
assume r1 < r2 ; :: thesis: (h | X) . r1 > (h | X) . r2
hence (h | X) . r1 > (h | X) . r2 by B, A, NDef3; :: thesis: verum

end;

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