let th1, th2 be real number ; :: thesis: ( th1 in ].0 ,1.[ & th2 in ].0 ,1.[ & tan . th1 = tan . th2 implies th1 = th2 )
assume A1: ( th1 in ].0 ,1.[ & th2 in ].0 ,1.[ & tan . th1 = tan . th2 ) ; :: thesis: th1 = th2
then A2: ( 0 < th1 & th1 < 1 & 0 < th2 & th2 < 1 ) by XXREAL_1:4;
assume A3: th1 <> th2 ; :: thesis: contradiction
ex th being real number st
( th in ].0 ,1.[ & diff tan ,th = 0 )

proof

now

per cases ( th1 < th2 or th2 < th1 ) by A3, XXREAL_0:1;

suppose A4: th1 < th2 ; :: thesis: ex th being Real st
( th in ].0 ,1.[ & diff tan ,th = 0 )

A5: ( ].th1,th2.[ is open Subset of REAL & ].th1,th2.[ c= ].0 ,1.[ & [.th1,th2.] c= [.0 ,1.] )

proof

A6: for th being Real st th in ].th1,th2.[ holds
th in ].0 ,1.[

proof

let th be Real; :: thesis: ( th in ].th1,th2.[ implies th in ].0 ,1.[ )
assume th in ].th1,th2.[ ; :: thesis: th in ].0 ,1.[
then A7: ( th1 < th & th < th2 ) by XXREAL_1:4;
then th < 1 by A2, XXREAL_0:2;
hence th in ].0 ,1.[ by A2, A7, XXREAL_1:4; :: thesis: verum

end;

for th being Real st th in [.th1,th2.] holds
th in [.0 ,1.]

proof

let th be Real; :: thesis: ( th in [.th1,th2.] implies th in [.0 ,1.] )
assume th in [.th1,th2.] ; :: thesis: th in [.0 ,1.]
then A8: ( th1 <= th & th <= th2 ) by XXREAL_1:1;
then th <= 1 by A2, XXREAL_0:2;
hence th in [.0 ,1.] by A2, A8, XXREAL_1:1; :: thesis: verum

end;

hence ( ].th1,th2.[ is open Subset of REAL & ].th1,th2.[ c= ].0 ,1.[ & [.th1,th2.] c= [.0 ,1.] ) by A6, SUBSET_1:7; :: thesis: verum

end;

then A9: tan is_differentiable_on ].th1,th2.[ by Lm20, FDIFF_1:34;
tan | [.th1,th2.] is continuous by A5, Th76, FCONT_1:17;
then consider r being Real such that
A10: ( r in ].th1,th2.[ & diff tan ,r = 0 ) by A1, A4, A9, A5, Th75, ROLLE:1, XBOOLE_1:1;
take th = r; :: thesis: ( th in ].0 ,1.[ & diff tan ,th = 0 )
thus ( th in ].0 ,1.[ & diff tan ,th = 0 ) by A5, A10; :: thesis: verum

end;

suppose A11: th2 < th1 ; :: thesis: ex th being Real st
( th in ].0 ,1.[ & diff tan ,th = 0 )

A12: ( ].th2,th1.[ is open Subset of REAL & ].th2,th1.[ c= ].0 ,1.[ & [.th2,th1.] c= [.0 ,1.] )

proof

A13: for th being Real st th in ].th2,th1.[ holds
th in ].0 ,1.[

proof

let th be Real; :: thesis: ( th in ].th2,th1.[ implies th in ].0 ,1.[ )
assume th in ].th2,th1.[ ; :: thesis: th in ].0 ,1.[
then A14: ( th2 < th & th < th1 ) by XXREAL_1:4;
then th < 1 by A2, XXREAL_0:2;
hence th in ].0 ,1.[ by A2, A14, XXREAL_1:4; :: thesis: verum

end;

for th being Real st th in [.th2,th1.] holds
th in [.0 ,1.]

proof

let th be Real; :: thesis: ( th in [.th2,th1.] implies th in [.0 ,1.] )
assume th in [.th2,th1.] ; :: thesis: th in [.0 ,1.]
then A15: ( th2 <= th & th <= th1 ) by XXREAL_1:1;
then th <= 1 by A2, XXREAL_0:2;
hence th in [.0 ,1.] by A2, A15, XXREAL_1:1; :: thesis: verum

end;

hence ( ].th2,th1.[ is open Subset of REAL & ].th2,th1.[ c= ].0 ,1.[ & [.th2,th1.] c= [.0 ,1.] ) by A13, SUBSET_1:7; :: thesis: verum

end;

then A16: tan is_differentiable_on ].th2,th1.[ by Lm20, FDIFF_1:34;
tan | [.th2,th1.] is continuous by A12, Th76, FCONT_1:17;
then consider r being Real such that
A17: ( r in ].th2,th1.[ & diff tan ,r = 0 ) by A1, A11, A16, A12, Th75, ROLLE:1, XBOOLE_1:1;
take th = r; :: thesis: ( th in ].0 ,1.[ & diff tan ,th = 0 )
thus ( th in ].0 ,1.[ & diff tan ,th = 0 ) by A12, A17; :: thesis: verum

end;

end;

end;

hence ex th being real number st
( th in ].0 ,1.[ & diff tan ,th = 0 ) ; :: thesis: verum

end;

hence contradiction by Lm20; :: thesis: verum