let P, Q, R, S, T, U be POINT of BK-model-Plane; :: according to GTARSKI1:def 6 :: thesis: ( not P,Q equiv R,S or not P,Q equiv T,U or R,S equiv T,U )
assume that
A1: P,Q equiv R,S and
A2: P,Q equiv T,U ; :: thesis: R,S equiv T,U
consider h1 being Element of SubGroupK-isometry such that
A3: ex N being invertible Matrix of 3,F_Real st
( h1 = homography N & (homography N) . P = R & (homography N) . Q = S ) by A1, Def05;
consider N1 being invertible Matrix of 3,F_Real such that
A4: ( h1 = homography N1 & (homography N1) . P = R & (homography N1) . Q = S ) by A3;
reconsider N3 = N1 ~ as invertible Matrix of 3,F_Real ;
( P in BK_model & Q in BK_model ) ;
then A5: ( (homography N3) . R = P & (homography N3) . S = Q ) by A4, ANPROJ_9:15;
reconsider h3 = homography N3 as Element of SubGroupK-isometry by A4, BKMODEL2:47;
consider h2 being Element of SubGroupK-isometry such that
A6: ex N being invertible Matrix of 3,F_Real st
( h2 = homography N & (homography N) . P = T & (homography N) . Q = U ) by A2, Def05;
consider N2 being invertible Matrix of 3,F_Real such that
A7: ( h2 = homography N2 & (homography N2) . P = T & (homography N2) . Q = U ) by A6;
reconsider N4 = N2 * N3 as invertible Matrix of 3,F_Real ;
now :: thesis: ( homography N4 is Element of SubGroupK-isometry & N4 is invertible Matrix of 3,F_Real & (homography N4) . R = T & (homography N4) . S = U )
h2 * h3 is Element of SubGroupK-isometry ;
hence homography N4 is Element of SubGroupK-isometry by A7, BKMODEL2:46; :: thesis: ( N4 is invertible Matrix of 3,F_Real & (homography N4) . R = T & (homography N4) . S = U )
thus N4 is invertible Matrix of 3,F_Real ; :: thesis: ( (homography N4) . R = T & (homography N4) . S = U )
( R in BK_model & S in BK_model ) ;
hence ( (homography N4) . R = T & (homography N4) . S = U ) by A5, A7, ANPROJ_9:13; :: thesis: verum
end;
hence R,S equiv T,U by Def05; :: thesis: verum