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 Lm16, XXREAL_1:29;
then
1 in [.(tan . 0),(tan . 1).] \/ [.(tan . 1),(tan . 0).]
by A1, Lm16;
then consider th being Real such that
A2:
th in [.0,1.]
and
A3:
tan . th = 1
by Th69, Th70, FCONT_2:15;
A4:
0 <= th
by A2, XXREAL_1:1;
A5:
th <= 1
by A2, XXREAL_1:1;
A6:
0 < th
by A3, A4, Lm16;
A7:
th < 1
by A3, A5, Lm16, XXREAL_0:1;
take th1 = th * 4; ( tan . (th1 / 4) = 1 & th1 in ].0,4.[ )
thus
tan . (th1 / 4) = 1
by A3; th1 in ].0,4.[
th * 4 < 1 * 4
by A7, XREAL_1:68;
hence
th1 in ].0,4.[
by A6, XXREAL_1:4; verum