let th1, th2 be Real; :: thesis: ( tan . (th1 / 4) = 1 & th1 in ].0,4.[ & tan . (th2 / 4) = 1 & th2 in ].0,4.[ implies th1 = th2 )
assume that
A8: tan . (th1 / 4) = 1 and
A9: th1 in ].0,4.[ and
A10: tan . (th2 / 4) = 1 and
A11: th2 in ].0,4.[ ; :: thesis: th1 = th2
A12: 0 < th1 by A9, XXREAL_1:4;
th1 < 4 by A9, XXREAL_1:4;
then th1 / 4 < 4 / 4 by XREAL_1:74;
then A13: th1 / 4 in ].0,1.[ by A12, XXREAL_1:4;
A14: 0 < th2 by A11, XXREAL_1:4;
th2 < 4 by A11, XXREAL_1:4;
then th2 / 4 < 4 / 4 by XREAL_1:74;
then th2 / 4 in ].0,1.[ by A14, XXREAL_1:4;
then th1 / 4 = th2 / 4 by A8, A10, A13, Th71;
hence th1 = th2 ; :: thesis: verum