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= ].0 ,PI .[ by XXREAL_1:46;
then A2: sin . x0 > 0 by A1, COMPTRIG:23;
].(PI / 2),PI .[ c= ].(PI / 2),((3 / 2) * PI ).[ by COMPTRIG:21, XXREAL_1:46;
then cos . x0 < 0 by A1, COMPTRIG:29;
then (cos . x0) ^2 > 0 ;
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 Th6, X2, FDIFF_2:41;
hence sec .: ].(PI / 2),PI .[ is open by RELAT_1:148; :: thesis: verum