let A, B, C be Point of (TOP-REAL 2); :: thesis: ( A <> B & A <> C implies |.(A - B).| + |.(A - C).| <> 0 )
assume ( A <> B & A <> C ) ; :: thesis: |.(A - B).| + |.(A - C).| <> 0
then ( |.(A - B).| <> 0 & |.(A - C).| <> 0 ) by EUCLID_6:42;
hence |.(A - B).| + |.(A - C).| <> 0 ; :: thesis: verum