let r be Real; ( 0 <= r & r <= PI / 2 & cos r = 1 / 2 implies r = PI / 3 )
set X = [.0,(PI / 2).];
set f = cos | [.0,(PI / 2).];
assume that
A1:
0 <= r
and
A2:
r <= PI / 2
; ( not cos r = 1 / 2 or r = PI / 3 )
A3:
r in [.0,(PI / 2).]
by A1, A2, XXREAL_1:1;
assume A4:
cos r = 1 / 2
; r = PI / 3
A5:
dom cos = REAL
by FUNCT_2:def 1;
A6:
PI / 3 <= PI / 2
by XREAL_1:76;
then A7:
PI / 3 in [.0,(PI / 2).]
by XXREAL_1:1;
A8:
dom (cos | [.0,(PI / 2).]) = [.0,(PI / 2).]
by A5, RELAT_1:62;
then (cos | [.0,(PI / 2).]) . r =
cos (PI / 3)
by A1, A2, A4, EUCLID10:14, XXREAL_1:1, FUNCT_1:47
.=
(cos | [.0,(PI / 2).]) . (PI / 3)
by A6, A8, XXREAL_1:1, FUNCT_1:47
;
hence
r = PI / 3
by A3, A7, A8, FUNCT_1:def 4; verum