A1: 1 in [.(tan . 0 ),(tan . 1).]

proof

[.(tan . 0 ),(tan . 1).] = { r where r is Real : ( tan . 0 <= r & r <= tan . 1 ) } by RCOMP_1:def 1;
hence 1 in [.(tan . 0 ),(tan . 1).] by Lm21; :: thesis: verum

end;

[.(tan . 1),(tan . 0 ).] = {} by Lm21, XXREAL_1:29;
then 1 in [.(tan . 0 ),(tan . 1).] \/ [.(tan . 1),(tan . 0 ).] by A1;
then consider th being Real such that
A2: ( th in [.0 ,1.] & tan . th = 1 ) by Th76, Th75, FCONT_2:16;
( 0 <= th & th <= 1 ) by A2, XXREAL_1:1;
then A3: ( 0 < th & th < 1 ) by A2, Lm21, XXREAL_0:1;
take th1 = th * 4; :: thesis: ( tan . (th1 / 4) = 1 & th1 in ].0 ,4.[ )
thus tan . (th1 / 4) = 1 by A2; :: thesis: th1 in ].0 ,4.[
( 0 * 4 < th * 4 & th * 4 < 1 * 4 ) by A3, XREAL_1:70;
hence th1 in ].0 ,4.[ by XXREAL_1:4; :: thesis: verum