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

proof

let x be Real; :: thesis: ( x in ].0 ,(PI / 2).[ implies diff sec ,x > 0 )
assume A1: x in ].0 ,(PI / 2).[ ; :: thesis: diff sec ,x > 0
].0 ,(PI / 2).[ c= ].(- (PI / 2)),(PI / 2).[ by XXREAL_1:46;
then A2: cos . x > 0 by A1, COMPTRIG:27;
PI / 2 < PI / 1 by XREAL_1:78;
then ].0 ,(PI / 2).[ c= ].0 ,PI .[ by XXREAL_1:46;
then sin . x > 0 by A1, COMPTRIG:23;
then (sin . x) / ((cos . x) ^2 ) > 0 / ((cos . x) ^2 ) by A2;
hence diff sec ,x > 0 by A1, Th5; :: thesis: verum

end;

hence sec | ].0 ,(PI / 2).[ is increasing by Lm9, Th1, Th5, ROLLE:9, XBOOLE_1:1; :: thesis: verum