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:53;
A2: q = |[(q `1),(q `2)]| by EUCLID:53;
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, Th84; :: thesis: verum