let IT be Real; :: thesis: for x, y being Point of X st IT = ||.(x - y).|| holds
IT = ||.(y - x).||
let x, y be Point of X; :: 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