let M be MetrStruct ; ( ( for a, b, c being Element of M holds dist (a,c) <= (dist (a,b)) + (dist (b,c)) ) iff M is triangle )
hereby ( M is triangle implies for a, b, c being Element of M holds dist (a,c) <= (dist (a,b)) + (dist (b,c)) )
assume A1:
for
a,
b,
c being
Element of
M holds
dist (
a,
c)
<= (dist (a,b)) + (dist (b,c))
;
M is triangle
the
distance of
M is
triangle
proof
let a,
b,
c be
Element of
M;
METRIC_1:def 5 the distance of M . (a,c) <= ( the distance of M . (a,b)) + ( the distance of M . (b,c))
A2:
the
distance of
M . (
b,
c)
= dist (
b,
c)
;
( the
distance of
M . (
a,
b)
= dist (
a,
b) & the
distance of
M . (
a,
c)
= dist (
a,
c) )
;
hence
the
distance of
M . (
a,
c)
<= ( the distance of M . (a,b)) + ( the distance of M . (b,c))
by A1, A2;
verum
end; hence
M is
triangle
;
verum
end;
assume A3:
M is triangle
; for a, b, c being Element of M holds dist (a,c) <= (dist (a,b)) + (dist (b,c))
let a, b, c be Element of M; dist (a,c) <= (dist (a,b)) + (dist (b,c))
the distance of M is triangle
by A3;
hence
dist (a,c) <= (dist (a,b)) + (dist (b,c))
; verum