let th1, th2 be real number ; :: thesis: ( tan . (th1 / 4) = 1 & th1 in ].0 ,4.[ & tan . (th2 / 4) = 1 & th2 in ].0 ,4.[ implies th1 = th2 )
assume that
A11: tan . (th1 / 4) = 1 and
A12: th1 in ].0 ,4.[ and
A13: tan . (th2 / 4) = 1 and
A14: th2 in ].0 ,4.[ ; :: thesis: th1 = th2
A15: 0 < th1 by A12, XXREAL_1:4;
th1 < 4 by A12, XXREAL_1:4;
then th1 / 4 < 4 / 4 by XREAL_1:76;
then A18: th1 / 4 in ].0 ,1.[ by A15, XXREAL_1:4;
A19: 0 < th2 by A14, XXREAL_1:4;
th2 < 4 by A14, XXREAL_1:4;
then th2 / 4 < 4 / 4 by XREAL_1:76;
then th2 / 4 in ].0 ,1.[ by A19, XXREAL_1:4;
then th1 / 4 = th2 / 4 by A11, A13, A18, Th77;
hence th1 = th2 ; :: thesis: verum