let h be REAL -defined real-valued Function; :: thesis: for Y being set holds
( h | Y is increasing iff for r1, r2 being Real st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r1 < h . r2 )
let Y be set ; :: thesis: ( h | Y is increasing iff for r1, r2 being Real st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r1 < h . r2 )
thus ( h | Y is increasing implies for r1, r2 being Real st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r2 > h . r1 ) :: thesis: ( ( for r1, r2 being Real st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r1 < h . r2 ) implies h | Y is increasing )

proof

assume A1: h | Y is increasing ; :: thesis: for r1, r2 being Real st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r2 > h . r1
let r1, r2 be Real; :: thesis: ( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 implies h . r2 > h . r1 )
assume that
A2: r1 in Y /\ (dom h) and
A3: r2 in Y /\ (dom h) and
A4: r1 < r2 ; :: thesis: h . r2 > h . r1
A5: r2 in dom (h | Y) by A3, RELAT_1:61;
then A6: (h | Y) . r2 = h . r2 by FUNCT_1:47;
A7: r1 in dom (h | Y) by A2, RELAT_1:61;
then (h | Y) . r1 = h . r1 by FUNCT_1:47;
hence h . r2 > h . r1 by A1, A4, A7, A5, A6; :: thesis: verum

end;

assume A8: for r1, r2 being Real st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r1 < h . r2 ; :: thesis: h | Y is increasing
let r1, r2 be ExtReal; :: according to VALUED_0:def 13 :: thesis: ( not r1 in dom (h | Y) or not r2 in dom (h | Y) or r2 <= r1 or not (h | Y) . r2 <= (h | Y) . r1 )
assume that
A9: ( r1 in dom (h | Y) & r2 in dom (h | Y) ) and
A10: r1 < r2 ; :: thesis: not (h | Y) . r2 <= (h | Y) . r1
aa: dom (h | Y) c= REAL by RELAT_1:def 18;
A11: ( (h | Y) . r1 = h . r1 & (h | Y) . r2 = h . r2 ) by A9, FUNCT_1:47;
( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) ) by A9, RELAT_1:61;
hence not (h | Y) . r2 <= (h | Y) . r1 by A11, A8, A10, aa, A9; :: thesis: verum