let f be ext-real-valued Function; :: thesis: ( f is trivial implies ( f is increasing & f is decreasing ) )
assume Z: f is trivial ; :: thesis: ( f is increasing & f is decreasing )
thus f is increasing :: thesis: f is decreasing

proof

let e1 be ext-real number ; :: according to VALUED_0:def 13 :: thesis: for e2 being ext-real number st e1 in dom f & e2 in dom f & e1 < e2 holds
f . e1 < f . e2
let e2 be ext-real number ; :: thesis: ( e1 in dom f & e2 in dom f & e1 < e2 implies f . e1 < f . e2 )
assume ( e1 in dom f & e2 in dom f ) ; :: thesis: ( not e1 < e2 or f . e1 < f . e2 )
then e1 = e2 by Z, ZFMISC_1:def 10;
hence ( not e1 < e2 or f . e1 < f . e2 ) ; :: thesis: verum

end;

let e1 be ext-real number ; :: according to VALUED_0:def 14 :: thesis: for e2 being ext-real number st e1 in dom f & e2 in dom f & e1 < e2 holds
f . e1 > f . e2
let e2 be ext-real number ; :: thesis: ( e1 in dom f & e2 in dom f & e1 < e2 implies f . e1 > f . e2 )
assume ( e1 in dom f & e2 in dom f ) ; :: thesis: ( not e1 < e2 or f . e1 > f . e2 )
then e1 = e2 by Z, ZFMISC_1:def 10;
hence ( not e1 < e2 or f . e1 > f . e2 ) ; :: thesis: verum