:: Beltrami-Klein model, Part {II}
:: by Roland Coghetto
::
:: Received March 27, 2018
:: Copyright (c) 2018-2021 Association of Mizar Users


definition
func BK_model -> non empty Subset of (ProjectiveSpace (TOP-REAL 3)) equals :: BKMODEL2:def 1
 negative_conic (1,1,(- 1),0,0,0);
coherence
negative_conic (1,1,(- 1),0,0,0) is non empty Subset of (ProjectiveSpace (TOP-REAL 3))
proof end;
end;

:: deftheorem defines BK_model BKMODEL2:def 1 :
BK_model = negative_conic (1,1,(- 1),0,0,0);

theorem Th01: :: BKMODEL2:1
BK_model misses absolute
proof end;

theorem :: BKMODEL2:2
for P being Element of (ProjectiveSpace (TOP-REAL 3))
for u being non zero Element of (TOP-REAL 3) st P = Dir u & P in BK_model holds
u . 3 <> 0
proof end;

definition
let P be Element of BK_model ;
func BK_to_REAL2 P -> Element of inside_of_circle (0,0,1) means :Def01: :: BKMODEL2:def 2
 ex u being non zero Element of (TOP-REAL 3) st
( Dir u = P & u . 3 = 1 & it = |[(u . 1),(u . 2)]| );
existence
ex b1 being Element of inside_of_circle (0,0,1) ex u being non zero Element of (TOP-REAL 3) st
( Dir u = P & u . 3 = 1 & b1 = |[(u . 1),(u . 2)]| )
proof end;
uniqueness
for b1, b2 being Element of inside_of_circle (0,0,1) st ex u being non zero Element of (TOP-REAL 3) st
( Dir u = P & u . 3 = 1 & b1 = |[(u . 1),(u . 2)]| ) & ex u being non zero Element of (TOP-REAL 3) st
( Dir u = P & u . 3 = 1 & b2 = |[(u . 1),(u . 2)]| ) holds
b1 = b2
proof end;
end;

:: deftheorem Def01 defines BK_to_REAL2 BKMODEL2:def 2 :
for P being Element of BK_model
for b2 being Element of inside_of_circle (0,0,1) holds
( b2 = BK_to_REAL2 P iff ex u being non zero Element of (TOP-REAL 3) st
( Dir u = P & u . 3 = 1 & b2 = |[(u . 1),(u . 2)]| ) );

definition
let Q be Element of inside_of_circle (0,0,1);
func REAL2_to_BK Q -> Element of BK_model means :Def02: :: BKMODEL2:def 3
 ex P being Element of (TOP-REAL 2) st
( P = Q & it = Dir |[(P `1),(P `2),1]| );
existence
ex b1 being Element of BK_model ex P being Element of (TOP-REAL 2) st
( P = Q & b1 = Dir |[(P `1),(P `2),1]| )
proof end;
uniqueness
for b1, b2 being Element of BK_model st ex P being Element of (TOP-REAL 2) st
( P = Q & b1 = Dir |[(P `1),(P `2),1]| ) & ex P being Element of (TOP-REAL 2) st
( P = Q & b2 = Dir |[(P `1),(P `2),1]| ) holds
b1 = b2 ;
end;

:: deftheorem Def02 defines REAL2_to_BK BKMODEL2:def 3 :
for Q being Element of inside_of_circle (0,0,1)
for b2 being Element of BK_model holds
( b2 = REAL2_to_BK Q iff ex P being Element of (TOP-REAL 2) st
( P = Q & b2 = Dir |[(P `1),(P `2),1]| ) );

theorem :: BKMODEL2:3
for P being Element of BK_model holds REAL2_to_BK (BK_to_REAL2 P) = P
proof end;

theorem Th02: :: BKMODEL2:4
for P, Q being Element of BK_model holds
( P = Q iff BK_to_REAL2 P = BK_to_REAL2 Q )
proof end;

theorem :: BKMODEL2:5
for Q being Element of inside_of_circle (0,0,1) holds BK_to_REAL2 (REAL2_to_BK Q) = Q
proof end;

theorem :: BKMODEL2:6
for P, Q being Element of BK_model
for P1, P2, P3 being Element of absolute st P <> Q & P1 <> P2 & P,Q,P1 are_collinear & P,Q,P2 are_collinear & P,Q,P3 are_collinear & not P3 = P1 holds
P3 = P2
proof end;

theorem Th03: :: BKMODEL2:7
for P being Element of BK_model
for Q being Element of (ProjectiveSpace (TOP-REAL 3))
for v being non zero Element of (TOP-REAL 3) st P <> Q & Q = Dir v & v . 3 = 1 holds
ex P1 being Element of absolute st P,Q,P1 are_collinear
proof end;

theorem :: BKMODEL2:8
for P being Element of BK_model
for L being LINE of (IncProjSp_of real_projective_plane) ex Q being Element of (ProjectiveSpace (TOP-REAL 3)) st
( P <> Q & Q in L )
proof end;

theorem Th04: :: BKMODEL2:9
for a, b, c, d, e being Real
for u, v, w being Element of (TOP-REAL 3) st u = |[a,b,e]| & v = |[c,d,0]| & w = |[(a + c),(b + d),e]| holds
|{u,v,w}| = 0
proof end;

theorem Th05: :: BKMODEL2:10
for a, b being Real
for c being non zero Real holds |[a,b,c]| is non zero Element of (TOP-REAL 3)
proof end;

theorem Th06: :: BKMODEL2:11
for u, v being Element of (TOP-REAL 3)
for a, b, c, d, e being Real st u = |[a,b,c]| & v = |[d,e,0]| & are_Prop u,v holds
c = 0
proof end;

theorem :: BKMODEL2:12
for P, Q, R being Element of (ProjectiveSpace (TOP-REAL 3))
for u, v, w being non zero Element of (TOP-REAL 3) st P = Dir u & Q = Dir v & R = Dir w & u `3 <> 0 & v `3 = 0 & w = |[((u `1) + (v `1)),((u `2) + (v `2)),(u `3)]| holds
( R <> P & R <> Q )
proof end;

theorem Th07: :: BKMODEL2:13
for L being LINE of (IncProjSp_of real_projective_plane)
for P, Q being Element of (ProjectiveSpace (TOP-REAL 3)) st P <> Q & P in L & Q in L holds
L = Line (P,Q)
proof end;

theorem :: BKMODEL2:14
for L being LINE of (IncProjSp_of real_projective_plane)
for P, Q being Element of (ProjectiveSpace (TOP-REAL 3))
for u, v being non zero Element of (TOP-REAL 3) st P in L & Q in L & P = Dir u & Q = Dir v & u `3 <> 0 & v `3 = 0 holds
( P <> Q & Dir |[((u `1) + (v `1)),((u `2) + (v `2)),(u `3)]| in L )
proof end;

theorem Th08: :: BKMODEL2:15
for u, v, w being Element of (TOP-REAL 3) st v `3 = 0 & w = |[((u `1) + (v `1)),((u `2) + (v `2)),(u `3)]| holds
|{u,v,w}| = 0
proof end;

theorem Th09: :: BKMODEL2:16
for L being LINE of (IncProjSp_of real_projective_plane)
for P being Element of (ProjectiveSpace (TOP-REAL 3))
for u being non zero Element of (TOP-REAL 3) st P = Dir u & P in L & u . 3 <> 0 holds
ex Q being Element of (ProjectiveSpace (TOP-REAL 3)) ex v being non zero Element of (TOP-REAL 3) st
( Q = Dir v & Q in L & P <> Q & v . 3 <> 0 )
proof end;

theorem Th10: :: BKMODEL2:17
for P being Element of BK_model
for L being LINE of (IncProjSp_of real_projective_plane) st P in L holds
ex Q being Element of (ProjectiveSpace (TOP-REAL 3)) st
( P <> Q & Q in L & ( for u being non zero Element of (TOP-REAL 3) st Q = Dir u holds
u . 3 <> 0 ) )
proof end;

theorem Th11: :: BKMODEL2:18
for u, v being non zero Element of (TOP-REAL 3)
for k being non zero Real st u = k * v holds
Dir u = Dir v
proof end;

theorem :: BKMODEL2:19
for P being Element of BK_model
for Q being Element of (ProjectiveSpace (TOP-REAL 3)) st P <> Q holds
ex P1 being Element of absolute st P,Q,P1 are_collinear
proof end;

theorem Th12: :: BKMODEL2:20
for P, Q being Element of BK_model st P <> Q holds
ex P1, P2 being Element of absolute st
( P1 <> P2 & P,Q,P1 are_collinear & P,Q,P2 are_collinear )
proof end;

theorem Th13: :: BKMODEL2:21
for P, Q, R being Element of real_projective_plane
for u, v, w being non zero Element of (TOP-REAL 3)
for a, b, c, d being Real st P in BK_model & Q in absolute & P = Dir u & Q = Dir v & R = Dir w & u = |[a,b,1]| & v = |[c,d,1]| & w = |[((a + c) / 2),((b + d) / 2),1]| holds
( R in BK_model & R <> P & P,R,Q are_collinear )
proof end;

theorem Th14: :: BKMODEL2:22
for P, Q being Element of real_projective_plane st P in absolute & Q in BK_model holds
ex R being Element of real_projective_plane st
( R in BK_model & Q <> R & R,Q,P are_collinear )
proof end;

theorem Th15: :: BKMODEL2:23
for L being LINE of (IncProjSp_of real_projective_plane)
for p, q being POINT of (IncProjSp_of real_projective_plane)
for P, Q being Element of real_projective_plane st p = P & q = Q & P in BK_model & Q in absolute & q on L & p on L holds
ex p1, p2 being POINT of (IncProjSp_of real_projective_plane) ex P1, P2 being Element of real_projective_plane st
( p1 = P1 & p2 = P2 & P1 <> P2 & P1 in absolute & P2 in absolute & p1 on L & p2 on L )
proof end;

theorem Th16: :: BKMODEL2:24
for P being Element of BK_model
for Q being Element of absolute ex R being Element of absolute st
( Q <> R & Q,P,R are_collinear )
proof end;

theorem Th17: :: BKMODEL2:25
for P being Element of BK_model
for u being non zero Element of (TOP-REAL 3) st P = Dir u & u . 3 = 1 holds
((u . 1) ^2) + ((u . 2) ^2) < 1
proof end;

theorem Th18: :: BKMODEL2:26
for P1, P2 being Element of absolute
for Q being Element of BK_model
for u, v, w being non zero Element of (TOP-REAL 3) st Dir u = P1 & Dir v = P2 & Dir w = Q & u . 3 = 1 & v . 3 = 1 & w . 3 = 1 & v . 1 = - (u . 1) & v . 2 = - (u . 2) & P1,Q,P2 are_collinear holds
ex a being Real st
( - 1 < a & a < 1 & w . 1 = a * (u . 1) & w . 2 = a * (u . 2) )
proof end;

definition
let P be Element of absolute ;
func pole_infty P -> Element of real_projective_plane means :Def03: :: BKMODEL2:def 4
 ex u being non zero Element of (TOP-REAL 3) st
( P = Dir u & u . 3 = 1 & ((u . 1) ^2) + ((u . 2) ^2) = 1 & it = Dir |[(- (u . 2)),(u . 1),0]| );
existence
ex b1 being Element of real_projective_plane ex u being non zero Element of (TOP-REAL 3) st
( P = Dir u & u . 3 = 1 & ((u . 1) ^2) + ((u . 2) ^2) = 1 & b1 = Dir |[(- (u . 2)),(u . 1),0]| )
proof end;
uniqueness
for b1, b2 being Element of real_projective_plane st ex u being non zero Element of (TOP-REAL 3) st
( P = Dir u & u . 3 = 1 & ((u . 1) ^2) + ((u . 2) ^2) = 1 & b1 = Dir |[(- (u . 2)),(u . 1),0]| ) & ex u being non zero Element of (TOP-REAL 3) st
( P = Dir u & u . 3 = 1 & ((u . 1) ^2) + ((u . 2) ^2) = 1 & b2 = Dir |[(- (u . 2)),(u . 1),0]| ) holds
b1 = b2
proof end;
end;

:: deftheorem Def03 defines pole_infty BKMODEL2:def 4 :
for P being Element of absolute
for b2 being Element of real_projective_plane holds
( b2 = pole_infty P iff ex u being non zero Element of (TOP-REAL 3) st
( P = Dir u & u . 3 = 1 & ((u . 1) ^2) + ((u . 2) ^2) = 1 & b2 = Dir |[(- (u . 2)),(u . 1),0]| ) );

theorem Th19: :: BKMODEL2:27
for P being Element of absolute holds P <> pole_infty P
proof end;

theorem Th20: :: BKMODEL2:28
for P1, P2 being Element of absolute holds
( not pole_infty P1 = pole_infty P2 or P1 = P2 or ex u being non zero Element of (TOP-REAL 3) st
( P1 = Dir u & P2 = Dir |[(- (u `1)),(- (u `2)),1]| & u `3 = 1 ) )
proof end;

definition
let P be Element of absolute ;
func tangent P -> LINE of real_projective_plane means :Def04: :: BKMODEL2:def 5
 ex p being Element of real_projective_plane st
( p = P & it = Line (p,(pole_infty P)) );
existence
ex b1 being LINE of real_projective_plane ex p being Element of real_projective_plane st
( p = P & b1 = Line (p,(pole_infty P)) )
proof end;
uniqueness
for b1, b2 being LINE of real_projective_plane st ex p being Element of real_projective_plane st
( p = P & b1 = Line (p,(pole_infty P)) ) & ex p being Element of real_projective_plane st
( p = P & b2 = Line (p,(pole_infty P)) ) holds
b1 = b2 ;
end;

:: deftheorem Def04 defines tangent BKMODEL2:def 5 :
for P being Element of absolute
for b2 being LINE of real_projective_plane holds
( b2 = tangent P iff ex p being Element of real_projective_plane st
( p = P & b2 = Line (p,(pole_infty P)) ) );

theorem Th21: :: BKMODEL2:29
for P being Element of absolute holds P in tangent P
proof end;

theorem Th22: :: BKMODEL2:30
for P being Element of absolute holds (tangent P) /\ absolute = {P}
proof end;

theorem Th23: :: BKMODEL2:31
for P1, P2 being Element of absolute st tangent P1 = tangent P2 holds
P1 = P2
proof end;

theorem Th24: :: BKMODEL2:32
for P, Q being Element of absolute ex R being Element of real_projective_plane st
( R in tangent P & R in tangent Q )
proof end;

theorem Th25: :: BKMODEL2:33
for P1, P2 being Element of absolute st P1 <> P2 holds
ex P being Element of real_projective_plane st (tangent P1) /\ (tangent P2) = {P}
proof end;

theorem Th26: :: BKMODEL2:34
for M being Matrix of 3,REAL
for P being Element of absolute
for Q being Element of real_projective_plane
for u, v being non zero Element of (TOP-REAL 3)
for fp, fq being FinSequence of REAL st M = symmetric_3 (1,1,(- 1),0,0,0) & P = Dir u & Q = Dir v & u = fp & v = fq & Q in tangent P holds
SumAll (QuadraticForm (fq,M,fp)) = 0
proof end;

theorem Th27: :: BKMODEL2:35
for P, Q, R being Element of absolute
for P1, P2, P3, P4 being Point of real_projective_plane st P,Q,R are_mutually_distinct & P1 = P & P2 = Q & P3 = R & P4 in tangent P & P4 in tangent Q holds
( not P1,P2,P3 are_collinear & not P1,P2,P4 are_collinear & not P1,P3,P4 are_collinear & not P2,P3,P4 are_collinear )
proof end;

theorem :: BKMODEL2:36
for P, Q being Element of absolute
for R being Element of real_projective_plane
for u, v, w being non zero Element of (TOP-REAL 3) st P = Dir u & Q = Dir v & R = Dir w & R in tangent P & R in tangent Q & u . 3 = 1 & v . 3 = 1 & w . 3 = 0 & not P = Q holds
( u . 1 = - (v . 1) & u . 2 = - (v . 2) )
proof end;

theorem Th28: :: BKMODEL2:37
for P being Element of absolute
for R being Element of real_projective_plane
for u being non zero Element of (TOP-REAL 3) st R in tangent P & R = Dir u & u . 3 = 0 holds
R = pole_infty P
proof end;

theorem Th29: :: BKMODEL2:38
for a being non zero Real
for N being invertible Matrix of 3,F_Real st N = symmetric_3 (a,a,(- a),0,0,0) holds
(homography N) .: absolute = absolute
proof end;

theorem :: BKMODEL2:39
for ra being non zero Element of F_Real
for M, O being invertible Matrix of 3,F_Real st O = symmetric_3 (1,1,(- 1),0,0,0) & M = ra * O holds
(homography M) .: absolute = absolute
proof end;

theorem Th30: :: BKMODEL2:40
for P being Element of absolute holds tangent P misses BK_model
proof end;

theorem Th31: :: BKMODEL2:41
for P, PP1, PP2 being Element of real_projective_plane
for P1, P2 being Element of absolute
for Q being Element of real_projective_plane st P1 <> P2 & PP1 = P1 & PP2 = P2 & P in BK_model & P,PP1,PP2 are_collinear & Q in tangent P1 & Q in tangent P2 holds
ex R being Element of real_projective_plane st
( R in absolute & P,Q,R are_collinear )
proof end;

theorem Th32: :: BKMODEL2:42
for P, R, S being Element of real_projective_plane
for Q being Element of absolute st P in BK_model & R in tangent Q & P,S,R are_collinear & R <> S holds
Q <> S
proof end;

definition
let h be Element of EnsHomography3 ;
pred h is_K-isometry means :: BKMODEL2:def 6
 ex N being invertible Matrix of 3,F_Real st
( h = homography N & (homography N) .: absolute = absolute );
end;

:: deftheorem defines is_K-isometry BKMODEL2:def 6 :
for h being Element of EnsHomography3 holds
( h is_K-isometry iff ex N being invertible Matrix of 3,F_Real st
( h = homography N & (homography N) .: absolute = absolute ) );

theorem Th33: :: BKMODEL2:43
for h being Element of EnsHomography3 st h = homography (1. (F_Real,3)) holds
h is_K-isometry
proof end;

definition
func EnsK-isometry -> non empty Subset of EnsHomography3 equals :: BKMODEL2:def 7
 { h where h is Element of EnsHomography3 : h is_K-isometry } ;
coherence
{ h where h is Element of EnsHomography3 : h is_K-isometry } is non empty Subset of EnsHomography3
proof end;
end;

:: deftheorem defines EnsK-isometry BKMODEL2:def 7 :
EnsK-isometry = { h where h is Element of EnsHomography3 : h is_K-isometry } ;

definition
func SubGroupK-isometry -> strict Subgroup of GroupHomography3 means :Def05: :: BKMODEL2:def 8
 the carrier of it = EnsK-isometry ;
existence
ex b1 being strict Subgroup of GroupHomography3 st the carrier of b1 = EnsK-isometry
proof end;
uniqueness
for b1, b2 being strict Subgroup of GroupHomography3 st the carrier of b1 = EnsK-isometry & the carrier of b2 = EnsK-isometry holds
b1 = b2
proof end;
end;

:: deftheorem Def05 defines SubGroupK-isometry BKMODEL2:def 8 :
for b1 being strict Subgroup of GroupHomography3 holds
( b1 = SubGroupK-isometry iff the carrier of b1 = EnsK-isometry );

theorem :: BKMODEL2:44
for h being Element of EnsK-isometry
for N being invertible Matrix of 3,F_Real st h = homography N holds
(homography N) .: absolute = absolute
proof end;

theorem Th34: :: BKMODEL2:45
( homography (1. (F_Real,3)) = 1_ GroupHomography3 & homography (1. (F_Real,3)) = 1_ SubGroupK-isometry )
proof end;

theorem Th35: :: BKMODEL2:46
for N1, N2 being invertible Matrix of 3,F_Real
for h1, h2 being Element of SubGroupK-isometry st h1 = homography N1 & h2 = homography N2 holds
( h1 * h2 is Element of SubGroupK-isometry & h1 * h2 = homography (N1 * N2) )
proof end;

theorem Th36: :: BKMODEL2:47
for N being invertible Matrix of 3,F_Real
for h being Element of SubGroupK-isometry st h = homography N holds
( h " = homography (N ~) & homography (N ~) is Element of SubGroupK-isometry )
proof end;

theorem Th37: :: BKMODEL2:48
for s being Element of (ProjectiveSpace (TOP-REAL 3))
for p, q, r being Element of absolute st p,q,r are_mutually_distinct & s in (tangent p) /\ (tangent q) holds
ex N being invertible Matrix of 3,F_Real st
( (homography N) .: absolute = absolute & (homography N) . Dir101 = p & (homography N) . Dirm101 = q & (homography N) . Dir011 = r & (homography N) . Dir010 = s )
proof end;

theorem Th38: :: BKMODEL2:49
for p1, q1, r1, p2, q2, r2 being Element of absolute
for s1, s2 being Element of real_projective_plane st p1,q1,r1 are_mutually_distinct & p2,q2,r2 are_mutually_distinct & s1 in (tangent p1) /\ (tangent q1) & s2 in (tangent p2) /\ (tangent q2) holds
ex N being invertible Matrix of 3,F_Real st
( (homography N) .: absolute = absolute & (homography N) . p1 = p2 & (homography N) . q1 = q2 & (homography N) . r1 = r2 & (homography N) . s1 = s2 )
proof end;

theorem :: BKMODEL2:50
for p1, q1, r1, p2, q2, r2 being Element of absolute st p1,q1,r1 are_mutually_distinct & p2,q2,r2 are_mutually_distinct holds
ex N being invertible Matrix of 3,F_Real st
( (homography N) .: absolute = absolute & (homography N) . p1 = p2 & (homography N) . q1 = q2 & (homography N) . r1 = r2 )
proof end;

theorem Th39: :: BKMODEL2:51
for CLSP being CollSp
for p, q, r, s being Element of CLSP st Line (p,q) = Line (r,s) holds
r,s,p are_collinear by COLLSP:10, COLLSP:11;

theorem Th40: :: BKMODEL2:52
for CLSP being CollSp
for p, q being Element of CLSP holds Line (p,q) = Line (q,p)
proof end;

theorem Th41: :: BKMODEL2:53
for N being invertible Matrix of 3,F_Real
for p, q, r, s being Element of (ProjectiveSpace (TOP-REAL 3)) st Line (((homography N) . p),((homography N) . q)) = Line (((homography N) . r),((homography N) . s)) holds
( p,q,r are_collinear & p,q,s are_collinear & r,s,p are_collinear & r,s,q are_collinear )
proof end;

theorem Th42: :: BKMODEL2:54
for N being invertible Matrix of 3,F_Real
for p, q, r, s, t, u, np, nq, nr, ns being Element of real_projective_plane st p <> q & r <> s & np <> nq & nr <> ns & p,q,t are_collinear & r,s,t are_collinear & np = (homography N) . p & nq = (homography N) . q & nr = (homography N) . r & ns = (homography N) . s & np,nq,u are_collinear & nr,ns,u are_collinear & not u = (homography N) . t holds
Line (np,nq) = Line (nr,ns)
proof end;

theorem Th43: :: BKMODEL2:55
for N being invertible Matrix of 3,F_Real
for p, q, r, s, t, u, np, nq, nr, ns being Element of real_projective_plane st p <> q & r <> s & np <> nq & nr <> ns & p,q,t are_collinear & r,s,t are_collinear & np = (homography N) . p & nq = (homography N) . q & nr = (homography N) . r & ns = (homography N) . s & np,nq,u are_collinear & nr,ns,u are_collinear & not p,q,r are_collinear holds
u = (homography N) . t
proof end;

theorem :: BKMODEL2:56
for p, q being Element of absolute
for a, b being Element of BK_model ex N being invertible Matrix of 3,F_Real st
( (homography N) .: absolute = absolute & (homography N) . a = b & (homography N) . p = q )
proof end;

theorem :: BKMODEL2:57
for p, q, r, s being Element of absolute st p,q,r are_mutually_distinct & q,p,s are_mutually_distinct holds
ex N being invertible Matrix of 3,F_Real st
( (homography N) .: absolute = absolute & (homography N) . p = q & (homography N) . q = p & (homography N) . r = s & ( for t being Element of real_projective_plane st t in (tangent p) /\ (tangent q) holds
(homography N) . t = t ) )
proof end;

theorem Th44: :: BKMODEL2:58
for P, Q being Element of BK_model st P <> Q holds
ex P1, P2, P3, P4 being Element of absolute ex P5 being Element of (ProjectiveSpace (TOP-REAL 3)) st
( P1 <> P2 & P,Q,P1 are_collinear & P,Q,P2 are_collinear & P,P5,P3 are_collinear & Q,P5,P4 are_collinear & P1,P2,P3 are_mutually_distinct & P1,P2,P4 are_mutually_distinct & P5 in (tangent P1) /\ (tangent P2) )
proof end;

theorem Th45: :: BKMODEL2:59
for P, Q being Element of BK_model st P <> Q holds
ex N being invertible Matrix of 3,F_Real st
( (homography N) .: absolute = absolute & (homography N) . P = Q & (homography N) . Q = P & ex P1, P2 being Element of absolute st
( P1 <> P2 & P,Q,P1 are_collinear & P,Q,P2 are_collinear & (homography N) . P1 = P2 & (homography N) . P2 = P1 ) )
proof end;

theorem :: BKMODEL2:60
for P, Q being Element of BK_model ex h being Element of SubGroupK-isometry ex N being invertible Matrix of 3,F_Real st
( h = homography N & (homography N) . P = Q & (homography N) . Q = P )
proof end;

theorem :: BKMODEL2:61
for P, Q, R, S, T, U being Element of BK_model st ex h1, h2 being Element of SubGroupK-isometry ex N1, N2 being invertible Matrix of 3,F_Real st
( h1 = homography N1 & h2 = homography N2 & (homography N1) . P = R & (homography N1) . Q = S & (homography N2) . R = T & (homography N2) . S = U ) holds
ex h3 being Element of SubGroupK-isometry ex N3 being invertible Matrix of 3,F_Real st
( h3 = homography N3 & (homography N3) . P = T & (homography N3) . Q = U )
proof end;

theorem :: BKMODEL2:62
for P, Q, R being Element of BK_model
for h being Element of SubGroupK-isometry
for N being invertible Matrix of 3,F_Real st h = homography N & (homography N) . P = R & (homography N) . Q = R holds
P = Q by ANPROJ_9:16;