let p, q be Point of (TOP-REAL 2); :: thesis: dist p,q = sqrt ((((p `1 ) - (q `1 )) ^2 ) + (((p `2 ) - (q `2 )) ^2 ))
A1: p = |[(p `1 ),(p `2 )]| by EUCLID:57;
A2: q = |[(q `1 ),(q `2 )]| by EUCLID:57;
ex a, b being Point of (Euclid 2) st
( p = a & q = b & dist a,b = dist p,q ) by Def1;
hence dist p,q = sqrt ((((p `1 ) - (q `1 )) ^2 ) + (((p `2 ) - (q `2 )) ^2 )) by A1, A2, Th100; :: thesis: verum