for x0 being Real st x0 in ].(PI / 2),PI.[ holds
diff (sec,x0) > 0

proof

let x0 be Real; :: thesis: ( x0 in ].(PI / 2),PI.[ implies diff (sec,x0) > 0 )
assume A1: x0 in ].(PI / 2),PI.[ ; :: thesis: diff (sec,x0) > 0
].(PI / 2),PI.[ c= ].(PI / 2),((3 / 2) * PI).[ by COMPTRIG:5, XXREAL_1:46;
then A2: cos . x0 < 0 by A1, COMPTRIG:13;
].(PI / 2),PI.[ c= ].0,PI.[ by XXREAL_1:46;
then sin . x0 > 0 by A1, COMPTRIG:7;
then (sin . x0) / ((cos . x0) ^2) > 0 / ((cos . x0) ^2) by A2;
hence diff (sec,x0) > 0 by A1, Th6; :: thesis: verum

end;

then rng (sec | ].(PI / 2),PI.[) is open by Lm12, Th6, FDIFF_2:41;
hence sec .: ].(PI / 2),PI.[ is open by RELAT_1:115; :: thesis: verum