let x be set ; :: thesis: for h being PartFunc of REAL ,REAL holds h | {x} is decreasing
let h be PartFunc of REAL ,REAL ; :: thesis: h | {x} is decreasing

now

let r1, r2 be Element of REAL ; :: thesis: ( r1 in {x} /\ (dom h) & r2 in {x} /\ (dom h) & r1 < r2 implies h . r1 > h . r2 )
assume A1: ( r1 in {x} /\ (dom h) & r2 in {x} /\ (dom h) & r1 < r2 ) ; :: thesis: h . r1 > h . r2
then ( r1 in {x} & r2 in {x} ) by XBOOLE_0:def 4;
then ( r1 = x & r2 = x ) by TARSKI:def 1;
hence h . r1 > h . r2 by A1; :: thesis: verum

end;

hence h | {x} is decreasing by Def3; :: thesis: verum