A1:
[.(tan . 0 ),(tan . 1).] = { r where r is Real : ( tan . 0 <= r & r <= tan . 1 ) }
by RCOMP_1:def 1;
[.(tan . 1),(tan . 0 ).] = {}
by Lm17, XXREAL_1:29;
then
1 in [.(tan . 0 ),(tan . 1).] \/ [.(tan . 1),(tan . 0 ).]
by A1, Lm17;
then consider th being Real such that
A4:
th in [.0 ,1.]
and
A5:
tan . th = 1
by Th75, Th76, FCONT_2:16;
A6:
0 <= th
by A4, XXREAL_1:1;
A7:
th <= 1
by A4, XXREAL_1:1;
A8:
0 < th
by A5, A6, Lm17;
A9:
th < 1
by A5, A7, Lm17, XXREAL_0:1;
take th1 = th * 4; ( tan . (th1 / 4) = 1 & th1 in ].0 ,4.[ )
thus
tan . (th1 / 4) = 1
by A5; th1 in ].0 ,4.[
th * 4 < 1 * 4
by A9, XREAL_1:70;
hence
th1 in ].0 ,4.[
by A8, XXREAL_1:4; verum