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 . a,b = dist a,b ;
A3: the distance of M . a,c = dist a,c ;
the distance of M . b,c = dist b,c ;
hence the distance of M . a,c <= (the distance of M . a,b) + (the distance of M . b,c) by A1, A2, A3; :: thesis: verum

end;

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

end;

assume M is triangle ; :: thesis: for a, b, c being Element of M holds dist a,c <= (dist a,b) + (dist b,c)
then A4: the distance of M is triangle by Def10;
let a, b, c be Element of M; :: thesis: dist a,c <= (dist a,b) + (dist b,c)
thus dist a,c <= (dist a,b) + (dist b,c) by A4, Def6; :: thesis: verum