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

proof

let x be Real; :: thesis: ( x in ].(PI / 2),PI .[ implies diff sec ,x > 0 )
assume A4: x in ].(PI / 2),PI .[ ; :: thesis: diff sec ,x > 0
].(PI / 2),PI .[ c= ].0 ,PI .[ by XXREAL_1:46;
then A5: sin . x > 0 by A4, COMPTRIG:23;
PI <= (3 / 2) * PI by XREAL_1:153;
then ].(PI / 2),PI .[ c= ].(PI / 2),((3 / 2) * PI ).[ by XXREAL_1:46;
then cos . x < 0 by A4, COMPTRIG:29;
then (cos . x) ^2 > 0 ;
then (sin . x) / ((cos . x) ^2 ) > 0 / ((cos . x) ^2 ) by A5;
hence diff sec ,x > 0 by A4, Th6; :: thesis: verum

end;

PI / 2 < PI / 1 by XREAL_1:78;
hence sec | ].(PI / 2),PI .[ is increasing by A3, Th6, X2, ROLLE:9; :: thesis: verum