let r be Real; :: thesis: ( 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 ; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum