let IT be Real; :: thesis: for x, y being Point of st IT = ||.(x - y).|| holds
IT = ||.(y - x).||
let x, y be Point of ; :: thesis: ( IT = ||.(x - y).|| implies IT = ||.(y - x).|| )
||.(x - y).|| = ||.(- (y - x)).|| by RLVECT_1:47
.= ||.(y - x).|| by Th37 ;
hence ( IT = ||.(x - y).|| implies IT = ||.(y - x).|| ) ; :: thesis: verum