let n be Nat; Pitag_dist n is_metric_of REAL n
let x, y, z be Element of REAL n; PCOMPS_1:def 6 ( ( not (Pitag_dist n) . (x,y) = 0 or x = y ) & ( not x = y or (Pitag_dist n) . (x,y) = 0 ) & (Pitag_dist n) . (x,y) = (Pitag_dist n) . (y,x) & (Pitag_dist n) . (x,z) <= ((Pitag_dist n) . (x,y)) + ((Pitag_dist n) . (y,z)) )
A1:
(Pitag_dist n) . (y,z) = |.(y - z).|
by Def6;
(Pitag_dist n) . (x,y) = |.(x - y).|
by Def6;
hence
( (Pitag_dist n) . (x,y) = 0 iff x = y )
by Th13; ( (Pitag_dist n) . (x,y) = (Pitag_dist n) . (y,x) & (Pitag_dist n) . (x,z) <= ((Pitag_dist n) . (x,y)) + ((Pitag_dist n) . (y,z)) )
thus (Pitag_dist n) . (x,y) =
|.(x - y).|
by Def6
.=
|.(y - x).|
by Th15
.=
(Pitag_dist n) . (y,x)
by Def6
; (Pitag_dist n) . (x,z) <= ((Pitag_dist n) . (x,y)) + ((Pitag_dist n) . (y,z))
( (Pitag_dist n) . (x,y) = |.(x - y).| & (Pitag_dist n) . (x,z) = |.(x - z).| )
by Def6;
hence
(Pitag_dist n) . (x,z) <= ((Pitag_dist n) . (x,y)) + ((Pitag_dist n) . (y,z))
by A1, Th16; verum