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 ;

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 )

hence
R,S equiv T,U
by Def05; :: thesis: verum
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 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