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 5 :: 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 ; :: 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;
hence dist (a,c) <= (dist (a,b)) + (dist (b,c)) ; :: thesis: verum