A1: [.(tan . 0 ),(tan . 1).] = { r where r is Real : ( tan . 0 <= r & r <= tan . 1 ) } by RCOMP_1:def 1;
A2: [.(tan . 1),(tan . 0 ).] = {} by Lm17, XXREAL_1:29;
A3: 1 in [.(tan . 0 ),(tan . 1).] \/ [.(tan . 1),(tan . 0 ).] by A1, A2, Lm17;
consider th being Real such that
A4: th in [.0 ,1.] and
A5: tan . th = 1 by A3, 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; :: thesis: ( tan . (th1 / 4) = 1 & th1 in ].0 ,4.[ )
thus tan . (th1 / 4) = 1 by A5; :: thesis: th1 in ].0 ,4.[
A10: th * 4 < 1 * 4 by A9, XREAL_1:70;
thus th1 in ].0 ,4.[ by A8, A10, XXREAL_1:4; :: thesis: verum