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 )

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

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 A3:
M is triangle
; :: thesis: 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

end;the distance of M is triangle

proof

hence
M is triangle
; :: thesis: verum
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;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

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