theorem THYQ: :: GTARSKI2:8

for a, b, c, d being Real holds dist (|[a,b]|,|[c,d]|) = sqrt (((a - c) ^2) + ((b - d) ^2))