let a, b be POINT of BK-model-Plane; :: thesis: a,a equiv b,b
reconsider A = a, B = b as Element of BK_model ;
reconsider P = Dir |[1,0,1]| as Element of absolute by Th59;
consider N being invertible Matrix of 3,F_Real such that
A1: (homography N) .: absolute = absolute and
A2: (homography N) . a = b and
(homography N) . P = P by BKMODEL2:56;
homography N in { (homography N) where N is invertible Matrix of 3,F_Real : verum } ;
then reconsider h = homography N as Element of EnsHomography3 by ANPROJ_9:def 1;
h is_K-isometry by A1, BKMODEL2:def 6;
then h in EnsK-isometry by BKMODEL2:def 7;
then reconsider h = homography N as Element of SubGroupK-isometry by BKMODEL2:def 8;
ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st
( h = homography N & (homography N) . a = b & (homography N) . a = b )

proof

take h ; :: thesis: ex N being invertible Matrix of 3,F_Real st
( h = homography N & (homography N) . a = b & (homography N) . a = b )
take N ; :: thesis: ( h = homography N & (homography N) . a = b & (homography N) . a = b )
thus ( h = homography N & (homography N) . a = b & (homography N) . a = b ) by A2; :: thesis: verum

end;

hence a,a equiv b,b by BKMODEL3:def 8; :: thesis: verum