let A, B, C be Point of (TOP-REAL 2); ( A,C,B is_a_triangle & angle (C,A,B) = PI / 2 implies the_length_of_the_altitude (C,A,B) = |.(A - B).| * (tan (angle (A,B,C))) )
assume that
A1:
A,C,B is_a_triangle
and
A2:
angle (C,A,B) = PI / 2
; the_length_of_the_altitude (C,A,B) = |.(A - B).| * (tan (angle (A,B,C)))
A3:
A,C,B are_mutually_distinct
by A1, EUCLID_6:20;
then
|((B - A),(C - A))| = 0
by A2, EUCLID_3:45;
then A4:
|((A - B),(A - C))| = 0
by Th10;
(tan (angle (A,B,C))) * |.(A - B).| =
(|.(A - C).| / |.(A - B).|) * |.(A - B).|
by A1, A2, EUCLID10:35
.=
|.(A - C).|
by A3, EUCLID_6:42, XCMPLX_1:87
.=
|.(C - A).|
by EUCLID_6:43
;
then (tan (angle (A,B,C))) * |.(A - B).| =
|.((the_foot_of_the_altitude (C,A,B)) - C).|
by A4, A3, Th47
.=
|.(C - (the_foot_of_the_altitude (C,A,B))).|
by EUCLID_6:43
;
hence
the_length_of_the_altitude (C,A,B) = |.(A - B).| * (tan (angle (A,B,C)))
by A3, Def3; verum