let X be set ; for A being Subset of X
for er being ExtReal holds
( ( er >= 0 implies chi (er,A,X) is nonnegative ) & ( er <= 0 implies chi (er,A,X) is nonpositive ) )
let A be Subset of X; for er being ExtReal holds
( ( er >= 0 implies chi (er,A,X) is nonnegative ) & ( er <= 0 implies chi (er,A,X) is nonpositive ) )
let er be ExtReal; ( ( er >= 0 implies chi (er,A,X) is nonnegative ) & ( er <= 0 implies chi (er,A,X) is nonpositive ) )
hereby ( er <= 0 implies chi (er,A,X) is nonpositive )
assume a1:
er >= 0
;
chi (er,A,X) is nonnegative now for x being object st x in dom (chi (er,A,X)) holds
(chi (er,A,X)) . x >= 0 let x be
object ;
( x in dom (chi (er,A,X)) implies (chi (er,A,X)) . x >= 0 )assume a2:
x in dom (chi (er,A,X))
;
(chi (er,A,X)) . x >= 0
(
x in A implies
(chi (er,A,X)) . x >= 0 )
by a1, Def1;
hence
(chi (er,A,X)) . x >= 0
by a2, Def1;
verum end; hence
chi (
er,
A,
X) is
nonnegative
by SUPINF_2:52;
verum
end;
assume a3:
er <= 0
; chi (er,A,X) is nonpositive
now for x being set st x in dom (chi (er,A,X)) holds
(chi (er,A,X)) . x <= 0 let x be
set ;
( x in dom (chi (er,A,X)) implies (chi (er,A,X)) . x <= 0 )assume a4:
x in dom (chi (er,A,X))
;
(chi (er,A,X)) . x <= 0
(
x in A implies
(chi (er,A,X)) . x <= 0 )
by a3, Def1;
hence
(chi (er,A,X)) . x <= 0
by a4, Def1;
verum end;
hence
chi (er,A,X) is nonpositive
by MESFUNC5:9; verum