let n be Element of NAT ; :: thesis: for p, q being Point of
for p', q' being Point of st p = p' & q = q' holds
dist p',q' = |.(p - q).|
let p, q be Point of ; :: thesis: for p', q' being Point of st p = p' & q = q' holds
dist p',q' = |.(p - q).|
let p', q' be Point of ; :: thesis: ( p = p' & q = q' implies dist p',q' = |.(p - q).| )
assume A1: ( p = p' & q = q' ) ; :: thesis: dist p',q' = |.(p - q).|
reconsider pp = p, qq = q as Element of REAL n by EUCLID:25;
dist p',q' = |.(pp - qq).| by A1, Th20;
hence dist p',q' = |.(p - q).| by EUCLID:73; :: thesis: verum