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 & () . P = R & () . Q = S ) by ;
consider N1 being invertible Matrix of 3,F_Real such that
A4: ( h1 = homography N1 & () . P = R & () . 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 & () . S = Q ) by ;
reconsider h3 = homography N3 as Element of SubGroupK-isometry by ;
consider h2 being Element of SubGroupK-isometry such that
A6: ex N being invertible Matrix of 3,F_Real st
( h2 = homography N & () . P = T & () . Q = U ) by ;
consider N2 being invertible Matrix of 3,F_Real such that
A7: ( h2 = homography N2 & () . P = T & () . 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 & () . R = T & () . S = U )
h2 * h3 is Element of SubGroupK-isometry ;
hence homography N4 is Element of SubGroupK-isometry by ; :: thesis: ( N4 is invertible Matrix of 3,F_Real & () . R = T & () . S = U )
thus N4 is invertible Matrix of 3,F_Real ; :: thesis: ( () . R = T & () . S = U )
( R in BK_model & S in BK_model ) ;
hence ( (homography N4) . R = T & () . S = U ) by ; :: thesis: verum
end;
hence R,S equiv T,U by Def05; :: thesis: verum