let Y be set ; :: thesis: for h being PartFunc of REAL ,REAL holds
( h | Y is increasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r1 < h . r2 )
let h be PartFunc of REAL ,REAL ; :: thesis: ( h | Y is increasing iff for r1, r2 being Element of 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 Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r2 > h . r1 ) :: thesis: ( ( for r1, r2 being Element of 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 Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r2 > h . r1
let r1, r2 be Element of REAL ; :: thesis: ( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 implies h . r2 > h . r1 )
assume A2: ( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 ) ; :: thesis: h . r2 > h . r1
B2: ( r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 ) by A2, RELAT_1:90;
( (h | Y) . r1 = h . r1 & (h | Y) . r2 = h . r2 ) by B2, FUNCT_1:70;
hence h . r2 > h . r1 by A1, NDef2, B2; :: thesis: verum

end;

assume A3: for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r2 > h . r1 ; :: thesis: h | Y is increasing
let r1 be Element of REAL ; :: according to RFUNCT_2:def 2 :: thesis: for r2 being Element of REAL st r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 holds
(h | Y) . r1 < (h | Y) . r2
let r2 be Element of REAL ; :: thesis: ( r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 implies (h | Y) . r1 < (h | Y) . r2 )
assume Z: ( r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 ) ; :: thesis: (h | Y) . r1 < (h | Y) . r2
then X: ( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 ) by RELAT_1:90;
( (h | Y) . r1 = h . r1 & (h | Y) . r2 = h . r2 ) by Z, FUNCT_1:70;
hence (h | Y) . r1 < (h | Y) . r2 by A3, X; :: thesis: verum