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