:: deftheorem Def05 defines BK-model-Equidistance BKMODEL3:def 8 :
for b₁ being Relation of [:BK_model,BK_model:],[:BK_model,BK_model:] holds
( b₁ = BK-model-Equidistance iff for a, b, c, d being Element of BK_model holds
( [[a,b],[c,d]] in b₁ iff ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st
( h = homography N & (homography N) . a = c & (homography N) . b = d ) ) );