let th1, th2 be real number ; ( 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.[
; th1 = th2
A15:
0 < th1
by A12, XXREAL_1:4;
A16:
th1 < 4
by A12, XXREAL_1:4;
A17:
th1 / 4 < 4 / 4
by A16, XREAL_1:76;
A18:
th1 / 4 in ].0 ,1.[
by A15, A17, XXREAL_1:4;
A19:
0 < th2
by A14, XXREAL_1:4;
A20:
th2 < 4
by A14, XXREAL_1:4;
A21:
th2 / 4 < 4 / 4
by A20, XREAL_1:76;
A22:
th2 / 4 in ].0 ,1.[
by A19, A21, XXREAL_1:4;
A23:
th1 / 4 = th2 / 4
by A11, A13, A18, A22, Th77;
thus
th1 = th2
by A23; verum