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

now :: thesis: for r1, r2 being Real st r1 in R /\ (dom (id R)) & r2 in R /\ (dom (id R)) & r1 < r2 holds

(id R) . r1 < (id R) . r2

hence
(id R) | R is increasing
by Th20; :: thesis: verum(id R) . r1 < (id R) . r2

let r1, r2 be Real; :: thesis: ( r1 in R /\ (dom (id R)) & r2 in R /\ (dom (id R)) & r1 < r2 implies (id R) . r1 < (id R) . r2 )

assume that

A1: r1 in R /\ (dom (id R)) and

A2: r2 in R /\ (dom (id R)) and

A3: r1 < r2 ; :: thesis: (id R) . r1 < (id R) . r2

r1 in R by A1, XBOOLE_0:def 4;

then A4: (id R) . r1 = r1 by FUNCT_1:18;

r2 in R by A2, XBOOLE_0:def 4;

hence (id R) . r1 < (id R) . r2 by A3, A4, FUNCT_1:18; :: thesis: verum

end;assume that

A1: r1 in R /\ (dom (id R)) and

A2: r2 in R /\ (dom (id R)) and

A3: r1 < r2 ; :: thesis: (id R) . r1 < (id R) . r2

r1 in R by A1, XBOOLE_0:def 4;

then A4: (id R) . r1 = r1 by FUNCT_1:18;

r2 in R by A2, XBOOLE_0:def 4;

hence (id R) . r1 < (id R) . r2 by A3, A4, FUNCT_1:18; :: thesis: verum