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
A4: ( tan . (th1 / 4) = 1 & th1 in ].0 ,4.[ ) and
A5: ( tan . (th2 / 4) = 1 & th2 in ].0 ,4.[ ) ; :: thesis: th1 = th2
( th1 / 4 in ].0 ,1.[ & th2 / 4 in ].0 ,1.[ )

proof

( 0 < th1 & th1 < 4 ) by A4, XXREAL_1:4;
then ( 0 / 4 < th1 / 4 & th1 / 4 < 4 / 4 ) by XREAL_1:76;
hence th1 / 4 in ].0 ,1.[ by XXREAL_1:4; :: thesis: th2 / 4 in ].0 ,1.[
( 0 < th2 & th2 < 4 ) by A5, XXREAL_1:4;
then ( 0 / 4 < th2 / 4 & th2 / 4 < 4 / 4 ) by XREAL_1:76;
hence th2 / 4 in ].0 ,1.[ by XXREAL_1:4; :: thesis: verum

end;

then th1 / 4 = th2 / 4 by A4, A5, Th77;
hence th1 = th2 ; :: thesis: verum