let M be MetrStruct ; :: thesis: ( ( for a, b, c being Element of M holds dist a,c <= (dist a,b) + (dist b,c) ) iff M is triangle )

hereby :: thesis: ( 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) ; :: thesis: M is triangle
the distance of M is triangle

proof

let a, b, c be Element of M; :: according to METRIC_1:def 6 :: thesis: 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; :: thesis: verum

end;

hence M is triangle by Def10; :: thesis: verum

end;

assume A3: M is triangle ; :: thesis: 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; :: thesis: dist a,c <= (dist a,b) + (dist b,c)
the distance of M is triangle by A3, Def10;
hence dist a,c <= (dist a,b) + (dist b,c) by Def6; :: thesis: verum