id X is increasing

proof

let e1 be ext-real number ; :: according to VALUED_0:def 13 :: thesis: for e2 being ext-real number st e1 in dom (id X) & e2 in dom (id X) & e1 < e2 holds
(id X) . e1 < (id X) . e2
let e2 be ext-real number ; :: thesis: ( e1 in dom (id X) & e2 in dom (id X) & e1 < e2 implies (id X) . e1 < (id X) . e2 )
assume ( e1 in dom (id X) & e2 in dom (id X) ) ; :: thesis: ( not e1 < e2 or (id X) . e1 < (id X) . e2 )
then ( (id X) . e1 = e1 & (id X) . e2 = e2 ) by FUNCT_1:35;
hence ( not e1 < e2 or (id X) . e1 < (id X) . e2 ) ; :: thesis: verum

end;

hence for b₁ being Function of X,X st b₁ = id X holds
b₁ is increasing ; :: thesis: verum