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:33
.= ||.(y - x).|| by Th31 ;
hence ( IT = ||.(x - y).|| implies IT = ||.(y - x).|| ) ; :: thesis: verum