let R be Subset of REAL ; :: thesis: (id R) | R is increasing

now

let r1, r2 be Element of REAL ; :: thesis: ( r1 in R /\ (dom (id R)) & r2 in R /\ (dom (id R)) & r1 < r2 implies (id R) . r1 < (id R) . r2 )
assume A1: ( r1 in R /\ (dom (id R)) & r2 in R /\ (dom (id R)) & r1 < r2 ) ; :: thesis: (id R) . r1 < (id R) . r2
then ( r1 in R & r1 in dom (id R) & r2 in R & r2 in dom (id R) ) by XBOOLE_0:def 4;
then ( (id R) . r1 = r1 & (id R) . r2 = r2 ) by FUNCT_1:35;
hence (id R) . r1 < (id R) . r2 by A1; :: thesis: verum

end;

hence (id R) | R is increasing by Def2; :: thesis: verum