let p1, p2 be Point of (TOP-REAL 2); :: thesis: ( abs ((p1 `1 ) - (p2 `1 )) <= |.(p1 - p2).| & abs ((p1 `2 ) - (p2 `2 )) <= |.(p1 - p2).| )
( (p1 `1 ) - (p2 `1 ) = (p1 - p2) `1 & (p1 `2 ) - (p2 `2 ) = (p1 - p2) `2 ) by TOPREAL3:8;
hence ( abs ((p1 `1 ) - (p2 `1 )) <= |.(p1 - p2).| & abs ((p1 `2 ) - (p2 `2 )) <= |.(p1 - p2).| ) by Th50; :: thesis: verum