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

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

now :: thesis: for r1, r2 being Real st r1 in {x} /\ (dom h) & r2 in {x} /\ (dom h) & r1 < r2 holds

h . r1 > h . r2

hence
h | {x} is decreasing
by Th21; :: thesis: verumh . r1 > h . r2

let r1, r2 be Real; :: thesis: ( r1 in {x} /\ (dom h) & r2 in {x} /\ (dom h) & r1 < r2 implies h . r1 > h . r2 )

assume that

A1: r1 in {x} /\ (dom h) and

A2: r2 in {x} /\ (dom h) and

A3: r1 < r2 ; :: thesis: h . r1 > h . r2

r1 in {x} by A1, XBOOLE_0:def 4;

then A4: r1 = x by TARSKI:def 1;

r2 in {x} by A2, XBOOLE_0:def 4;

hence h . r1 > h . r2 by A3, A4, TARSKI:def 1; :: thesis: verum

end;assume that

A1: r1 in {x} /\ (dom h) and

A2: r2 in {x} /\ (dom h) and

A3: r1 < r2 ; :: thesis: h . r1 > h . r2

r1 in {x} by A1, XBOOLE_0:def 4;

then A4: r1 = x by TARSKI:def 1;

r2 in {x} by A2, XBOOLE_0:def 4;

hence h . r1 > h . r2 by A3, A4, TARSKI:def 1; :: thesis: verum