text:
:: Beltrami-Klein model, Part {IV}
::  by Roland Coghetto

environ

 vocabularies NAT_1, MATRIX_6, FINSEQ_2, COMPLEX1, REAL_1, XCMPLX_0, ANPROJ_1,
      PENCIL_1, MCART_1, EUCLID_5, ALGSTR_0, ARYTM_1, ARYTM_3, CARD_1, EUCLID,
      FUNCT_1, INCSP_1, MATRIX_1, NUMBERS, PRE_TOPC, RELAT_1, STRUCT_0,
      SUBSET_1, SUPINF_2, VECTSP_1, XBOOLE_0, MESFUNC1, ANPROJ_8, ANPROJ_9,
      TARSKI, XXREAL_0, PASCAL, SQUARE_1, JGRAPH_6, RVSUM_1, FINSEQ_1,
      MATRIX_3, BKMODEL1, BKMODEL2, BKMODEL3, RLTOPSP1, GTARSKI1, GTARSKI2,
      METRIC_1, EUCLID12, CONVEX1, XXREAL_1, ALGSTR_4, BKMODEL4;
 notations RELSET_1, ORDINAL1, XCMPLX_0, PRE_TOPC, RVSUM_1, TARSKI, XBOOLE_0,
      RLVECT_1, COLLSP, EUCLID_5, PASCAL, XXREAL_0, ANPROJ_9, SQUARE_1,
      XREAL_0, JGRAPH_6, SUBSET_1, NUMBERS, FUNCT_1, FUNCT_2, FINSEQ_1,
      STRUCT_0, ALGSTR_0, VECTSP_1, FINSEQ_2, EUCLID, ANPROJ_1, MATRIX_6,
      LAPLACE, ANPROJ_8, MATRIX_1, MATRIX_3, BKMODEL1, BKMODEL2, RLTOPSP1,
      GTARSKI1, METRIC_1, EUCLID12, XXREAL_1, GTARSKI2, BKMODEL3;
 constructors REALSET1, FINSEQ_4, LAPLACE, MATRPROB, RELSET_1, MONOID_0,
      EUCLID_5, MATRIX13, ANPROJ_8, PASCAL, SQUARE_1, BINOP_2, GTARSKI2,
      EUCLID12, CONVEX1, XXREAL_1, BKMODEL3;
 registrations MEMBERED, ORDINAL1, XXREAL_0, XBOOLE_0, ANPROJ_1, STRUCT_0,
      VECTSP_1, REVROT_1, RELSET_1, XREAL_0, MONOID_0, EUCLID, VALUED_0,
      MATRIX_6, SQUARE_1, XCMPLX_0, NUMBERS, TOPREAL9, TOPREALC, GTARSKI2,
      RLTOPSP1, CONVEX1, BKMODEL3;
 requirements REAL, SUBSET, NUMERALS, ARITHM, BOOLE;
 definitions TARSKI, GTARSKI1;
 equalities VECTSP_1, STRUCT_0, BKMODEL1, GTARSKI2, EUCLID, XCMPLX_0, BKMODEL3;
 expansions TARSKI, STRUCT_0, XBOOLE_0, GTARSKI1;
 theorems XREAL_0, LAPLACE, MATRIX_6, XREAL_1, EUCLID_5, ANPROJ_1, EUCLID,
      XCMPLX_1, RVSUM_1, FINSEQ_1, FUNCT_1, FUNCT_2, ANPROJ_8, ANPROJ_9,
      PASCAL, TARSKI, XBOOLE_0, SQUARE_1, TOPREAL9, EUCLID_2, FINSEQ_2,
      BKMODEL1, BKMODEL2, GTARSKI1, GTARSKI2, RLTOPSP1, CONVEX1, XXREAL_1,
      MATRIX_9, EUCLID12, GTARSKI3, BKMODEL3;

begin :: Preliminaries

theorem Th25:
  for a,b being Real st a <> b holds 1 - (a / (a - b)) = - b / (a - b)
  proof
    let a,b be Real;
    assume a <> b;
    then a - b <> 0;
    then 1 - (a / (a - b)) = (a - b) / (a - b) - a / (a - b) by XCMPLX_1:60
                          .= (a - b - a) / (a - b);
    hence thesis;
  end;

theorem
  for a,b being Real st 0 < a * b holds 0 < a / b
  proof
    let a,b be Real;
    assume
A1: 0 < a * b; then
A2: b <> 0; then
    0 < b^2 by SQUARE_1:12;
    then 0 / b^2 < (a * b) / b^2 by A1;
    then 0 < (a * b) / (b * b) by SQUARE_1:def 1;
    then 0 < (a / b) * (b / b) by XCMPLX_1:76;
    then 0 < (a / b) * 1 by A2,XCMPLX_1:60;
    hence thesis;
  end;

theorem Th31:
  for a,b,c being Real st 0 <= a <= 1 & 0 < b * c holds
  0 <= (a * c) / ((1 - a) * b + a * c) <= 1
  proof
    let a,b,c be Real;
    assume that
A1: 0 <= a <= 1 and
A2: 0 < b * c;
    per cases by A2,XREAL_1:134;
    suppose
A3:   0 < b & 0 < c;
B3:   a - a <= 1 - a by A1,XREAL_1:9;
      hence 0 <= (a * c) / ((1 - a) * b + a * c) by A1,A3;
      0 + a * c <= (1 - a) * b + a * c by A3,B3,XREAL_1:6;
      hence (a * c) / ((1 - a) * b + a * c) <= 1 by A1,A3,XREAL_1:183;
    end;
    suppose
A4:   b < 0 & c < 0;
A5:   a - a <= 1 - a by A1,XREAL_1:9;
      hence 0 <= (a * c) / ((1 - a) * b + a * c) by A1,A4;
      (1 - a) * b + a * c <= 0 + a * c by A4,A5,XREAL_1:6;
      hence (a * c) / ((1 - a) * b + a * c) <= 1 by A1,A4,XREAL_1:184;
    end;
  end;

theorem Th32:
  for a,b,c being Real st (1 - a) * b + a * c <> 0 holds
    1 - ((a * c) / ((1 - a) * b + a * c)) =
      (1 - a) * b / ((1 - a) * b + a * c)
  proof
    let a,b,c be Real;
    set r = (1 - a) * b + a * c;
    assume (1 - a) * b + a * c <> 0; then
    1 - (a * c) / r = r / r - (a * c) / r by XCMPLX_1:60
                   .= (1 - a) * b / r;
    hence thesis;
  end;

theorem Th33:
  for a,b,c,d being Real st b <> 0 holds
    a * b / c * d / b = a * d / c
  proof
    let a,b,c,d be Real;
    assume
A1: b <> 0;
    a * b / c * d / b = a * ((d / c) * (b / b))
                     .= a * ((d / c) * 1) by A1,XCMPLX_1:60;
    hence thesis;
  end;

theorem Th35:
  for u being Element of TOP-REAL 3 holds u = |[u.1,u.2,u.3]|
  proof
    let u be Element of TOP-REAL 3;
    thus u = |[u`1,u`2,u`3]| by EUCLID_5:3
          .= |[u.1,u`2,u`3]| by EUCLID_5:def 1
          .= |[u.1,u.2,u`3]| by EUCLID_5:def 2
          .= |[u.1,u.2,u.3]| by EUCLID_5:def 3;
  end;

theorem Th01:
  for P being Element of BK_model holds BK_to_REAL2 P in TarskiEuclid2Space
  proof
    let P be Element of BK_model;
    the MetrStruct of TarskiEuclid2Space = the MetrStruct of Euclid 2 &
    BK_to_REAL2 P in TOP-REAL 2 by GTARSKI1:def 13;
    hence thesis by EUCLID:22;
  end;

definition
  let P be POINT of BK-model-Plane;
  func BK_to_T2 P -> POINT of TarskiEuclid2Space means :Def01:
  ex p be Element of BK_model st P = p &
  it = BK_to_REAL2 p;
  existence
  proof
    reconsider p = P as Element of BK_model;
    BK_to_REAL2 p in TarskiEuclid2Space by Th01;
    hence thesis;
  end;
  uniqueness;
end;

definition
  let P be POINT of TarskiEuclid2Space;
  assume
A1: Tn2TR P in inside_of_circle(0,0,1);
  func T2_to_BK P -> POINT of BK-model-Plane means
:Def02:
  ex u be non zero Element of TOP-REAL 3 st
  it = Dir u & u`3 = 1 & Tn2TR P = |[u`1,u`2]|;
  existence
  proof
    reconsider p = Tn2TR P as Element of inside_of_circle(0,0,1) by A1;
    reconsider Q = REAL2_to_BK p as Element of BK_model;
    consider P2 be Element of TOP-REAL 2 such that
A2: P2 = p and
A3: REAL2_to_BK p = Dir |[P2`1,P2`2,1]| by BKMODEL2:def 3;
    reconsider u = |[P2`1,P2`2,1]| as non zero Element of TOP-REAL 3;
    now
      thus Q = Dir u by A3;
      |[u`1,u`2,u`3]| = |[P2`1,P2`2,1]| by EUCLID_5:3;
      then
A4:   u`1 = P2`1 & u`2 = P2`2 & u`3 = 1 by FINSEQ_1:78;
      thus u`3 = 1 by EUCLID_5:2;
      thus p = |[u`1,u`2]| by A2,A4,EUCLID:53;
    end;
    hence thesis;
  end;
  uniqueness
  proof
    let P1,P2 be POINT of BK-model-Plane such that
A5: ex u be non zero Element of TOP-REAL 3 st
    P1 = Dir u & u`3 = 1 & Tn2TR P = |[u`1,u`2]| and
A6: ex v be non zero Element of TOP-REAL 3 st
    P2 = Dir v & v`3 = 1 & Tn2TR P = |[v`1,v`2]|;
    consider u be non zero Element of TOP-REAL 3 such that
A7: P1 = Dir u and
A8: u`3 = 1 and
A9: Tn2TR P = |[u`1,u`2]| by A5;
    consider v be non zero Element of TOP-REAL 3 such that
A10: P2 = Dir v and
A11: v`3 = 1 and
A12: Tn2TR P = |[v`1,v`2]| by A6;
A13: u`1 = v`1 & u`2 = v`2 by A9,A12,FINSEQ_1:77;
    u = |[v`1,v`2,v`3]| by A13,A8,A11,EUCLID_5:3
     .= v by EUCLID_5:3;
    hence thesis by A7,A10;
  end;
end;

theorem Th02:
  for P being POINT of BK-model-Plane holds
  Tn2TR BK_to_T2 P in inside_of_circle(0,0,1)
  proof
    let P be POINT of BK-model-Plane;
    consider p be Element of BK_model such that
    P = p and
A1: BK_to_T2 P = BK_to_REAL2 p by Def01;
    reconsider Q = BK_to_T2 P as POINT of TarskiEuclid2Space;
    thus thesis by A1;
  end;

theorem
  for P being POINT of BK-model-Plane holds T2_to_BK BK_to_T2 P = P
  proof
    let P be POINT of BK-model-Plane;
    consider p be Element of BK_model such that
A1: P = p and
A2: BK_to_T2 P = BK_to_REAL2 p by Def01;
    consider u be non zero Element of TOP-REAL 3 such that
A3: Dir u = p and
A4: u.3 = 1 and
A5: BK_to_REAL2 p = |[u.1,u.2]| by BKMODEL2:def 2;
    reconsider Q = BK_to_T2 P as POINT of TarskiEuclid2Space;
    consider v be non zero Element of TOP-REAL 3 such that
A6: T2_to_BK Q = Dir v and
A7: v`3 = 1 and
A8: Tn2TR Q = |[v`1,v`2]| by A2,Def02;
    u.1 = v`1 & u.2 = v`2 by A8,A5,A2,FINSEQ_1:77; then
A9: u`1 = v`1 & u`2 = v`2 by EUCLID_5:def 1,def 2;
    u = |[u`1,u`2,u`3]| by EUCLID_5:3
     .= |[v`1,v`2,v`3]| by A4,A7,A9,EUCLID_5:def 3
     .= v by EUCLID_5:3;
    hence thesis by A1,A6,A3;
  end;

theorem Th03:
  for P being POINT of TarskiEuclid2Space st
  Tn2TR P is Element of inside_of_circle(0,0,1) holds BK_to_T2 T2_to_BK P = P
  proof
    let P be POINT of TarskiEuclid2Space;
    assume Tn2TR P is Element of inside_of_circle(0,0,1);
    then consider u be non zero Element of TOP-REAL 3 such that
A1: T2_to_BK P = Dir u and
A2: u`3 = 1 and
A3: Tn2TR P = |[u`1,u`2]| by Def02;
    reconsider Q9 = T2_to_BK P as Element of BK-model-Plane;
    reconsider Q = T2_to_BK P as Element of BK_model;
    consider p be Element of BK_model such that
A4: Q9 = p and
A5: BK_to_T2 Q9 = BK_to_REAL2 p by Def01;
    consider v be non zero Element of TOP-REAL 3 such that
A6: Dir v = p and
A7: v.3 = 1 and
A8: BK_to_REAL2 p = |[v.1,v.2]| by BKMODEL2:def 2;
    are_Prop u,v by A4,A6,A1,ANPROJ_1:22;
    then consider a be Real such that a <> 0 and
A9: u = a * v by ANPROJ_1:1;
A10: 1 = a * v`3 by A2,A9,EUCLID_5:9
     .= a * 1 by A7,EUCLID_5:def 3
     .= a;
    |[u`1,u`2,u`3]| = u by EUCLID_5:3
                   .= |[1 * v`1,1 * v`2,1 * v`3]| by A9,A10,EUCLID_5:7;
    then u`1 = v`1 & u`2 = v`2 by FINSEQ_1:78;
    then u`1 = v.1 & u`2 = v.2 by EUCLID_5:def 1,def 2;
    hence thesis by A5,A8,A3;
  end;

theorem Th04:
  for P being Point of BK-model-Plane
  for p being Element of BK_model st P = p holds
  BK_to_T2 P = BK_to_REAL2 p & Tn2TR BK_to_T2 P = BK_to_REAL2 p
  proof
    let P be Point of BK-model-Plane;
    let p be Element of BK_model;
    assume
A1: P = p;
    ex p be Element of BK_model st P = p &
    BK_to_T2 P = BK_to_REAL2 p by Def01;
    hence thesis by A1;
  end;

theorem Th05:
  for P,Q,R being Point of BK-model-Plane
  for P2,Q2,R2 being POINT of TarskiEuclid2Space st
  P2 = BK_to_T2 P & Q2 = BK_to_T2 Q & R2 = BK_to_T2 R
  holds between P,Q,R iff between P2,Q2,R2
  proof
    let P,Q,R be Point of BK-model-Plane;
    let P2,Q2,R2 be POINT of TarskiEuclid2Space;
    assume that
A1: P2 = BK_to_T2 P and
A2: Q2 = BK_to_T2 Q and
A3: R2 = BK_to_T2 R;
    reconsider p = P,q = Q, r = R as Element of BK_model;
A4: Tn2TR BK_to_T2 P = BK_to_REAL2 p &
      Tn2TR BK_to_T2 Q = BK_to_REAL2 q &
      Tn2TR BK_to_T2 R = BK_to_REAL2 r by Th04;
    hereby
      assume between P,Q,R;
      then BK_to_REAL2 q in LSeg(BK_to_REAL2 p,BK_to_REAL2 r)
        by BKMODEL3:def 7;
      hence between P2,Q2,R2 by A4,A1,A2,A3,GTARSKI2:20;
    end;
    assume between P2,Q2,R2;
    then Tn2TR BK_to_T2 Q in LSeg(Tn2TR BK_to_T2 P,Tn2TR BK_to_T2 R)
      by A1,A2,A3,GTARSKI2:20;
    hence between P,Q,R by A4,BKMODEL3:def 7;
  end;

theorem Th06:
  for P,Q being Element of TOP-REAL 2 st P <> Q holds
  P.1 <> Q.1 or P.2 <> Q.2
  proof
    let P,Q be Element of TOP-REAL 2;
    assume
A1: P <> Q;
    assume P.1 = Q.1 & P.2 = Q.2;
    then P`1 = Q`1 & P`2 = Q`2;
    then P = |[Q`1,Q`2]| by EUCLID:53
          .= Q by EUCLID:53;
    hence contradiction by A1;
  end;

theorem Th07:
  for a,b being Real
  for P,Q being Element of TOP-REAL 2 st P <> Q &
  (1 - a) * P + a * Q = (1 - b) * P + b * Q holds
  a = b
  proof
    let a,b be Real;
    let P,Q be Element of TOP-REAL 2;
    assume that
A1: P <> Q and
A2: (1 - a) * P + a * Q = (1 - b) * P + b * Q;
    reconsider PR2 = P, QR2= Q as Element of REAL 2 by EUCLID:22;
    reconsider R2 = (1-a)*PR2+a*QR2 as Element of TOP-REAL 2 by EUCLID:22;
    per cases by A1,Th06;
    suppose P.1 <> Q.1;
      then
A3:   QR2.1 - PR2.1 <> 0;
      0 = R2.1 - R2.1
       .= (R2 - R2).1 by RVSUM_1:27
       .= ((b - a) * (QR2 - PR2)).1 by A2,EUCLID12:1
       .= (b - a) * (QR2 - PR2).1 by RVSUM_1:44
       .= (b - a) * (QR2.1 - PR2.1) by RVSUM_1:27;
      then (b - a) = 0 by A3;
      hence thesis;
    end;
    suppose P.2 <> Q.2; then
A4:   QR2.2 - PR2.2 <> 0;
      0 = R2.2 - R2.2
       .= (R2 - R2).2 by RVSUM_1:27
       .= ((b - a) * (QR2 - PR2)).2 by A2,EUCLID12:1
       .= (b - a) * (QR2 - PR2).2 by RVSUM_1:44
       .= (b - a) * (QR2.2 - PR2.2) by RVSUM_1:27;
      then (b - a) = 0 by A4;
      hence thesis;
    end;
  end;

theorem Th08:
  for P,Q being Point of BK-model-Plane st Tn2TR BK_to_T2 P = Tn2TR BK_to_T2 Q
  holds P = Q
  proof
    let P,Q be Point of BK-model-Plane;
    assume
A1: Tn2TR BK_to_T2 P = Tn2TR BK_to_T2 Q;
    reconsider p = P,q = Q as Element of BK_model;
    Tn2TR BK_to_T2 P = BK_to_REAL2 p &
    Tn2TR BK_to_T2 Q = BK_to_REAL2 q by Th04;
    hence thesis by A1,BKMODEL2:4;
  end;

definition
  let P,Q,R be Point of BK-model-Plane;
  assume that
A1: between P,Q,R and
A2: P <> R;
  func length(P,Q,R) -> Real means
:Def03:
  0 <= it <= 1 &
  Tn2TR BK_to_T2 Q = (1 - it) * Tn2TR BK_to_T2 P + it * Tn2TR BK_to_T2 R;
  existence
  proof
    reconsider P2 = BK_to_T2 P,Q2 = BK_to_T2 Q,R2 = BK_to_T2 R as
      Point of TarskiEuclid2Space;
    reconsider p = P,q = Q,r = R as Element of BK_model;
    BK_to_T2 P = BK_to_REAL2 p & Tn2TR BK_to_T2 P = BK_to_REAL2 p &
    BK_to_T2 Q = BK_to_REAL2 q & Tn2TR BK_to_T2 Q = BK_to_REAL2 q &
    BK_to_T2 R = BK_to_REAL2 r & Tn2TR BK_to_T2 R = BK_to_REAL2 r by Th04;
    then Tn2TR BK_to_T2 Q in LSeg(Tn2TR BK_to_T2 P,Tn2TR BK_to_T2 R)
      by A1,BKMODEL3:def 7;
    then consider r be Real such that
A3: 0 <= r and
A4: r <= 1 and
A5: Tn2TR BK_to_T2 Q = (1-r) * Tn2TR BK_to_T2 P + r * Tn2TR BK_to_T2 R
      by RLTOPSP1:76;
    take r;
    thus thesis by A3,A4,A5;
  end;
  uniqueness by A2,Th07,Th08;
end;

theorem Th09:
  for P,Q being Point of BK-model-Plane holds
  between P,P,Q & between P,Q,Q
  proof
    let P,Q be Point of BK-model-Plane;
    reconsider P2 = BK_to_T2 P,Q2 = BK_to_T2 Q as Point of TarskiEuclid2Space;
    between P2,P2,Q2 by GTARSKI1:17;
    hence between P,P,Q by Th05;
    between P2,Q2,Q2 by GTARSKI1:14;
    hence between P,Q,Q by Th05;
  end;

theorem
  for P,Q being Point of BK-model-Plane st P <> Q holds
  length(P,P,Q) = 0 & length(P,Q,Q) = 1
  proof
    let P,Q be Point of BK-model-Plane;
    assume
A1: P <> Q;
    reconsider P2 = BK_to_T2 P,Q2 = BK_to_T2 Q as Point of TarskiEuclid2Space;
A2: between P,P,Q by Th09;
A3: between P,Q,Q by Th09;
    reconsider r = 0 as Real;
    now
      thus 0 <= r <= 1;
      thus (1 - r ) * Tn2TR BK_to_T2 P + r * Tn2TR BK_to_T2 Q
        = |[ 1 * (Tn2TR BK_to_T2 P)`1, 1 * (Tn2TR BK_to_T2 P)`2 ]|
          + 0 * Tn2TR BK_to_T2 Q by EUCLID:57
       .= |[ (Tn2TR BK_to_T2 P)`1, (Tn2TR BK_to_T2 P)`2 ]|
          + |[ 0 * (Tn2TR BK_to_T2 Q)`1, 0 * (Tn2TR BK_to_T2 Q)`2 ]|
          by EUCLID:57
       .= |[ (Tn2TR BK_to_T2 P)`1 + 0 , (Tn2TR BK_to_T2 P)`2 + 0 ]|
          by EUCLID:56
       .= Tn2TR BK_to_T2 P by EUCLID:53;
    end;
    hence length(P,P,Q) = 0 by A1,A2,Def03;
    reconsider s = 1 as Real;
    now
      thus 0 <= s <= 1;
      thus (1 - s ) * Tn2TR BK_to_T2 P + s * Tn2TR BK_to_T2 Q
        = |[ 1 * (Tn2TR BK_to_T2 Q)`1, 1 * (Tn2TR BK_to_T2 Q)`2 ]|
          + 0 * Tn2TR BK_to_T2 P by EUCLID:57
       .= |[ (Tn2TR BK_to_T2 Q)`1, (Tn2TR BK_to_T2 Q)`2 ]|
          + |[ 0 * (Tn2TR BK_to_T2 P)`1, 0 * (Tn2TR BK_to_T2 P)`2 ]|
          by EUCLID:57
       .= |[ (Tn2TR BK_to_T2 Q)`1 + 0 , (Tn2TR BK_to_T2 Q)`2 + 0 ]|
          by EUCLID:56
       .= Tn2TR BK_to_T2 Q by EUCLID:53;
    end;
    hence length(P,Q,Q) = 1 by A1,A3,Def03;
  end;

theorem
  for N being Matrix of 3,F_Real st
  N = <* <* 2,   0,    -1 *>,
         <* 0, sqrt 3,  0 *>,
         <* 1,   0,    -2 *> *> holds
  Det N = (-3) * sqrt 3 & N is invertible
  proof
    let N be Matrix of 3,F_Real;
    assume
A1: N = <* <* 2,   0   ,-1 *>,
           <* 0, sqrt 3, 0 *>,
           <* 1,   0   ,-2 *> *>;
    reconsider a = 2,b = 0,c = -1,d = 0,e = sqrt 3,f = 0,g = 1,h = 0,i = -2
      as Element of F_Real by XREAL_0:def 1;
    Det N = a*e*i - c*e*g - a*f*h + b*f*g - b*d*i + c*d*h by A1,MATRIX_9:46;
    then Det N = (-3) * sqrt 3 & Det N <> 0.F_Real by SQUARE_1:24;
    hence thesis by LAPLACE:34;
  end;

theorem Th10:
  for a11,a12,a13,a21,a22,a23,a31,a32,a33,
      b11,b12,b13,b21,b22,b23,b31,b32,b33,
      ab11,ab12,ab13,ab21,ab22,ab23,ab31,ab32,ab33 being Element of F_Real
  for A,B being Matrix of 3,F_Real st
  A = <* <* a11,a12,a13 *>,
         <* a21,a22,a23 *>,
         <* a31,a32,a33 *> *> &
  B = <* <* b11,b12,b13 *>,
         <* b21,b22,b23 *>,
         <* b31,b32,b33 *> *> &
  ab11 = a11 * b11 + a12 * b21 + a13 * b31 &
  ab12 = a11 * b12 + a12 * b22 + a13 * b32 &
  ab13 = a11 * b13 + a12 * b23 + a13 * b33 &
  ab21 = a21 * b11 + a22 * b21 + a23 * b31 &
  ab22 = a21 * b12 + a22 * b22 + a23 * b32 &
  ab23 = a21 * b13 + a22 * b23 + a23 * b33 &
  ab31 = a31 * b11 + a32 * b21 + a33 * b31 &
  ab32 = a31 * b12 + a32 * b22 + a33 * b32 &
  ab33 = a31 * b13 + a32 * b23 + a33 * b33 holds
  A * B = <* <* ab11, ab12, ab13 *>,
             <* ab21, ab22, ab23 *>,
             <* ab31, ab32, ab33 *> *> by ANPROJ_9:6;

theorem Th11:
  for N1,N2 being Matrix of 3,F_Real st
  N1 = <* <* 2,    0,   -1 *>,
          <* 0, sqrt 3,  0 *>,
          <* 1,    0,   -2 *> *> &
  N2 = <* <* 2/3,   0,     -1/3  *>,
          <* 0,  1/sqrt 3,  0   *>,
          <* 1/3,   0,     -2/3 *> *> holds
  N1 * N2 = <* <* 1,0,0 *>,
               <* 0,1,0 *>,
               <* 0,0,1 *> *>
  proof
    let N1,N2 be Matrix of 3,F_Real;
    assume that
A1: N1 = <* <* 2,   0,   -1 *>,
            <* 0, sqrt 3, 0 *>,
            <* 1,   0,   -2 *> *> and
A2: N2 = <* <* 2/3,     0,   -1/3 *>,
            <* 0,  1/sqrt 3,   0  *>,
            <* 1/3,     0,   -2/3 *> *>;
    reconsider a = 2,b = 0,c = -1,d = 0, e = sqrt 3,f = 0,g = 1,h=0,i = -2,
      a9 = 2/3,b9=0,c9 = - 1/3,d9=0,e9 = 1/sqrt 3,f9=0,g9 = 1/3,h9=0,i9 = -2/3
    as Element of F_Real by XREAL_0:def 1;
    reconsider n11 = a*a9+b*d9+c*g9, n12 = a*b9+b*e9+c*h9,
      n13 = a*c9+b*f9+c*i9, n21 = d*a9+e*d9+f*g9,
      n22 = d*b9+e*e9+f*h9, n23 = d*c9+e*f9+f*i9,
      n31 = g*a9+h*d9+i*g9, n32 = g*b9+h*e9+i*h9,
      n33 = g*c9+h*f9+i*i9 as Element of F_Real;
    n11 = 1 & n12 = 0 & n13 = 0 & n21 = 0 &
      n22 = 1 & n23 = 0 & n31 = 0 & n32 = 0 & n33 = 1
      by SQUARE_1:24,XCMPLX_1:106;
    hence thesis by A1,A2,Th10;
  end;

theorem Th12:
  for N1,N2 being Matrix of 3,F_Real st
  N2 = <* <* 2,   0,   -1 *>,
          <* 0, sqrt 3, 0 *>,
          <* 1,   0,   -2 *> *> &
  N1 = <* <* 2/3,   0,     -1/3 *>,
          <* 0,  1/sqrt 3,   0  *>,
          <* 1/3,   0,     -2/3 *> *> holds
  N1 * N2 = <* <* 1,0,0 *>,
               <* 0,1,0 *>,
               <* 0,0,1 *> *>
  proof
    let N1,N2 be Matrix of 3,F_Real;
    assume that
A1: N2 = <* <* 2,   0,    -1 *>,
            <* 0, sqrt 3, 0  *>,
            <* 1,   0,    -2 *> *> and
A2: N1 = <* <* 2/3,    0,     -1/3 *>,
            <* 0,   1/sqrt 3, 0    *>,
            <* 1/3,    0,     -2/3 *> *>;
    reconsider a9 = 2,b9 = 0,c9 = -1,d9 = 0, e9 = sqrt 3,f9 = 0,g9 = 1,h9=0,
      i9 = -2,a = 2/3,b=0,c = - 1/3,d=0,e = 1/sqrt 3,f=0,g = 1/3,h=0,i = -2/3
    as Element of F_Real by XREAL_0:def 1;
    reconsider n11 = a*a9+b*d9+c*g9, n12 = a*b9+b*e9+c*h9,
    n13 = a*c9+b*f9+c*i9, n21 = d*a9+e*d9+f*g9,
    n22 = d*b9+e*e9+f*h9, n23 = d*c9+e*f9+f*i9,
    n31 = g*a9+h*d9+i*g9,n32 = g*b9+h*e9+i*h9,n33 = g*c9+h*f9+i*i9
      as Element of F_Real;
    n11 = 1 & n12 = 0 & n13 = 0 & n21 = 0 &
      n22 = 1 & n23 = 0 & n31 = 0 & n32 = 0 & n33 = 1
      by SQUARE_1:24,XCMPLX_1:106;
    hence thesis by A1,A2,Th10;
  end;

theorem Th13:
  for N1,N2 being Matrix of 3,F_Real st
  N1 = <* <* 2,   0,   -1 *>,
          <* 0, sqrt 3, 0 *>,
          <* 1,   0,   -2 *> *> &
  N2 = <* <* 2/3,     0,     -1/3 *>,
          <* 0,    1/sqrt 3,    0 *>,
          <* 1/3,     0,     -2/3 *> *>
  holds N1 is_reverse_of N2
  proof
    let N1,N2 be Matrix of 3,F_Real;
    assume
A1: N1 = <* <* 2,   0,    -1 *>,
            <* 0, sqrt 3,  0 *>,
            <* 1,   0,    -2 *> *> &
    N2 = <* <* 2/3,   0,      -1/3 *>,
            <* 0,   1/sqrt 3,    0 *>,
            <* 1/3,   0,      -2/3 *> *>;
    N2 * N1 = 1.(F_Real,3) & N1 * N2 = 1.(F_Real,3) by A1,Th11,Th12,ANPROJ_9:1;
    hence thesis by MATRIX_6:def 2;
  end;

theorem Th14:
  for N being invertible Matrix of 3,F_Real st
  N = <* <* 2/3,   0   ,-1/3 *>,
         <* 0, 1/sqrt 3, 0   *>,
         <* 1/3,   0   ,-2/3 *> *> holds
  homography(N).:absolute c= absolute
  proof
    let N be invertible Matrix of 3,F_Real;
    assume
A1: N = <* <* 2/3,   0   ,-1/3 *>,
           <* 0, 1/sqrt 3, 0   *>,
           <* 1/3,   0   ,-2/3 *> *>;
    reconsider a=2/3,b=0,c = -1/3,d=0,e=1/sqrt 3,f=0,g=1/3,h=0,i=-2/3
      as Element of F_Real by XREAL_0:def 1;
    homography(N).:absolute c= absolute
    proof
      let x be object;
      assume x in homography(N).:absolute;
      then consider y be object such that
A2:   y in dom homography(N) and
A3:   y in absolute and
A4:   x = homography(N).y by FUNCT_1:def 6;
      reconsider y as Point of ProjectiveSpace TOP-REAL 3 by A2;
      consider yu be non zero Element of TOP-REAL 3 such that
A5:   (yu.1)^2 + (yu.2)^2 = 1 and
A6:   yu.3 = 1 and
A7:   y = Dir yu by A3,BKMODEL1:89;
A8:   yu`1 * yu`1 + yu`2 * yu`2 = yu.1 * yu`1 + yu`2 * yu`2
                                   by EUCLID_5:def 1
                               .= yu.1 * yu.1 + yu`2 * yu`2 by EUCLID_5:def 1
                               .= yu.1 * yu.1 + yu.2 * yu`2 by EUCLID_5:def 2
                               .= yu.1 * yu.1 + yu.2 * yu.2 by EUCLID_5:def 2
                               .= (yu.1)^2 + yu.2 * yu.2 by SQUARE_1:def 1
                               .= 1 by A5,SQUARE_1:def 1;
A9:   yu`3 * yu`3 = yu.3 * yu`3 by EUCLID_5:def 3
                 .= 1 by A6,EUCLID_5:def 3;
      consider u,v be Element of TOP-REAL 3,
                uf be FinSequence of F_Real,
                p be FinSequence of 1-tuples_on REAL such that
A10:  y = Dir u & u is not zero & u = uf & p = N * uf & v = M2F p &
        v is not zero & homography(N).y = Dir v by ANPROJ_8:def 4;
      are_Prop u,yu by A7,A10,ANPROJ_1:22;
      then consider l be Real such that l <> 0 and
A11:  u = l * yu by ANPROJ_1:1;
      reconsider u1 = l * yu`1,u2 = l * yu`2,u3 = l * yu`3 as Element of F_Real
        by XREAL_0:def 1;
      uf = <* u1,u2,u3 *> by A11,A10,EUCLID_5:7;
      then
      v = <* a*u1+b*u2+c*u3,d*u1+e*u2+f*u3,g*u1+h*u2+i*u3 *> by A1,A10,PASCAL:8
       .= <* (2/3) * u1 - (1/3) * u3, (1/sqrt 3) * u2,
             (1/3) * u1 - (2/3) * u3 *>;
       then v`1 = (2/3) * u1 - (1/3) * u3 & v`2 = (1 / sqrt 3) * u2 &
       v`3 = (1/3) * u1 - (2/3) * u3 by EUCLID_5:2;
       then
A12:   v.1 = (2/3) * u1 - (1/3) * u3 & v.2 = (1/sqrt 3) * u2 &
         v.3 = (1/3) * u1 - (2/3) * u3 by EUCLID_5:def 1,def 2,def 3;
       set k = (1/3)*(1/3);
       1 / sqrt 3 = sqrt 3 / 3 by BKMODEL3:10; then
A13:   (1 / sqrt 3) * (1 / sqrt 3) = k * ((sqrt 3) * sqrt 3)
                                  .= k * (sqrt (3 * 3)) by SQUARE_1:29
                                  .= k * sqrt (3^2) by SQUARE_1:def 1
                                  .= k * 3 by SQUARE_1:def 2;
A14:   v.2 * v.2 = (1/sqrt 3) * (1/sqrt 3) * u2 * u2 by A12
                .= k * 3 * u2 * u2 by A13;
        reconsider P = homography(N).y as Point of ProjectiveSpace TOP-REAL 3;
        qfconic(1,1,-1,0,0,0,v)=0
        proof
          qfconic(1,1,-1,0,0,0,v)
          = 1 * v.1 * v.1 + 1 * v.2 * v.2 + (-1) * v.3 * v.3
            + 0 * v.1 * v.2 + 0 * v.1 * v.3 + 0 * v.2 * v.3 by PASCAL:def 1
         .= k * (4 * u1 * u1 - 4 * u1 * u3 + u3 * u3) + k * 3 * u2 * u2
            - k * (u1 * u1 - 4 * u1 * u3 + 4 * u3 * u3) by A12,A14
         .= k * 3 * (l * l) * (yu`1 * yu`1 + yu`2 * yu`2 - yu`3 * yu`3)
         .= 0 by A8,A9;
         hence thesis;
       end;
       hence x in absolute by A4,A10,PASCAL:11;
     end;
     hence thesis;
   end;

theorem
  for N being invertible Matrix of 3,F_Real st
  N = <* <* 2,   0   , -1 *>,
         <* 0, sqrt 3,  0 *>,
         <* 1,   0   , -2 *> *>
  holds
  homography(N).:absolute = absolute
  proof
    let N be invertible Matrix of 3,F_Real;
    assume
A1: N = <* <* 2,   0   ,-1 *>,
           <* 0, sqrt 3, 0 *>,
           <* 1,   0   ,-2 *> *>;
    reconsider a=2,b=0,c = -1,d=0,e=sqrt 3,f=0,g=1,h=0,i=-2
      as Element of F_Real by XREAL_0:def 1;
A2: homography(N).:absolute c= absolute
    proof
      let x be object;
      assume x in homography(N).:absolute;
      then consider y be object such that
A3:   y in dom homography(N) and
A4:   y in absolute and
A5:   x = homography(N).y by FUNCT_1:def 6;
      reconsider y as Point of ProjectiveSpace TOP-REAL 3 by A3;
      consider yu be non zero Element of TOP-REAL 3 such that
A6:   (yu.1)^2 + (yu.2)^2 = 1 and
A7:   yu.3 = 1 and
A8:   y = Dir yu by A4,BKMODEL1:89;
A9:   yu`1 * yu`1 + yu`2 * yu`2 = yu.1 * yu`1 + yu`2 * yu`2 by EUCLID_5:def 1
                               .= yu.1 * yu.1 + yu`2 * yu`2 by EUCLID_5:def 1
                               .= yu.1 * yu.1 + yu.2 * yu`2 by EUCLID_5:def 2
                               .= yu.1 * yu.1 + yu.2 * yu.2 by EUCLID_5:def 2
                               .= (yu.1)^2 + yu.2 * yu.2 by SQUARE_1:def 1
                               .= 1 by A6,SQUARE_1:def 1;
A10:  yu`3 * yu`3 = yu.3 * yu`3 by EUCLID_5:def 3
                 .= 1 by A7,EUCLID_5:def 3;
      consider u,v be Element of TOP-REAL 3,
                uf be FinSequence of F_Real,
                p be FinSequence of 1-tuples_on REAL
      such that
A11:  y = Dir u & u is not zero & u = uf & p = N * uf & v = M2F p &
        v is not zero & homography(N).y = Dir v by ANPROJ_8:def 4;
        are_Prop u,yu by A8,A11,ANPROJ_1:22;
      then consider l be Real such that l <> 0 and
A12:  u = l * yu by ANPROJ_1:1;
      reconsider u1 = l * yu`1,u2 = l * yu`2,u3 = l * yu`3
        as Element of F_Real by XREAL_0:def 1;
      uf = <* u1,u2,u3 *> by A12,EUCLID_5:7,A11;
      then v = <* a*u1+b*u2+c*u3,d*u1+e*u2+f*u3,g*u1+h*u2+i*u3 *>
                by A1,A11,PASCAL:8
            .= <* 2 * u1 - u3, (sqrt 3) * u2,u1 - 2 * u3 *>;
      then v`1 = 2 * u1 - u3 & v`2 = (sqrt 3) * u2 & v`3 = u1 - 2 * u3
        by EUCLID_5:2;
      then
A13:  v.1 = 2 * u1 - u3 & v.2 = (sqrt 3) * u2 & v.3 = u1 - 2 * u3
             by EUCLID_5:def 1,def 2,def 3;
A14:  v.1 * v.1 = (2 * u1 - u3)^2 by A13,SQUARE_1:def 1
               .= (2 * u1)^2 - 2 * (2 * u1) * u3 + u3^2 by SQUARE_1:5
               .= (2 * u1) * (2 * u1) - 2 * (2 * u1) * u3 + u3^2
                 by SQUARE_1:def 1
               .= 4 * u1 * u1 - 4 * u1 * u3 + u3 * u3 by SQUARE_1:def 1;
A15:  v.2 * v.2 = (sqrt 3) * (sqrt 3) * u2 * u2 by A13
               .= sqrt (3 * 3) * u2 * u2 by SQUARE_1:29
               .= sqrt (3^2) * u2 * u2 by SQUARE_1:def 1
               .= 3 * u2 * u2 by SQUARE_1:def 2;
A16:  v.3 * v.3 = (u1 - 2 * u3)^2 by A13,SQUARE_1:def 1
               .= u1^2 - 2 * u1 * (2 * u3) + (2 * u3)^2 by SQUARE_1:5
               .= u1 * u1 - 2 * 2 * u1 * u3 + (2 * u3)^2 by SQUARE_1:def 1
               .= u1 * u1 - 2 * 2 * u1 * u3 + (2 * u3) * (2 * u3)
                 by SQUARE_1:def 1
               .= u1 * u1 - 4 * u1 * u3 + 4 * u3 * u3;
      reconsider P = homography(N).y as Point of ProjectiveSpace TOP-REAL 3;
      qfconic(1,1,-1,0,0,0,v)=0
      proof
        qfconic(1,1,-1,0,0,0,v) = 1 * v.1 * v.1 + 1 * v.2 * v.2
                                   + (-1) * v.3 * v.3 +
                                   0 * v.1 * v.2 + 0 * v.1 * v.3 +
                                   0 * v.2 * v.3 by PASCAL:def 1
                               .= (4 * u1 * u1 - 4 * u1 * u3 + u3 * u3) +
                                   3 * u2 * u2 - (u1 * u1
                                   - 4 * u1 * u3 + 4 * u3 * u3) by A14,A15,A16
                               .= 3 * (l * l) * (yu`1 * yu`1 + yu`2 * yu`2
                                   - yu`3 * yu`3)
                               .= 0 by A9,A10;
        hence thesis;
      end;
      hence x in absolute by A5,A11,PASCAL:11;
    end;
    absolute c= homography(N).:absolute
    proof
      let x be object;
      assume
A17:  x in absolute;
      reconsider N1 = <* <* 2/3,   0   ,-1/3 *>,
                         <* 0, 1/sqrt 3, 0 *>,
                         <* 1/3,   0   ,-2/3 *> *> as Matrix of 3,F_Real
                         by ANPROJ_8:19;
      N1 is_reverse_of N by A1,Th13;
      then reconsider N1 as invertible Matrix of 3,F_Real by MATRIX_6:def 3;
A18:  homography(N1).:absolute c= absolute by Th14;
      dom homography(N1) = the carrier of ProjectiveSpace TOP-REAL 3
        by FUNCT_2:def 1;
      then homography(N1).x in homography(N1).:absolute by A17,FUNCT_1:108;
      then reconsider y = homography(N1).x as Element of absolute by A18;
A19:  N * N1 = 1.(F_Real,3) by A1,Th11,ANPROJ_9:1;
      now
        dom homography(N) = the carrier of ProjectiveSpace TOP-REAL 3
          by FUNCT_2:def 1;
        hence y in dom homography(N);
        thus y in absolute;
        reconsider P = x as Point of ProjectiveSpace TOP-REAL 3 by A17;
        thus homography(N).y = homography(1.(F_Real,3)).P by A19,ANPROJ_9:13
                            .= x by ANPROJ_9:14;
      end;
      hence x in homography(N).:absolute by FUNCT_1:108;
    end;
    hence thesis by A2;
  end;

theorem Th15:
  for a,b,r being Real
  for P,Q,R being Element of TOP-REAL 2 st
  Q in LSeg(P,R) & P in inside_of_circle(a,b,r) & R in inside_of_circle(a,b,r)
  holds Q in inside_of_circle(a,b,r)
  proof
    let a,b,r be Real;
    let P,Q,R be Element of TOP-REAL 2;
    assume that
A1: Q in LSeg(P,R) and
A2: P in inside_of_circle(a,b,r) and
A3: R in inside_of_circle(a,b,r);
    consider s be Real such that
A4: 0 <= s & s <= 1 and
A5: Q = (1 - s)*P + s * R by A1,RLTOPSP1:76;
    s in [. 0,1 .] by A4,XXREAL_1:1;
    then s in ]. 0,1 .[ or s = 0 or s = 1 by XXREAL_1:5;
    then per cases by XXREAL_1:4;
    suppose
A6:   0 < s & s < 1;
      Q = s * R + (1 - s)* P by A5;
      hence thesis by A2,A3,A6,CONVEX1:def 2;
    end;
    suppose
      s = 0;
      then Q = P + 0 * R by A5,RVSUM_1:52
            .= P by GTARSKI2:2;
      hence thesis by A2;
    end;
    suppose s = 1;
      then Q = R + 0 * P by A5,RVSUM_1:52
            .= R by GTARSKI2:2;
      hence thesis by A3;
    end;
  end;

theorem Th16:
  for u,v being non zero Element of TOP-REAL 3 st
  Dir u = Dir v & u.3 <> 0 & u.3 = v.3 holds u = v
  proof
    let u,v be non zero Element of TOP-REAL 3;
    assume that
A1: Dir u = Dir v and
A2: u.3 <> 0 and
A3: u.3 = v.3;
    are_Prop u,v by A1,ANPROJ_1:22;
    then consider a be Real such that a <> 0 and
A4: u = a * v by ANPROJ_1:1;
    u.3 = a * u.3 by A3,A4,RVSUM_1:44;
    then a = 1 by A2,XCMPLX_1:7;
    hence thesis by A4,RVSUM_1:52;
  end;

theorem Th17:
  for R being Element of ProjectiveSpace TOP-REAL 3
  for P,Q being Element of BK_model
  for u,v,w being non zero Element of TOP-REAL 3
  for r being Real st 0 <= r <= 1 & P = Dir u &
  Q = Dir v & R = Dir w & u.3 = 1 & v.3 = 1 &
  w = r * u + (1 - r) * v holds R is Element of BK_model
  proof
    let R be Element of ProjectiveSpace TOP-REAL 3;
    let P,Q be Element of BK_model;
    let u,v,w be non zero Element of TOP-REAL 3;
    let r be Real;
    assume that
A1: 0 <= r <= 1 and
A2: P = Dir u & Q = Dir v & R = Dir w and
A3: u.3 = 1 & v.3 = 1 and
A4: w = r * u + (1 - r) * v;
    reconsider ru = r * u,rv  = (1 - r) * v as Element of REAL 3 by EUCLID:22;
A5: w.3 = ru.3 + rv.3 by A4,RVSUM_1:11
       .= r * u.3 + rv.3 by RVSUM_1:44
       .= r + (1 - r) * 1 by A3,RVSUM_1:44
       .= 1;
    consider u2 be non zero Element of TOP-REAL 3 such that
A6: Dir u2 = P & u2.3 = 1 & BK_to_REAL2 P = |[u2.1,u2.2]| by BKMODEL2:def 2;
A7: u = u2 by A2,A3,A6,Th16;
    reconsider ru2 = |[u2.1,u2.2]| as Element of TOP-REAL 2;
    consider v2 be non zero Element of TOP-REAL 3 such that
A8: Dir v2 = Q & v2.3 = 1 & BK_to_REAL2 Q = |[v2.1,v2.2]| by BKMODEL2:def 2;
A9: v = v2 by A2,A3,A8,Th16;
    reconsider rv2 = |[v2.1,v2.2]| as Element of TOP-REAL 2;
    reconsider rw = |[w.1,w.2]| as Element of TOP-REAL 2;
    rw = r * ru2 + (1 - r) * rv2
    proof
A10:  w.1 = ru.1 + rv.1 by A4,RVSUM_1:11
                .= r * u.1 + rv.1 by RVSUM_1:44
                .= r * u2.1 + (1 - r) * v2.1 by A7,A9,RVSUM_1:44;
A13:  w.2 = ru.2 + rv.2 by A4,RVSUM_1:11
                .= r * u.2 + rv.2 by RVSUM_1:44
                .= r * u2.2 + (1 - r) * v2.2 by A7,A9,RVSUM_1:44;
      r * ru2 + (1 - r) * rv2 = |[r*u2.1,r*u2.2]| + (1 - r) * |[v2.1,v2.2]|
                                 by EUCLID:58
                             .= |[r*u2.1,r*u2.2]| + |[(1-r)*v2.1,(1-r)*v2.2]|
                                 by EUCLID:58;
      hence thesis by A10,A13,EUCLID:56;
    end;
    then rw = (1 - r) * rv2 + r * ru2;
    then rw in {(1 - r) * rv2 + r * ru2 where r is Real:0 <= r & r <= 1} by A1;
    then rw in LSeg(rv2,ru2) by RLTOPSP1:def 2;
    then reconsider rw as Element of inside_of_circle(0,0,1) by A6,A8,Th15;
    consider RW2 be Element of TOP-REAL 2 such that
A11: RW2 = rw & REAL2_to_BK rw = Dir |[RW2`1,RW2`2,1]| by BKMODEL2:def 3;
A12: rw`1 = w.1 & rw`2 = w.2 by EUCLID:52;
    w = |[w`1,w`2,w`3]| by EUCLID_5:3
     .= |[w.1,w`2,w`3]| by EUCLID_5:def 1
     .= |[w.1,w.2,w`3]| by EUCLID_5:def 2
     .= |[w.1,w.2,w.3]| by EUCLID_5:def 3;
    hence thesis by A2,A11,A5,A12;
  end;

theorem Th18:
  for N being invertible Matrix of 3,F_Real
  for n11,n12,n13,n21,n22,n23,n31,n32,n33 being Element of F_Real
  for P,Q being Point of ProjectiveSpace TOP-REAL 3
  for u,v being non zero Element of TOP-REAL 3 st
  N = <* <* n11,n12,n13 *>,
         <* n21,n22,n23 *>,
         <* n31,n32,n33 *> *> &
  P = Dir u & Q = Dir v & Q = homography(N).P & u.3 = 1
  holds ex a being non zero Real st
  v.1 = a * (n11 * u.1 + n12 * u.2 + n13) &
  v.2 = a * (n21 * u.1 + n22 * u.2 + n23) &
  v.3 = a * (n31 * u.1 + n32 * u.2 + n33)
  proof
    let N be invertible Matrix of 3,F_Real;
    let n11,n12,n13,n21,n22,n23,n31,n32,n33 be Element of F_Real;
    let P,Q be Point of ProjectiveSpace TOP-REAL 3;
    let u,v be non zero Element of TOP-REAL 3;
    assume
A1: N = <* <* n11,n12,n13 *>, <* n21,n22,n23 *>, <* n31,n32,n33 *> *> &
    P = Dir u & Q = Dir v & Q = homography(N).P & u.3 = 1;
    consider u9,v9 be Element of TOP-REAL 3,
                uf be FinSequence of F_Real,
                p be FinSequence of 1-tuples_on REAL
    such that
A2: P = Dir u9 & u9 is not zero & u9 = uf & p = N * uf & v9 = M2F p &
      v9 is not zero & homography(N).P = Dir v9 by ANPROJ_8:def 4;
    are_Prop u,u9 by A1,A2,ANPROJ_1:22;
    then consider a be Real such that
A3: a <> 0 & u9 = a * u by ANPROJ_1:1;
A4: |[u9`1,u9`2,u9`3]| = u9 by EUCLID_5:3
                      .= |[ a * u`1,a * u`2, a * u`3 ]|
                        by A3,EUCLID_5:7
                      .= |[ a * u`1,a * u`2, a * u.3 ]| by EUCLID_5:def 3
                      .= |[ a * u`1,a * u`2, a]| by A1;
    reconsider uf1=a*u`1,uf2=a*u`2,uf3=a as Element of F_Real by XREAL_0:def 1;
    reconsider x1 = n11*u`1+n12*u`2+n13, x2 = n21*u`1+n22*u`2+n23,
    x3 = n31*u`1+n32*u`2+n33 as Element of REAL by XREAL_0:def 1;
    uf = <* uf1,uf2,uf3 *> by A2,A4,EUCLID_5:3;
    then
A5: v9 = <* n11*uf1+n12*uf2+n13*uf3,
            n21*uf1+n22*uf2+n23*uf3,
            n31*uf1+n32*uf2+n33*uf3 *> by A1,A2,PASCAL:8
      .= <* a*(n11*u`1+n12*u`2+n13),
            a*(n21*u`1+n22*u`2+n23),
            a*(n31*u`1+n32*u`2+n33) *>
      .= a * |[x1,x2,x3]| by EUCLID_5:8;
    are_Prop v,v9 by A1,A2,ANPROJ_1:22;
    then consider b be Real such that
A6: b <> 0 and
A7: v = b * v9 by ANPROJ_1:1;
A8: v = b * |[a * x1,a * x2, a * x3]| by A7,A5,EUCLID_5:8
     .= |[ b * (a * x1),b * (a * x2),b * (a * x3)]| by EUCLID_5:8
     .= |[ (b * a) * (n11 * u`1 + n12 * u`2 + n13),
           (b * a) * (n21 * u`1 + n22 * u`2 + n23),
           (b * a) * (n31 * u`1 + n32 * u`2 + n33) ]|;
    reconsider c = b * a as non zero Real by A3,A6;
    take c;
    v`1 = c * (n11 * u`1 + n12 * u`2 + n13) &
      v`2 = c * (n21 * u`1 + n22 * u`2 + n23) &
      v`3 = c * (n31 * u`1 + n32 * u`2 + n33)
      by A8,EUCLID_5:2;
    then v.1 = c * (n11 * u`1 + n12 * u`2 + n13) &
      v.2 = c * (n21 * u`1 + n22 * u`2 + n23) &
      v.3 = c * (n31 * u`1 + n32 * u`2 + n33)
      by EUCLID_5:def 1,def 2,def 3;
    then v.1 = c * (n11 * u.1 + n12 * u`2 + n13) &
      v.2 = c * (n21 * u.1 + n22 * u`2 + n23) &
      v.3 = c * (n31 * u.1 + n32 * u`2 + n33)
      by EUCLID_5:def 1;
    hence thesis by EUCLID_5:def 2;
  end;

theorem Th19:
  for N being invertible Matrix of 3,F_Real
  for n11,n12,n13,n21,n22,n23,n31,n32,n33 being Element of F_Real
  for P being Element of BK_model
  for Q being Point of ProjectiveSpace TOP-REAL 3
  for u,v being non zero Element of TOP-REAL 3 st
  N = <* <* n11,n12,n13 *>,
         <* n21,n22,n23 *>,
         <* n31,n32,n33 *> *> &
  P = Dir u & Q = Dir v & Q = homography(N).P &
  u.3 = 1 & v.3 = 1 holds n31 * u.1 + n32 * u.2 + n33 <> 0 &
  v.1 = (n11 * u.1 + n12 * u.2 + n13) / (n31 * u.1 + n32 * u.2 + n33) &
  v.2 = (n21 * u.1 + n22 * u.2 + n23) / (n31 * u.1 + n32 * u.2 + n33)
  proof
    let N be invertible Matrix of 3,F_Real;
    let n11,n12,n13,n21,n22,n23,n31,n32,n33 be Element of F_Real;
    let P be Element of BK_model;
    let Q be Point of ProjectiveSpace TOP-REAL 3;
    let u,v be non zero Element of TOP-REAL 3;
    assume that
A1: N = <* <* n11,n12,n13 *>,
              <* n21,n22,n23 *>,
              <* n31,n32,n33 *> *> and
A2: P = Dir u and
A3: Q = Dir v and
A4: Q = homography(N).P and
A5: u.3 = 1 and
A6: v.3 = 1;
    consider a be non zero Real such that
A7: v.1 = a * (n11 * u.1 + n12 * u.2 + n13) and
A8: v.2 = a * (n21 * u.1 + n22 * u.2 + n23) and
A9: v.3 = a * (n31 * u.1 + n32 * u.2 + n33) by A1,A2,A3, A4,A5,Th18;
    thus n31 * u.1 + n32 * u.2 + n33 <> 0 by A6,A9;
    reconsider nn = n31 * u.1 + n32 * u.2 + n33 as non zero Real by A6,A9;
    a = 1 / nn by A6,A9,XCMPLX_1:73;
    hence thesis by A7,A8;
  end;

theorem Th20:
  for N being invertible Matrix of 3,F_Real
  for h being Element of SubGroupK-isometry
  for n11,n12,n13,n21,n22,n23,n31,n32,n33 being Element of F_Real
  for P being Element of BK_model
  for u being non zero Element of TOP-REAL 3 st
  h = homography(N) & N = <* <* n11,n12,n13 *>,
                             <* n21,n22,n23 *>,
                             <* n31,n32,n33 *> *> &
  P = Dir u & u.3 = 1 holds n31 * u.1 + n32 * u.2 + n33 <> 0
  proof
    let N be invertible Matrix of 3,F_Real;
    let h be Element of SubGroupK-isometry;
    let n11,n12,n13,n21,n22,n23,n31,n32,n33 be Element of F_Real;
    let P be Element of BK_model;
    let u be non zero Element of TOP-REAL 3;
    assume
A1: h = homography(N) & N = <* <* n11,n12,n13 *>,
                               <* n21,n22,n23 *>,
                               <* n31,n32,n33 *> *> &
    P = Dir u & u.3 = 1;
    reconsider Q = homography(N).P as Point of ProjectiveSpace TOP-REAL 3;
    reconsider Q = homography(N).P as Element of BK_model by A1,BKMODEL3:36;
    ex v be non zero Element of TOP-REAL 3 st Q = Dir v & v.3 = 1 &
      BK_to_REAL2 Q = |[v.1,v.2]| by BKMODEL2:def 2;
    hence thesis by A1,Th19;
  end;

theorem Th21:
  for N being invertible Matrix of 3,F_Real
  for n11,n12,n13,n21,n22,n23,n31,n32,n33 being Element of F_Real
  for P being Element of absolute
  for Q being Point of ProjectiveSpace TOP-REAL 3
  for u,v being non zero Element of TOP-REAL 3 st
  N = <* <* n11,n12,n13 *>,
         <* n21,n22,n23 *>,
         <* n31,n32,n33 *> *> &
  P = Dir u & Q = Dir v & Q = homography(N).P & u.3 = 1 & v.3 = 1
  holds n31 * u.1 + n32 * u.2 + n33 <> 0 &
  v.1 = (n11 * u.1 + n12 * u.2 + n13) / (n31 * u.1 + n32 * u.2 + n33) &
  v.2 = (n21 * u.1 + n22 * u.2 + n23) / (n31 * u.1 + n32 * u.2 + n33)
  proof
    let N be invertible Matrix of 3,F_Real;
    let n11,n12,n13,n21,n22,n23,n31,n32,n33 be Element of F_Real;
    let P be Element of absolute;
    let Q be Point of ProjectiveSpace TOP-REAL 3;
    let u,v be non zero Element of TOP-REAL 3;
    assume
A1: N = <* <* n11,n12,n13 *>,
           <* n21,n22,n23 *>,
           <* n31,n32,n33 *> *> &
    P = Dir u & Q = Dir v & Q = homography(N).P & u.3 = 1 & v.3 = 1;
    consider a be non zero Real such that
A2: v.1 = a * (n11 * u.1 + n12 * u.2 + n13) and
A3: v.2 = a * (n21 * u.1 + n22 * u.2 + n23) and
A4: v.3 = a * (n31 * u.1 + n32 * u.2 + n33) by A1,Th18;
    thus n31 * u.1 + n32 * u.2 + n33 <> 0 by A1,A4;
    reconsider nn = n31 * u.1 + n32 * u.2 + n33 as non zero Real by A1,A4;
    a = 1 / nn by A1,A4,XCMPLX_1:73;
    hence thesis by A2,A3;
  end;

theorem Th22:
  for N being invertible Matrix of 3,F_Real
  for h being Element of SubGroupK-isometry
  for n11,n12,n13,n21,n22,n23,n31,n32,n33 being Element of F_Real
  for P being Element of absolute
  for u being non zero Element of TOP-REAL 3 st
  h = homography(N) & N = <* <* n11,n12,n13 *>,
                             <* n21,n22,n23 *>,
                             <* n31,n32,n33 *> *> &
  P = Dir u & u.3 = 1 holds n31 * u.1 + n32 * u.2 + n33 <> 0
  proof
    let N be invertible Matrix of 3,F_Real;
    let h be Element of SubGroupK-isometry;
    let n11,n12,n13,n21,n22,n23,n31,n32,n33 be Element of F_Real;
    let P be Element of absolute;
    let u be non zero Element of TOP-REAL 3;
    assume
A1: h = homography(N) & N = <* <* n11,n12,n13 *>,
                               <* n21,n22,n23 *>,
                               <* n31,n32,n33 *> *> &
    P = Dir u & u.3 = 1;
    reconsider Q = homography(N).P as Point of ProjectiveSpace TOP-REAL 3;
    reconsider Q = homography(N).P as Element of absolute by A1,BKMODEL3:35;
    ex v be non zero Element of TOP-REAL 3 st Q = Dir v & v.3 = 1 &
      absolute_to_REAL2 Q = |[v.1,v.2]| by BKMODEL1:def 8;
    hence thesis by A1,Th21;
  end;

theorem Th23:
  for N being invertible Matrix of 3,F_Real
  for h being Element of SubGroupK-isometry
  for n11,n12,n13,n21,n22,n23,n31,n32,n33 being Element of F_Real
  for P being Element of BK_model
  for u being non zero Element of TOP-REAL 3 st
  h = homography(N) & N = <* <* n11,n12,n13 *>,
                             <* n21,n22,n23 *>,
                             <* n31,n32,n33 *> *> &
  P = Dir u & u.3 = 1 holds
  homography(N).P = Dir |[
    (n11 * u.1 + n12 * u.2 + n13) / (n31 * u.1 + n32 * u.2 + n33),
    (n21 * u.1 + n22 * u.2 + n23) / (n31 * u.1 + n32 * u.2 + n33),
    1 ]|
  proof
    let N be invertible Matrix of 3,F_Real;
    let h be Element of SubGroupK-isometry;
    let n11,n12,n13,n21,n22,n23,n31,n32,n33 be Element of F_Real;
    let P be Element of BK_model;
    let u be non zero Element of TOP-REAL 3;
    assume
A1: h = homography(N) & N = <* <* n11,n12,n13 *>,
                               <* n21,n22,n23 *>,
                               <* n31,n32,n33 *> *> &
    P = Dir u & u.3 = 1;
    reconsider Q = homography(N).P as Element of BK_model by A1,BKMODEL3:36;
    consider v be non zero Element of TOP-REAL 3 such that
A2: Q = Dir v & v.3 = 1 & BK_to_REAL2 Q = |[v.1,v.2]| by BKMODEL2:def 2;
    n31 * u.1 + n32 * u.2 + n33 <> 0 &
      v.1 = (n11 * u.1 + n12 * u.2 + n13) / (n31 * u.1 + n32 * u.2 + n33) &
      v.2 = (n21 * u.1 + n22 * u.2 + n23) / (n31 * u.1 + n32 * u.2 + n33)
      by A2,A1,Th19;
    then v`1 = (n11 * u.1 + n12 * u.2 + n13) / (n31 * u.1 + n32 * u.2 + n33) &
      v`2 = (n21 * u.1 + n22 * u.2 + n23) / (n31 * u.1 + n32 * u.2 + n33) &
      v`3 = 1 by A2,EUCLID_5:def 1,def 2,def 3;
    hence thesis by A2,EUCLID_5:3;
  end;

theorem Th24:
  for N being invertible Matrix of 3,F_Real
  for h being Element of SubGroupK-isometry
  for n11,n12,n13,n21,n22,n23,n31,n32,n33 being Element of F_Real
  for P being Element of absolute
  for u being non zero Element of TOP-REAL 3 st
  h = homography(N) & N = <* <* n11,n12,n13 *>,
                             <* n21,n22,n23 *>,
                             <* n31,n32,n33 *> *> &
  P = Dir u & u.3 = 1 holds
  homography(N).P = Dir |[
    (n11 * u.1 + n12 * u.2 + n13) / (n31 * u.1 + n32 * u.2 + n33),
    (n21 * u.1 + n22 * u.2 + n23) / (n31 * u.1 + n32 * u.2 + n33),
    1 ]|
  proof
    let N be invertible Matrix of 3,F_Real;
    let h be Element of SubGroupK-isometry;
    let n11,n12,n13,n21,n22,n23,n31,n32,n33 be Element of F_Real;
    let P be Element of absolute;
    let u be non zero Element of TOP-REAL 3;
    assume that
A1: h = homography(N) & N = <* <* n11,n12,n13 *>,
                               <* n21,n22,n23 *>,
                               <* n31,n32,n33 *> *> and
A2: P = Dir u & u.3 = 1;
    reconsider Q = homography(N).P as Element of absolute by A1,BKMODEL3:35;
    consider v be non zero Element of TOP-REAL 3 such that
A3: Q = Dir v & v.3 = 1 &
      absolute_to_REAL2(Q) = |[v.1,v.2]| by BKMODEL1:def 8;
    now
      n31 * u.1 + n32 * u.2 + n33 <> 0 &
        v.1 = (n11 * u.1 + n12 * u.2 + n13) / (n31 * u.1 + n32 * u.2 + n33) &
        v.2 = (n21 * u.1 + n22 * u.2 + n23) / (n31 * u.1 + n32 * u.2 + n33)
        by A3,A2,A1,Th21;
      hence v`1 = (n11 * u.1 + n12 * u.2 + n13) /
                    (n31 * u.1 + n32 * u.2 + n33) &
        v`2 = (n21 * u.1 + n22 * u.2 + n23) / (n31 * u.1 + n32 * u.2 + n33) &
        v`3 = 1 by A3,EUCLID_5:def 1,def 2,def 3;
      thus homography(N).P = Dir |[v`1,v`2,v`3]| by A3,EUCLID_5:3;
    end;
    hence thesis;
  end;

theorem Th26:
  for A being Subset of TOP-REAL 3
  for B being convex non empty Subset of TOP-REAL 2
  for r being Real
  for x being Element of TOP-REAL 3 st
  A = {x where x is Element of TOP-REAL 3:|[x`1,x`2]| in B & x`3 = r}
  holds A is non empty convex
  proof
    let A be Subset of TOP-REAL 3;
    let B be convex non empty Subset of TOP-REAL 2;
    let r be Real;
    let x be Element of TOP-REAL 3;
    assume
A1: A = {x where x is Element of TOP-REAL 3:|[x`1,x`2]| in B & x`3 = r};
A2: for z be Element of TOP-REAL 3 holds z in A iff |[z`1,z`2]| in B & z`3 = r
    proof
      let z be Element of TOP-REAL 3;
      hereby
        assume z in A;
        then ex z9 be Element of TOP-REAL 3 st z = z9 & |[z9`1,z9`2]| in B &
          z9`3 = r by A1;
        hence |[z`1,z`2]| in B & z`3 = r;
      end;
      assume |[z`1,z`2]| in B & z`3 = r;
      hence z in A by A1;
    end;
    set y = the Element of B;
    reconsider z = |[y`1,y`2,r]| as Element of TOP-REAL 3;
    z = |[z`1,z`2,z`3]| by EUCLID_5:3;
    then
A3: z`1 = y`1 & z`2 = y`2 & z`3 = r by FINSEQ_1:78;
    y in B;
    then |[z`1,z`2]| in B & z`3 = r by A3,EUCLID:53;
    then z in A by A1;
    hence A is non empty;
    now
      let u,v be Element of TOP-REAL 3;
      let s be Real;
      assume that
A4:   0 < s < 1 and
A5:   u in A and
A6:   v in A;
      reconsider w = s * u + (1 - s) * v as Element of TOP-REAL 3;
      now
        reconsider su = s * u,sv = (1 - s) * v as Element of TOP-REAL 3;
        su = |[s * u`1,s * u`2,s * u`3]| &
          sv = |[(1-s)*v`1,(1-s)*v`2,(1-s)*v`3]| by EUCLID_5:7;
        then
A7:     |[s * u`1 + (1-s)*v`1,s*u`2+(1-s)*v`2,s*u`3+(1-s)*v`3]|
          = w by EUCLID_5:6
         .= |[w`1,w`2,w`3]| by EUCLID_5:3;
        then
A8:     w`1 = s * u`1 + (1-s)*v`1 & w`2=s*u`2+(1-s)*v`2 & w`3=s*u`3+(1-s)*v`3
          by FINSEQ_1:78;
        u`3 = r & v`3 = r by A5,A6,A2;
        hence w`3 = r by A7,FINSEQ_1:78;
        reconsider u9 = |[u`1,u`2]|,v9 = |[v`1,v`2]|,w9 = |[w`1,w`2]|
          as Element of TOP-REAL 2;
        now
          thus u9 in B & v9 in B by A2,A6,A5;
          thus |[w`1,w`2]| = |[s*u`1,s*u`2]| + |[(1-s)*v`1,(1-s)*v`2]|
                             by A8,EUCLID:56
                          .= s * |[u`1,u`2]| + |[(1-s)*v`1,(1-s)*v`2]|
                             by EUCLID:58
                          .= s * u9 + (1 - s) * v9 by EUCLID:58;
        end;
        hence |[w`1,w`2]| in B by A4,CONVEX1:def 2;
      end;
      hence s * u + (1 - s) * v in A by A1;
    end;
    hence A is convex by CONVEX1:def 2;
  end;

theorem Th27:
  for n1,n2,n3 being Element of F_Real
  for n,u being Element of TOP-REAL 3 st n = <* n1,n2,n3 *> &
  u.3 = 1 holds |( n, u )| = n1 * u.1 + n2 * u.2 + n3
  proof
    let n1,n2,n3 be Element of F_Real;
    let n,u be Element of TOP-REAL 3;
    assume that
A1: n = <* n1,n2,n3 *> and
A2: u.3 = 1;
    n = |[n`1,n`2,n`3]| by EUCLID_5:3;
    then
A3: n`1 = n1 & n`2 = n2 & n`3 = n3 by A1,FINSEQ_1:78;
    |( n, u )| = n1 * u`1 + n2 * u`2 + n3 * u`3 by A3,EUCLID_5:29
              .= n1 * u.1 + n2 * u`2 + n3 * u`3 by EUCLID_5:def 1
              .= n1 * u.1 + n2 * u.2 + n3 * u`3 by EUCLID_5:def 2
              .= n1 * u.1 + n2 * u.2 + n3 * u.3 by EUCLID_5:def 3;
    hence thesis by A2;
  end;

theorem Th28:
  for A being convex non empty Subset of TOP-REAL 3
  for n,u,v being Element of TOP-REAL 3 st
  (for w being Element of TOP-REAL 3 st w in A holds |( n,w )| <> 0) &
  u in A & v in A holds 0 < |( n,u )| * |( n,v )|
  proof
    let A be convex non empty Subset of TOP-REAL 3;
    let n,u,v be Element of TOP-REAL 3;
    assume that
A1: for w be Element of TOP-REAL 3 st w in A holds |( n,w )| <> 0 and
A2: u in A & v in A;
    set x = |( n,u )|,
        y = |( n,v )|;
    assume
A3: not 0 < |( n,u )| * |( n,v)|;
A4: x <> 0 & y <> 0 by A1,A2;
    then
A5: 0 < x / (x - y) < 1 by A3,BKMODEL3:1;
    reconsider l = x / (x - y) as non zero Real by A3,A4,BKMODEL3:1;
    reconsider w = l * v + (1 - l) * u as Element of TOP-REAL 3;
    x <> y
    proof
      assume x = y;
      then l = 0 by XCMPLX_1:49;
      hence contradiction;
    end;
    then
A6: 1 - l = - y / (x - y) by Th25;
    |( n,w )| = 0
    proof
      |( n , w )| = |( n, l * v )| + |( n, (1 - l) * u)| by EUCLID_2:26
                 .= l * |(n , v)| + |( n, (1 - l) * u)| by EUCLID_2:19
                 .= x / (x - y) * y + (-y) / (x - y) * x by A6,EUCLID_2:19;
      hence thesis;
    end;
    hence contradiction by A1,A2,A5,CONVEX1:def 2;
  end;

theorem Th29:
  for n31,n32,n33 being Element of F_Real
  for u,v being Element of TOP-REAL 2 st u in inside_of_circle(0,0,1) &
  v in inside_of_circle(0,0,1) &
  (for w being Element of TOP-REAL 2 st w in inside_of_circle(0,0,1) holds
  n31 * w.1 + n32 * w.2 + n33 <> 0) holds
  0 < (n31 * u.1 + n32 * u.2 + n33) * (n31 * v.1 + n32 * v.2 + n33)
  proof
    let n31,n32,n33 be Element of F_Real;
    let u,v be Element of TOP-REAL 2;
    assume that
A1: u in inside_of_circle(0,0,1) and
A2: v in inside_of_circle(0,0,1) and
A3: for w be Element of TOP-REAL 2 st w in inside_of_circle(0,0,1) holds
      n31 * w.1 + n32 * w.2 + n33 <> 0;
    set B = inside_of_circle(0,0,1);
    set A = {x where x is Element of TOP-REAL 3:|[x`1,x`2]| in B & x`3 = 1};
    A c= the carrier of TOP-REAL 3
    proof
      let x be object;
      assume x in A;
      then ex y be Element of TOP-REAL 3 st x= y & |[y`1,y`2]| in B & y`3 = 1;
      hence thesis;
    end;
    then reconsider A as Subset of TOP-REAL 3;
    reconsider A as non empty convex Subset of TOP-REAL 3 by Th26;
    reconsider n = |[ n31,n32,n33 ]|, u9 = |[u.1,u.2,1]|,v9 = |[v.1,v.2,1]|
      as Element of TOP-REAL 3;
A4: |[u`1,u`2]| in B & |[v`1,v`2]| in B by A1,A2,EUCLID:53;
A5: u9`1 = u.1 & u9`2 = u.2 & u9`3 = 1 &
    v9`1 = v.1 & v9`2 = v.2 & v9`3 = 1 by EUCLID_5:2;
A6: u9 in A & v9 in A by A5,A4;
A7:
    now
      let w be Element of TOP-REAL 3;
      assume w in A;
      then consider x be Element of TOP-REAL 3 such that
A8:   w = x and
A9:   |[x`1,x`2]| in B and
A10:  x`3 = 1;
      reconsider v = |[x`1,x`2]| as Element of TOP-REAL 2;
      now
        w.3 = 1 by A8,A10,EUCLID_5:def 3;
        hence |(n,w)| = n31 * w.1 + n32 * w.2 + n33 by Th27;
        thus w.1 = w`1 by EUCLID_5:def 1
                .= v`1 by A8,EUCLID:52
                .= v.1;
        thus w.2 = w`2 by EUCLID_5:def 2
                .= v`2 by A8,EUCLID:52
                .= v.2;
      end;
      hence |(n,w)| <> 0 by A3,A9;
    end;
    now
      n = <*n31,n32,n33*> & u9.3 = 1 by A5,EUCLID_5:def 3;
      then |(n,u9)| = n31 * u9.1 + n32 * u9.2 + n33 by Th27;
      then |(n,u9)| = n31 * u9`1 + n32 * u9.2 + n33 by EUCLID_5:def 1;
      hence |(n,u9)| = n31 * u.1 + n32 * u.2 + n33 by A5,EUCLID_5:def 2;
      n = <*n31,n32,n33*> & v9.3 = 1 by A5,EUCLID_5:def 3;
      then |(n,v9)| = n31 * v9.1 + n32 * v9.2 + n33 by Th27;
      then |(n,v9)| = n31 * v9`1 + n32 * v9.2 + n33 by EUCLID_5:def 1;
      hence |(n,v9)| = n31 * v.1 + n32 * v.2 + n33 by A5,EUCLID_5:def 2;
    end;
    hence thesis by A7,A6,Th28;
  end;

theorem Th30:
  for n31,n32,n33 being Element of F_Real
  for u,v being Element of TOP-REAL 2 st u in inside_of_circle(0,0,1) &
  v in circle(0,0,1) &
  (for w be Element of TOP-REAL 2 st w in closed_inside_of_circle(0,0,1) holds
  n31 * w.1 + n32 * w.2 + n33 <> 0) holds
  0 < (n31 * u.1 + n32 * u.2 + n33) * (n31 * v.1 + n32 * v.2 + n33)
  proof
    let n31,n32,n33 be Element of F_Real;
    let u,v be Element of TOP-REAL 2;
    assume that
A1: u in inside_of_circle(0,0,1) and
A2: v in circle(0,0,1) and
A3: for w be Element of TOP-REAL 2 st w in closed_inside_of_circle(0,0,1) holds
    n31 * w.1 + n32 * w.2 + n33 <> 0;
    set B = closed_inside_of_circle(0,0,1);
    set A = {x where x is Element of TOP-REAL 3:|[x`1,x`2]| in B & x`3 = 1};
    A c= the carrier of TOP-REAL 3
    proof
      let x be object;
      assume x in A;
      then ex y be Element of TOP-REAL 3 st x = y & |[y`1,y`2]| in B & y`3 = 1;
      hence thesis;
    end;
    then reconsider A as Subset of TOP-REAL 3;
    reconsider A as non empty convex Subset of TOP-REAL 3 by Th26;
    reconsider n = |[ n31,n32,n33 ]|,
              u9 = |[u.1,u.2,1]|,v9 = |[v.1,v.2,1]| as Element of TOP-REAL 3;
    inside_of_circle(0,0,1) c= closed_inside_of_circle(0,0,1) &
      circle(0,0,1) c= closed_inside_of_circle(0,0,1) by TOPREAL9:46,53;
    then u in B & v in B by A1,A2;
    then
A4: |[u`1,u`2]| in B & |[v`1,v`2]| in B by EUCLID:53;
A5: u9`1 = u.1 & u9`2 = u.2 & u9`3 = 1 &
    v9`1 = v.1 & v9`2 = v.2 & v9`3 = 1 by EUCLID_5:2;
A6: u9 in A & v9 in A by A5,A4;
A7:
    now
      let w be Element of TOP-REAL 3;
      assume w in A;
      then consider x be Element of TOP-REAL 3 such that
A8:   w = x and
A9:   |[x`1,x`2]| in B and
A10:  x`3 = 1;
      reconsider v = |[x`1,x`2]| as Element of TOP-REAL 2;
      now
        w.3 = 1 by A8,A10,EUCLID_5:def 3;
        hence |(n,w)| = n31 * w.1 + n32 * w.2 + n33 by Th27;
        thus w.1 = w`1 by EUCLID_5:def 1
                .= v`1 by A8,EUCLID:52
                .= v.1;
        thus w.2 = w`2 by EUCLID_5:def 2
                .= v`2 by A8,EUCLID:52
                .= v.2;
      end;
      hence |(n,w)| <> 0 by A3,A9;
    end;
    now
      n = <*n31,n32,n33*> & u9.3 = 1 by A5,EUCLID_5:def 3;
      then |(n,u9)| = n31 * u9.1 + n32 * u9.2 + n33 by Th27;
      then |(n,u9)| = n31 * u9`1 + n32 * u9.2 + n33 by EUCLID_5:def 1;
      hence |(n,u9)| = n31 * u.1 + n32 * u.2 + n33 by A5,EUCLID_5:def 2;
      n = <*n31,n32,n33*> & v9.3 = 1 by A5,EUCLID_5:def 3;
      then |(n,v9)| = n31 * v9.1 + n32 * v9.2 + n33 by Th27;
      then |(n,v9)| = n31 * v9`1 + n32 * v9.2 + n33 by EUCLID_5:def 1;
      hence |(n,v9)| = n31 * v.1 + n32 * v.2 + n33 by A5,EUCLID_5:def 2;
    end;
    hence thesis by A7,A6,Th28;
  end;

theorem Th34:
  for l,r being Real
  for u,v,w being Element of TOP-REAL 3
  for n11,n12,n13,n21,n22,n23,n31,n32,n33,nu1,nu2,nu3,nv1,
  nv2,nv3,nw1,nw2,nw3 being Real st
  nu3 <> 0 & nv3 <> 0 & nw3 <> 0 &
  r = (l * nv3) / ((1 - l) * nu3 + l * nv3) &
  (1 - l) * nu3 + l * nv3 <> 0 &
  w = (1 - l) * u + l * v &
  nu1 = n11 * u.1 + n12 * u.2 + n13 &
  nu2 = n21 * u.1 + n22 * u.2 + n23 &
  nu3 = n31 * u.1 + n32 * u.2 + n33 &
  nv1 = n11 * v.1 + n12 * v.2 + n13 &
  nv2 = n21 * v.1 + n22 * v.2 + n23 &
  nv3 = n31 * v.1 + n32 * v.2 + n33 &
  nw1 = n11 * w.1 + n12 * w.2 + n13 &
  nw2 = n21 * w.1 + n22 * w.2 + n23 &
  nw3 = n31 * w.1 + n32 * w.2 + n33 holds
  (1 - r) * |[nu1 / nu3,nu2 / nu3,1]| + r * |[nv1 / nv3,nv2 / nv3,1]|
    = |[nw1 / nw3,nw2 / nw3,1]|
  proof
    let l,r be Real;
    let u,v,w be Element of TOP-REAL 3;
    let n11,n12,n13,n21,n22,n23,n31,n32,n33,nu1,nu2,nu3,nv1,nv2,nv3,
      nw1,nw2,nw3 be Real;
    assume
A1: nu3 <> 0 & nv3 <> 0 & nw3 <> 0 &
    r = (l * nv3) / ((1 - l) * nu3 + l * nv3) &
    (1 - l) * nu3 + l * nv3 <> 0 &
    w = (1 - l) * u + l * v &
    nu1 = n11 * u.1 + n12 * u.2 + n13 &
    nu2 = n21 * u.1 + n22 * u.2 + n23 &
    nu3 = n31 * u.1 + n32 * u.2 + n33 &
    nv1 = n11 * v.1 + n12 * v.2 + n13 &
    nv2 = n21 * v.1 + n22 * v.2 + n23 &
    nv3 = n31 * v.1 + n32 * v.2 + n33 &
    nw1 = n11 * w.1 + n12 * w.2 + n13 &
    nw2 = n21 * w.1 + n22 * w.2 + n23 &
    nw3 = n31 * w.1 + n32 * w.2 + n33;
    reconsider lu = (1 - l) * u, lv = l * v as Element of TOP-REAL 3;
    reconsider ru = (1 - l) * u, rv = l * v as Element of REAL 3 by EUCLID:22;
A2:
    now
      thus (lu + lv).1 = ru.1 + rv.1 by RVSUM_1:11
                      .= lu.1 + lv.1;
      thus (lu + lv).2 = ru.2 + rv.2 by RVSUM_1:11
                      .= lu.2 + lv.2;
      thus (lu + lv).3 = ru.3 + rv.3 by RVSUM_1:11
                      .= lu.3 + lv.3;
    end;
A3:
    now
      thus w.1 = (1-l) * u.1 + (l * v).1 by A1,A2,RVSUM_1:44
              .= (1-l) * u.1 + l * v.1 by RVSUM_1:44;
      thus w.2 = (1-l) * u.2 + (l * v).2 by A1,A2,RVSUM_1:44
              .= (1-l) * u.2 + l * v.2 by RVSUM_1:44;
      thus w.3 = (1-l) * u.3 + (l * v).3 by A1,A2,RVSUM_1:44
              .= (1-l) * u.3 + l * v.3 by RVSUM_1:44;
    end;
A4:
    now
      now
        thus (1 - r) * nu1 / nu3 = ((1 - l) * nu3 /
                                     ((1 - l) * nu3 + l * nv3)) *
                                     nu1 / nu3 by A1,Th32
                                .= (1 - l) * nu1 / ((1 - l) * nu3 + l * nv3)
                                     by A1,Th33;
        thus r * nv1 / nv3 = l * nv1 / ((1 - l) * nu3 + l * nv3) by A1,Th33;
      end;
      hence (1 - r) * nu1 / nu3 + r * nv1 / nv3 = ((1 - l) * nu1 + l * nv1) /
                                                    ((1 - l) * nu3 + l * nv3)
                                               .= nw1 / nw3 by A1,A3;
      now
        thus (1 - r) * nu2 / nu3 = ((1 - l) * nu3 /
                                     ((1 - l) * nu3 + l * nv3)) *
                                     nu2 / nu3 by A1,Th32
                                .= (1 - l) * nu2 / ((1 - l) * nu3 + l * nv3)
                                     by A1,Th33;
        thus r * nv2 / nv3 = l * nv2 / ((1 - l) * nu3 + l * nv3) by A1,Th33;
      end;
      hence (1 - r) * nu2 / nu3 + r * nv2 / nv3
        = ((1 - l) * nu2 + l * nv2) / ((1 - l) * nu3 + l * nv3)
       .= nw2 / nw3 by A1,A3;
    end;
    (1 - r) * |[nu1 / nu3,nu2 / nu3,1]| + r * |[nv1 / nv3,nv2 / nv3,1]|
      = |[ (1 - r) * (nu1 / nu3), (1 - r) * (nu2 / nu3), (1 - r) * 1 ]| +
        r * |[nv1 / nv3,nv2 / nv3,1]| by EUCLID_5:8
     .= |[ (1 - r) * nu1 / nu3, (1 - r) * nu2 / nu3, 1 - r ]|
        + |[r * (nv1 / nv3),r * (nv2 / nv3),r * 1]| by EUCLID_5:8
     .= |[ (1 - r) * nu1 / nu3 + r * nv1 / nv3, (1 - r) * nu2 / nu3 +
        r * nv2 / nv3 , 1 - r + r]| by EUCLID_5:6
     .= |[ nw1 / nw3, nw2 / nw3, 1]| by A4;
    hence thesis;
  end;

theorem
  for N being invertible Matrix of 3,F_Real
  for h being Element of SubGroupK-isometry
  for n11,n12,n13,n21,n22,n23,n31,n32,n33 being Element of F_Real
  for P being Element of BK_model st h = homography(N) &
  N = <* <* n11,n12,n13 *>, <* n21,n22,n23 *>, <* n31,n32,n33 *> *>
  holds homography(N).P = Dir |[
    (n11 * (BK_to_REAL2 P)`1 + n12 * (BK_to_REAL2 P)`2 + n13) /
    (n31 * (BK_to_REAL2 P)`1 + n32 * (BK_to_REAL2 P)`2 + n33),
    (n21 * (BK_to_REAL2 P)`1 + n22 * (BK_to_REAL2 P)`2 + n23) /
    (n31 * (BK_to_REAL2 P)`1 + n32 * (BK_to_REAL2 P)`2 + n33),1 ]|
  proof
    let N be invertible Matrix of 3,F_Real;
    let h be Element of SubGroupK-isometry;
    let n11,n12,n13,n21,n22,n23,n31,n32,n33 be Element of F_Real;
    let P be Element of BK_model;
    assume
A1: h = homography(N) & N = <* <* n11,n12,n13 *>,
                               <* n21,n22,n23 *>,
                               <* n31,n32,n33 *> *>;
    consider u be non zero Element of TOP-REAL 3 such that
A2: P = Dir u & u.3 = 1 & BK_to_REAL2 P = |[u.1,u.2]| by BKMODEL2:def 2;
    (BK_to_REAL2 P)`1 = u.1 & (BK_to_REAL2 P)`2 = u.2 &
    homography(N).P = Dir |[(n11 * u.1 + n12 * u.2 + n13) /
                            (n31 * u.1 + n32 * u.2 + n33),
                            (n21 * u.1 + n22 * u.2 + n23)
                            / (n31 * u.1 + n32 * u.2 + n33),1 ]|
                              by A1,A2,Th23,EUCLID:52;
    hence thesis;
  end;

theorem Th36:
  for h being Element of SubGroupK-isometry
  for N being invertible Matrix of 3,F_Real
  for n11,n12,n13,n21,n22,n23,n31,n32,n33 being Element of F_Real
  for u2 being Element of TOP-REAL 2
  st h = homography(N) & N = <* <* n11,n12,n13 *>,
                                <* n21,n22,n23 *>,
                                <* n31,n32,n33 *> *> &
  u2 in inside_of_circle(0,0,1) holds n31 * u2.1 + n32 * u2.2 + n33 <> 0
  proof
    let h be Element of SubGroupK-isometry;
    let N be invertible Matrix of 3,F_Real;
    let n11,n12,n13,n21,n22,n23,n31,n32,n33 be Element of F_Real;
    let u2 be Element of TOP-REAL 2;
    assume that
A1: h = homography(N) and
A2: N = <* <* n11,n12,n13 *>, <* n21,n22,n23 *>, <* n31,n32,n33 *> *> and
A3: u2 in inside_of_circle(0,0,1);
    reconsider uic = u2 as Element of inside_of_circle(0,0,1) by A3;
    consider Q be Element of TOP-REAL 2 such that
A4: Q = uic & REAL2_to_BK uic = Dir |[Q`1,Q`2,1]| by BKMODEL2:def 3;
    reconsider P = REAL2_to_BK uic as Element of BK_model;
    reconsider v = |[Q`1,Q`2,1]| as non zero Element of TOP-REAL 3;
A5: v.1 = v`1 by EUCLID_5:def 1
       .= u2.1 by A4,EUCLID_5:2;
A6: v.2 = v`2 by EUCLID_5:def 2
       .= u2.2 by A4,EUCLID_5:2;
    now
      thus P = Dir v by A4;
      thus v.3 = v`3 by EUCLID_5:def 3
              .= 1 by EUCLID_5:2;
    end;
    hence thesis by A5,A6,A1,A2,Th20;
  end;

Lem01:
  0^2 + 0^2 = 0
  proof
    0^2 + 0^2 = 0 * 0 + 0^2 by SQUARE_1:def 1
             .= 0 * 0 by SQUARE_1:def 1;
    hence thesis;
  end;

theorem Th37:
  for r being positive Real
  for u being Element of TOP-REAL 2 st u in circle(0,0,r)
  holds u is non zero
  proof
    let r be positive Real;
    let u be Element of TOP-REAL 2;
    assume
A1: u in circle(0,0,r);
    assume u is zero;
    then r^2 = 0 by A1,BKMODEL1:14,EUCLID:54,Lem01;
    hence contradiction;
  end;

theorem Th38:
  for h being Element of SubGroupK-isometry
  for N being invertible Matrix of 3,F_Real
  for n11,n12,n13,n21,n22,n23,n31,n32,n33 being Element of F_Real
  for u2 being Element of TOP-REAL 2
  st h = homography(N) & N = <* <* n11,n12,n13 *>,
                                <* n21,n22,n23 *>,
                                <* n31,n32,n33 *> *> &
  u2 in closed_inside_of_circle(0,0,1) holds n31 * u2.1 + n32 * u2.2 + n33 <> 0
  proof
    let h be Element of SubGroupK-isometry;
    let N be invertible Matrix of 3,F_Real;
    let n11,n12,n13,n21,n22,n23,n31,n32,n33 be Element of F_Real;
    let u2 be Element of TOP-REAL 2;
    assume that
A1: h = homography(N) and
A2: N = <* <* n11,n12,n13 *>, <* n21,n22,n23 *>, <* n31,n32,n33 *> *> and
A3: u2 in closed_inside_of_circle(0,0,1);
    u2 in inside_of_circle(0,0,1) \/ circle(0,0,1) by A3,TOPREAL9:55;
    then per cases by XBOOLE_0:def 3;
    suppose
      u2 in inside_of_circle(0,0,1);
      then reconsider uic = u2 as Element of inside_of_circle(0,0,1);
      consider Q be Element of TOP-REAL 2 such that
A4:   Q = uic & REAL2_to_BK uic = Dir |[Q`1,Q`2,1]| by BKMODEL2:def 3;
      reconsider P = REAL2_to_BK uic as Element of BK_model;
      reconsider v = |[Q`1,Q`2,1]| as non zero Element of TOP-REAL 3;
A5:   v.1 = v`1 by EUCLID_5:def 1
         .= u2.1 by A4,EUCLID_5:2;
A6:   v.2 = v`2 by EUCLID_5:def 2
         .= u2.2 by A4,EUCLID_5:2;
      now
        thus P = Dir v by A4;
        thus v.3 = v`3 by EUCLID_5:def 3
                .= 1 by EUCLID_5:2;
      end;
      hence thesis by A5,A6,A1,A2,Th20;
    end;
    suppose
A7:   u2 in circle(0,0,1);
      then reconsider u2 as non zero Element of TOP-REAL 2 by Th37;
      reconsider P = REAL2_to_absolute u2 as Element of absolute;
      reconsider v = |[u2.1,u2.2,1]| as non zero Element of TOP-REAL 3;
A8:   v.1 = v`1 by EUCLID_5:def 1
         .= u2.1 by EUCLID_5:2;
A9:   v.2 = v`2 by EUCLID_5:def 2
         .= u2.2 by EUCLID_5:2;
      now
        thus P is Element of absolute;
        thus P = Dir v by A7,BKMODEL1:def 9;
        thus v.3 = v`3 by EUCLID_5:def 3
                .= 1 by EUCLID_5:2;
      end;
      hence thesis by A8,A9,A1,A2,Th22;
    end;
  end;

theorem Th39:
  for a,b,c,d,e,f,r being Real st
  (1 - r) * |[a,b,1]| + r * |[c,d,1]| = |[e,f,1]| holds
  (1 - r) * |[a,b]| + r * |[c,d]| = |[e,f]|
  proof
    let a,b,c,d,e,f,r be Real;
    assume (1 - r) * |[a,b,1]| + r * |[c,d,1]| = |[e,f,1]|;
    then |[e,f,1]|=|[(1 - r) * a,(1 - r) * b,(1 - r) * 1]| + r * |[c,d,1]|
      by EUCLID_5:8
                 .=|[(1 - r) * a,(1 - r) * b,(1 - r)]|
                     + |[r * c,r * d,r * 1]| by EUCLID_5:8
                 .=|[(1 - r) * a + r * c,(1 - r) * b + r * d,1 - r + r]|
                     by EUCLID_5:6;
    then e = (1 - r) * a + r * c & f = (1 - r) * b + r * d by FINSEQ_1:78;
    then |[e,f]| = |[ (1 - r) * a, (1 - r) * b ]| + |[ r * c,r * d]|
      by EUCLID:56
                .= (1 - r) * |[a,b]| + |[r * c,r * d]| by EUCLID:58
                .= (1 - r) * |[a,b]| + r * |[c,d]| by EUCLID:58;
    hence thesis;
  end;

theorem
  for P,Q,R,P9,Q9,R9 being POINT of BK-model-Plane
  for p,q,r,p9,q9,r9 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) &
  between P,Q,R & P = p & Q = q & R = r & p9 = homography(N).p &
  q9 = homography(N).q & r9 = homography(N).r &
  P9 = p9 & Q9 = q9 & R9 = r9 holds between P9,Q9,R9
  proof
    let P,Q,R,P9,Q9,R9 be POINT of BK-model-Plane;
    let p,q,r,p9,q9,r9 be Element of BK_model;
    let h be Element of SubGroupK-isometry;
    let N be invertible Matrix of 3,F_Real;
    assume that
A1: h = homography(N) and
A2: between P,Q,R and
A3: P = p and
A4: Q = q and
A5: R = r and
A6: p9 = homography(N).p and
A7: q9 = homography(N).q and
A8: r9 = homography(N).r and
A9: P9 = p9 and
A10: Q9 = q9 and
A11: R9 = r9;
    consider n11,n12,n13,n21,n22,n23,n31,n32,n33 be Element of F_Real such that
A12: N = <* <* n11,n12,n13 *>,
            <* n21,n22,n23 *>,
            <* n31,n32,n33 *> *> by PASCAL:3;
    consider u be non zero Element of TOP-REAL 3 such that
A13: Dir u = p & u.3 = 1 & BK_to_REAL2 p = |[u.1,u.2]| by BKMODEL2:def 2;
    consider v be non zero Element of TOP-REAL 3 such that
A14: Dir v = r & v.3 = 1 & BK_to_REAL2 r = |[v.1,v.2]| by BKMODEL2:def 2;
    consider w be non zero Element of TOP-REAL 3 such that
A15: Dir w = q & w.3 = 1 & BK_to_REAL2 q = |[w.1,w.2]| by BKMODEL2:def 2;
    reconsider nu1 = n11 * u.1 + n12 * u.2 + n13,
      nu2 = n21 * u.1 + n22 * u.2 + n23,
      nu3 = n31 * u.1 + n32 * u.2 + n33,
      nv1 = n11 * v.1 + n12 * v.2 + n13,
      nv2 = n21 * v.1 + n22 * v.2 + n23,
      nv3 = n31 * v.1 + n32 * v.2 + n33,
      nw1 = n11 * w.1 + n12 * w.2 + n13,
      nw2 = n21 * w.1 + n22 * w.2 + n23,
      nw3 = n31 * w.1 + n32 * w.2 + n33 as Real;
A16: BK_to_T2 P = BK_to_REAL2 p & Tn2TR BK_to_T2 P = BK_to_REAL2 p &
      BK_to_T2 Q = BK_to_REAL2 q & Tn2TR BK_to_T2 Q = BK_to_REAL2 q &
      BK_to_T2 R = BK_to_REAL2 r & Tn2TR BK_to_T2 R = BK_to_REAL2 r
      by A3,A4,A5,Th04;
    then Tn2TR BK_to_T2 Q in LSeg(Tn2TR BK_to_T2 P,Tn2TR BK_to_T2 R)
      by A2,A3,A4,A5,BKMODEL3:def 7;
    then consider l be Real such that
A17: 0 <= l & l <= 1 and
A18: Tn2TR BK_to_T2 Q = (1 - l) * Tn2TR BK_to_T2 P + l * Tn2TR BK_to_T2 R
      by RLTOPSP1:76;
    |[w.1,w.2]| = |[ (1 - l) * u.1, (1 - l) * u.2 ]| + l * |[v.1,v.2]|
      by A18,A16,A13,A14,A15,EUCLID:58
               .= |[ (1 - l) * u.1, (1 - l) * u.2 ]| + |[l * v.1,l * v.2]|
                 by EUCLID:58
               .= |[ (1 - l) * u.1 + l * v.1, (1 - l) * u.2 + l * v.2]|
                 by EUCLID:56;
    then
A19: w.1 = (1 - l) * u.1 + l * v.1 &
    w.2 = (1 - l) * u.2 + l * v.2 by FINSEQ_1:77;
    set r = (l * nv3) / ((1 - l) * nu3 + l * nv3);
    now
      thus w = |[w`1,w`2,w`3]| by EUCLID_5:3
            .= |[w.1,w`2,w`3]| by EUCLID_5:def 1
            .= |[w.1,w.2,w`3]| by EUCLID_5:def 2
            .= |[(1 - l) * u.1 + l * v.1, (1 - l) * u.2 + l * v.2,
              (1 - l) * 1 + l * 1]| by A15,A19,EUCLID_5:def 3
            .= |[(1 -l) * u.1,(1 - l) * u.2,(1 - l) * 1]| +
              |[ l * v.1,l * v.2, l * 1]| by EUCLID_5:6
            .= (1 - l) * |[u.1,u.2,1]| +
              |[ l * v.1,l * v.2, l * 1]| by EUCLID_5:8
            .= (1 - l) * |[u.1,u.2,1]| +
              l * |[v.1,v.2, 1]| by EUCLID_5:8
            .= (1 - l) * u + l * |[v.1,v.2,v.3]| by A13,A14,Th35
            .= (1 - l) * u + l * v by Th35;
      thus nu3 <> 0 by A1,A12,A13,Th20;
      thus nv3 <> 0 by A1,A12,A14,Th20;
      thus
A20:  nw3 <> 0 by A1,A12,A15,Th20;
      thus nw3 = (1 - l) * nu3 + l * nv3 by A19;
      thus (1 - l) * nu3 + l * nv3 <> 0 by A19,A20;
    end;
    then
A21: (1 - r) * |[nu1 / nu3,nu2 / nu3,1]| + r * |[nv1 / nv3,nv2 / nv3,1]|
      = |[nw1 / nw3,nw2 / nw3,1]| by Th34;
A22: 0 <= r <= 1
    proof
      now
        thus 0 <= l <= 1 by A17;
        thus 0 < nu3 * nv3
        proof
          reconsider u1 = |[u.1,u.2]|, v1 = |[v.1,v.2]| as
            Element of TOP-REAL 2;
A23:      u1.1 = u1`1 .= u.1 by EUCLID:52;
A24:      u1.2 = u1`2 .= u.2 by EUCLID:52;
A25:      v1.1 = v1`1 .= v.1 by EUCLID:52;
A26:      v1.2 = v1`2 .= v.2 by EUCLID:52;
          reconsider m31 = n31, m32 = n32, m33 = n33 as Element of F_Real;
          u1 in inside_of_circle(0,0,1) &
            v1 in inside_of_circle(0,0,1) &
            for w1 be Element of TOP-REAL 2 st
              w1 in inside_of_circle(0,0,1) holds
              m31 * w1.1 + m32 * w1.2 + m33 <> 0 by A13,A14,A1,A12,Th36;
          hence thesis by A23,A24,A25,A26,Th29;
        end;
      end;
      hence thesis by Th31;
    end;
A27: BK_to_T2 P9 = BK_to_REAL2 p9 &
      Tn2TR BK_to_T2 P9 = BK_to_REAL2 p9 &
      BK_to_T2 Q9 = BK_to_REAL2 q9 &
      Tn2TR BK_to_T2 Q9 = BK_to_REAL2 q9 &
      BK_to_T2 R9 = BK_to_REAL2 r9 &
      Tn2TR BK_to_T2 R9 = BK_to_REAL2 r9
      by A9,A10,A11,Th04;
    now
      thus 0 <= r <= 1 by A22;
      thus Tn2TR BK_to_T2 Q9 = (1 - r) * Tn2TR BK_to_T2 P9
                                + r * Tn2TR BK_to_T2 R9
      proof
        reconsider u2 = |[nu1/nu3,nu2/nu3,1]|
          as non zero Element of TOP-REAL 3;
        consider u3 be non zero Element of TOP-REAL 3 such that
A28:    Dir u3 = p9 & u3.3 = 1 & BK_to_REAL2 p9 = |[u3.1,u3.2]|
          by BKMODEL2:def 2;
        now
          thus Dir u3 = Dir u2 by A28,A6,A1,A12,A13,Th23;
          thus u2.3 = u2`3 by EUCLID_5:def 3
                   .= 1 by EUCLID_5:2;
          hence u2.3 = u3.3 by A28;
        end;
        then u2 = u3 by BKMODEL1:43;
        then
A29:    BK_to_REAL2 p9 = |[u2`1,u2.2]| by A28,EUCLID_5:def 1
                      .= |[u2`1,u2`2]| by EUCLID_5:def 2
                      .= |[nu1/nu3,u2`2]| by EUCLID_5:2
                      .= |[nu1/nu3,nu2/nu3]| by EUCLID_5:2;
        reconsider v2 = |[nv1/nv3,nv2/nv3,1]| as
          non zero Element of TOP-REAL 3;
        consider v3 be non zero Element of TOP-REAL 3 such that
A30:    Dir v3 = r9 & v3.3 = 1 & BK_to_REAL2 r9 = |[v3.1,v3.2]|
          by BKMODEL2:def 2;
        now
          thus Dir v3 = Dir v2 by A30,A1,A12,A14,Th23,A8;
          thus v2.3 = v2`3 by EUCLID_5:def 3
                   .= 1 by EUCLID_5:2;
          hence v2.3 = v3.3 by A30;
        end;
        then v2 = v3 by BKMODEL1:43;
        then
A31:    BK_to_REAL2 r9 = |[v2`1,v2.2]| by A30,EUCLID_5:def 1
                      .= |[v2`1,v2`2]| by EUCLID_5:def 2
                      .= |[nv1/nv3,v2`2]| by EUCLID_5:2
                      .= |[nv1/nv3,nv2/nv3]| by EUCLID_5:2;
        reconsider w2 = |[nw1/nw3,nw2/nw3,1]|
          as non zero Element of TOP-REAL 3;
        consider w3 be non zero Element of TOP-REAL 3 such that
A32:    Dir w3 = q9 & w3.3 = 1 & BK_to_REAL2 q9 = |[w3.1,w3.2]|
          by BKMODEL2:def 2;
        now
          thus Dir w3 = Dir w2 by A32,A1,A12,A15,Th23,A7;
          thus w2.3 = w2`3 by EUCLID_5:def 3
                   .= 1 by EUCLID_5:2;
          hence w2.3 = w3.3 by A32;
        end;
        then w2 = w3 by BKMODEL1:43;
        then BK_to_REAL2 q9 = |[w2`1,w2.2]| by A32,EUCLID_5:def 1
                           .= |[w2`1,w2`2]| by EUCLID_5:def 2
                           .= |[nw1/nw3,w2`2]| by EUCLID_5:2
                           .= |[nw1/nw3,nw2/nw3]| by EUCLID_5:2;
        hence thesis by A27,A29,A31,Th39,A21;
      end;
    end;
    then Tn2TR BK_to_T2 Q9 in {(1 - r) * Tn2TR BK_to_T2 P9
      + r * Tn2TR BK_to_T2 R9 where r is Real:0 <= r & r <= 1};
    then Tn2TR BK_to_T2 Q9 in LSeg(Tn2TR BK_to_T2 P9,Tn2TR BK_to_T2 R9)
      by RLTOPSP1:def 2;
    hence thesis by A27,A9,A10,A11,BKMODEL3:def 7;
  end;

definition
  let P be Point of ProjectiveSpace TOP-REAL 3;
  attr P is point_at_infty means
:Def04:
  ex u being non zero Element of TOP-REAL 3 st
  P = Dir u & u`3 = 0;
end;

theorem Th40:
  for P being Point of ProjectiveSpace TOP-REAL 3 st
  ex u being non zero Element of TOP-REAL 3 st
  P = Dir u & u`3 <> 0 holds P is non point_at_infty
  proof
    let P be Point of ProjectiveSpace TOP-REAL 3;
    given u be non zero Element of TOP-REAL 3 such that
A1: P = Dir u and
A2: u`3 <> 0;
    now
      let v be non zero Element of TOP-REAL 3;
      assume P = Dir v;
      then are_Prop u,v by A1,ANPROJ_1:22;
      then consider a be Real such that
A3:   a <> 0 and
A4:   v = a * u by ANPROJ_1:1;
      v`3 = a * u`3 by A4,EUCLID_5:9;
      hence v`3 <> 0 by A2,A3;
    end;
    hence thesis;
  end;

registration
  cluster point_at_infty for Point of ProjectiveSpace TOP-REAL 3;
  existence
  proof
    reconsider u = |[1,0,0]| as non zero Element of TOP-REAL 3;
    reconsider P = Dir u as Point of ProjectiveSpace TOP-REAL 3 by ANPROJ_1:26;
    take P;
    u`3 = 0 by EUCLID_5:2;
    hence thesis;
  end;
  cluster non point_at_infty for Point of ProjectiveSpace TOP-REAL 3;
  correctness
  proof
    reconsider u = |[0,0,1]| as non zero Element of TOP-REAL 3;
    reconsider P = Dir u as Point of ProjectiveSpace TOP-REAL 3 by ANPROJ_1:26;
    take P;
    now
      let v be non zero Element of TOP-REAL 3;
      assume P = Dir v;
      then are_Prop u,v by ANPROJ_1:22;
      then consider a be Real such that
A1:   a <> 0 and
A2:   v = a * u by ANPROJ_1:1;
      v`3 = a * u`3 by A2,EUCLID_5:9
         .= a * 1 by EUCLID_5:2
         .= a;
      hence v`3 <> 0 by A1;
    end;
    hence thesis;
  end;
end;

definition
  let P being non point_at_infty Point of ProjectiveSpace TOP-REAL 3;
  func RP3_to_REAL2 P -> Element of REAL 2 means
:Def05:
  ex u being non zero Element of TOP-REAL 3 st P = Dir u & u`3 = 1 &
  it = |[u`1,u`2]|;
  existence
  proof
    consider u be Element of TOP-REAL 3 such that
A1: u is not zero and
A2: P = Dir u by ANPROJ_1:26;
A3: P is non point_at_infty;
    reconsider v = |[u`1/u`3,u`2/u`3,1]| as non zero Element of TOP-REAL 3;
    u`3 * v = |[ u`3 * (u`1/u`3),u`3 * (u`2/u`3),u`3*1]| by EUCLID_5:8
           .= |[u`1,u`3*(u`2/u`3),u`3]| by A1,A2,A3,XCMPLX_1:87
           .= |[u`1,u`2,u`3]| by A1,A2,A3,XCMPLX_1:87
           .= u by EUCLID_5:3;
    then are_Prop u,v by A1,A2,A3,ANPROJ_1:1;
    then
A4: P = Dir v by A2,A1,ANPROJ_1:22;
A5: v`3 = 1 by EUCLID_5:2;
    |[v`1,v`2]| is Element of REAL 2 by EUCLID:22;
    hence thesis by A4,A5;
  end;
  uniqueness
  proof
    let u,v be Element of REAL 2 such that
A6: ex w be non zero Element of TOP-REAL 3 st P = Dir w & w`3 = 1 &
      u = |[w`1,w`2]| and
A7: ex w be non zero Element of TOP-REAL 3 st P = Dir w & w`3 = 1 &
      v = |[w`1,w`2]|;
    consider w1 be non zero Element of TOP-REAL 3 such that
A8: P = Dir w1 & w1`3 = 1 & u = |[w1`1,w1`2]| by A6;
    consider w2 be non zero Element of TOP-REAL 3 such that
A9: P = Dir w2 & w2`3 = 1 & v = |[w2`1,w2`2]| by A7;
    are_Prop w1,w2 by A8,A9,ANPROJ_1:22;
    then consider a be Real such that
    a <> 0 and
A10: w1 = a * w2 by ANPROJ_1:1;
    1 = a * w2`3 by A8,A10,EUCLID_5:9
     .= a by A9;
    then w1 = |[ 1 * w2`1,1 * w2`2,1 * w2`3]| by A10,EUCLID_5:7
           .= w2 by EUCLID_5:3;
    hence thesis by A8,A9;
  end;
end;

definition
  let P be non point_at_infty Point of ProjectiveSpace TOP-REAL 3;
  func RP3_to_T2 P -> Point of TarskiEuclid2Space equals
    RP3_to_REAL2 P;
  coherence
  proof
    the MetrStruct of TarskiEuclid2Space = the MetrStruct of Euclid 2
      by GTARSKI1:def 13;
    hence thesis;
  end;
end;

theorem Th41:
  for P,Q,R,P9,Q9,R9 being
    non point_at_infty Element of ProjectiveSpace TOP-REAL 3
  for h being Element of SubGroupK-isometry
  for N being invertible Matrix of 3,F_Real st h = homography(N) &
  P in BK_model & Q in BK_model & R in absolute &
  P9 = homography(N).P & Q9 = homography(N).Q & R9 = homography(N).R &
  between RP3_to_T2 P,RP3_to_T2 Q,RP3_to_T2 R holds
  between RP3_to_T2 P9,RP3_to_T2 Q9,RP3_to_T2 R9
  proof
    let P,Q,R,P9,Q9,R9 be
      non point_at_infty Element of ProjectiveSpace TOP-REAL 3;
    let h be Element of SubGroupK-isometry;
    let N be invertible Matrix of 3,F_Real;
    assume that
A1: h = homography(N) and
A2: P in BK_model and
A3: Q in BK_model and
A4: R in absolute and
A5: P9 = homography(N).P and
A6: Q9 = homography(N).Q and
A7: R9 = homography(N).R and
A8: between RP3_to_T2 P,RP3_to_T2 Q,RP3_to_T2 R;
    consider n11,n12,n13,n21,n22,n23,n31,n32,n33 be Element of F_Real such that
A9: N = <* <* n11,n12,n13 *>,
           <* n21,n22,n23 *>,
           <* n31,n32,n33 *> *> by PASCAL:3;
    consider u be non zero Element of TOP-REAL 3 such that
A10: P = Dir u & u`3 = 1 & RP3_to_REAL2 P = |[u`1,u`2]| by Def05;
A11: |[u`1,u`2]| = |[u.1,u`2]| by EUCLID_5:def 1
                .= |[u.1,u.2]| by EUCLID_5:def 2;
    then
A12: P = Dir u & u.3 = 1 & RP3_to_REAL2 P = |[u.1,u.2]| by A10,EUCLID_5:def 3;
    consider v be non zero Element of TOP-REAL 3 such that
A13: R = Dir v & v`3 = 1 & RP3_to_REAL2 R = |[v`1,v`2]| by Def05;
A14: |[v`1,v`2]| = |[v.1,v`2]| by EUCLID_5:def 1
                .= |[v.1,v.2]| by EUCLID_5:def 2;
    then
A15: R = Dir v & v.3 = 1 & RP3_to_REAL2 R = |[v.1,v.2]| by A13,EUCLID_5:def 3;
    consider w be non zero Element of TOP-REAL 3 such that
A16: Q = Dir w & w`3 = 1 & RP3_to_REAL2 Q = |[w`1,w`2]| by Def05;
A17: |[w`1,w`2]| = |[w.1,w`2]| by EUCLID_5:def 1
                .= |[w.1,w.2]| by EUCLID_5:def 2;
    then
A18: Q = Dir w & w.3 = 1 & RP3_to_REAL2 Q = |[w.1,w.2]| by A16,EUCLID_5:def 3;
    reconsider nu1 = n11 * u.1 + n12 * u.2 + n13,
      nu2 = n21 * u.1 + n22 * u.2 + n23, nu3 = n31 * u.1 + n32 * u.2 + n33,
      nv1 = n11 * v.1 + n12 * v.2 + n13, nv2 = n21 * v.1 + n22 * v.2 + n23,
      nv3 = n31 * v.1 + n32 * v.2 + n33, nw1 = n11 * w.1 + n12 * w.2 + n13,
      nw2 = n21 * w.1 + n22 * w.2 + n23, nw3 = n31 * w.1 + n32 * w.2 + n33
      as Real;
    Tn2TR RP3_to_T2 Q in LSeg(Tn2TR RP3_to_T2 P,Tn2TR RP3_to_T2 R)
      by A8,GTARSKI2:20;
    then consider l be Real such that
A19: 0 <= l & l <= 1 and
A20: Tn2TR RP3_to_T2 Q = (1 - l) * Tn2TR RP3_to_T2 P + l * Tn2TR RP3_to_T2 R
      by RLTOPSP1:76;
    |[w.1,w.2]| = |[ (1 - l) * u.1, (1 - l) * u.2 ]| + l * |[v.1,v.2]|
      by A20,A11,A10,A14,A17,A16,A13,EUCLID:58
               .= |[ (1 - l) * u.1, (1 - l) * u.2 ]| + |[l * v.1,l * v.2]|
                 by EUCLID:58
               .= |[ (1 - l) * u.1 + l * v.1, (1 - l) * u.2 + l * v.2]|
                 by EUCLID:56;
    then
A21: w.1 = (1 - l) * u.1 + l * v.1 & w.2 = (1 - l) * u.2 + l * v.2
      by FINSEQ_1:77;
    set r = (l * nv3) / ((1 - l) * nu3 + l * nv3);
    now
      thus w = |[w`1,w`2,w`3]| by EUCLID_5:3
            .= |[w.1,w`2,w`3]| by EUCLID_5:def 1
            .= |[(1 - l) * u.1 + l * v.1, (1 - l) * u.2 + l * v.2,
              (1 - l) * 1 + l * 1]| by A16,A21,EUCLID_5:def 2
            .= |[(1 -l) * u.1,(1 - l) * u.2,(1 - l) * 1]| +
              |[ l * v.1,l * v.2, l * 1]| by EUCLID_5:6
            .= (1 - l) * |[u.1,u.2,1]| +
              |[ l * v.1,l * v.2, l * 1]| by EUCLID_5:8
            .= (1 - l) * |[u.1,u.2,1]| +
              l * |[v.1,v.2, 1]| by EUCLID_5:8
            .= (1 - l) * u + l * |[v.1,v.2,v.3]| by A12,A15,Th35
            .= (1 - l) * u + l * v by Th35;
      thus nu3 <> 0 by A1,A2,A9,A12,Th20;
      thus nv3 <> 0 by A1,A4,A9,A15,Th22;
      thus
A22:  nw3 <> 0 by A3,A1,A9,A18,Th20;
      thus nw3 = (1 - l) * nu3 + l * nv3 by A21;
      thus (1 - l) * nu3 + l * nv3 <> 0 by A22,A21;
    end;
    then
A23: (1 - r) * |[nu1 / nu3,nu2 / nu3,1]|
      + r * |[nv1 / nv3,nv2 / nv3,1]|
      = |[nw1 / nw3,nw2 / nw3,1]| by Th34;
A24: 0 <= r <= 1
    proof
      now
        thus 0 <= l <= 1 by A19;
        thus 0 < nu3 * nv3
        proof
          reconsider u1 = |[u.1,u.2]|, v1 = |[v.1,v.2]| as
            Element of TOP-REAL 2;
A25:      u1.1 = u1`1 .= u.1 by EUCLID:52;
A26:      u1.2 = u1`2 .= u.2 by EUCLID:52;
A27:      v1.1 = v1`1 .= v.1 by EUCLID:52;
A28:      v1.2 = v1`2 .= v.2 by EUCLID:52;
          reconsider m31 = n31, m32 = n32, m33 = n33 as Element of F_Real;
          now
            reconsider PP = P as Element of BK_model by A2;
            consider u3 be non zero Element of TOP-REAL 3 such that
A29:        Dir u3 = PP & u3.3 = 1 & BK_to_REAL2 PP = |[u3.1,u3.2]|
              by BKMODEL2:def 2;
            u3 = u by A12,A29,Th16;
            hence u1 in inside_of_circle(0,0,1) by A29;
            thus v1 in circle(0,0,1) by A4,A15,BKMODEL1:84;
            thus for w1 be Element of TOP-REAL 2 st
              w1 in closed_inside_of_circle(0,0,1) holds
              m31 * w1.1 + m32 * w1.2 + m33 <> 0 by A1,A9,Th38;
          end;
          hence thesis by A25,A26,A27,A28,Th30;
        end;
      end;
      hence thesis by Th31;
    end;
    now
      thus 0 <= r <= 1 by A24;
      thus Tn2TR RP3_to_T2 Q9 = (1 - r) * Tn2TR RP3_to_T2 P9
                                + r * Tn2TR RP3_to_T2 R9
      proof
        reconsider u2 = |[nu1/nu3,nu2/nu3,1]| as
          non zero Element of TOP-REAL 3;
        reconsider PP9 = P9 as
          non point_at_infty Point of ProjectiveSpace TOP-REAL 3;
        consider u3 be non zero Element of TOP-REAL 3 such that
A30:    PP9 = Dir u3 & u3`3 = 1 & RP3_to_REAL2 PP9 = |[u3`1,u3`2]| by Def05;
        now
          thus Dir u3 = Dir u2 by A1,A2,A9,A12,Th23,A5,A30;
          thus u2.3 = u2`3 by EUCLID_5:def 3
                   .= 1 by EUCLID_5:2;
          hence u2.3 = u3.3 by A30,EUCLID_5:def 3;
        end;
        then u2 = u3 by BKMODEL1:43;
        then
A31:    RP3_to_REAL2 P9 = |[nu1/nu3,u2`2]| by A30,EUCLID_5:2
                       .= |[nu1/nu3,nu2/nu3]| by EUCLID_5:2;
        reconsider v2 = |[nv1/nv3,nv2/nv3,1]| as
          non zero Element of TOP-REAL 3;
        consider v3 be non zero Element of TOP-REAL 3 such that
A32:    Dir v3= R9 & v3`3 = 1 & RP3_to_REAL2 R9 = |[v3`1,v3`2]| by Def05;
        now
          thus Dir v3 = Dir v2 by A15,A1,A4,A9,Th24,A7,A32;
          thus v2.3 = v2`3 by EUCLID_5:def 3
                   .= 1 by EUCLID_5:2;
          hence v2.3 = v3.3 by A32,EUCLID_5:def 3;
        end;
        then v2 = v3 by BKMODEL1:43;
        then
A33:    RP3_to_REAL2 R9 = |[nv1/nv3,v2`2]| by A32,EUCLID_5:2
                       .= |[nv1/nv3,nv2/nv3]| by EUCLID_5:2;
        reconsider w2 = |[nw1/nw3,nw2/nw3,1]| as
          non zero Element of TOP-REAL 3;
        consider w3 be non zero Element of TOP-REAL 3 such that
A34:    Dir w3= Q9 & w3`3 = 1 & RP3_to_REAL2 Q9 = |[w3`1,w3`2]| by Def05;
        now
          thus Dir w3 = Dir w2 by A3,A1,A9,A18,Th23,A6,A34;
          thus w2.3 = w2`3 by EUCLID_5:def 3
                   .= 1 by EUCLID_5:2;
          hence w2.3 = w3.3 by A34,EUCLID_5:def 3;
        end;
        then w2 = w3 by BKMODEL1:43;
        then
A35:    RP3_to_REAL2 Q9 = |[nw1/nw3,w2`2]| by A34,EUCLID_5:2
                       .= |[nw1/nw3,nw2/nw3]| by EUCLID_5:2;
        RP3_to_REAL2 Q9 = (1 - r) * RP3_to_REAL2 P9 + r * RP3_to_REAL2 R9
        proof
          reconsider a = nu1/nu3, b = nu2/nu3, c = nv1/nv3, d = nv2/nv3,
          e = nw1/nw3, f = nw2/nw3 as Real;
          (1-r) * |[a,b]| + r * |[c,d]| = |[e,f]| by Th39,A23;
          hence thesis by A31,A33,A35;
        end;
        hence thesis;
      end;
    end;
    then Tn2TR RP3_to_T2 Q9 in {(1 - r) * Tn2TR RP3_to_T2 P9
      + r * Tn2TR RP3_to_T2 R9 where r is Real:0 <= r & r <= 1};
    then Tn2TR RP3_to_T2 Q9 in LSeg(Tn2TR RP3_to_T2 P9,Tn2TR RP3_to_T2 R9)
      by RLTOPSP1:def 2;
    hence thesis by GTARSKI2:20;
  end;

theorem Th42:
  for a,b,c being Real
  for u,v,w being Element of TOP-REAL 3
  st a <> 0 & a + b + c = 0 &
  a * u + b * v + c * w = 0.TOP-REAL 3 holds
  u in Line(v,w)
  proof
    let a,b,c be Real;
    let u,v,w be Element of TOP-REAL 3;
    assume that
A1: a <> 0 and
A2: a + b + c = 0 and
A3: a * u + b * v + c * w = 0.TOP-REAL 3;
A4: u = ((-b)/a) * v + ((-c)/a) * w by A1,A3,ANPROJ_8:12;
    reconsider r = (-c) / a as Real;
    (1 - r) = a / a + c / a by A1,XCMPLX_1:60
           .= (a + c) / a
           .= (-b) / a by A2;
    then u in the set of all (1 - r) * v + r * w where r is Real by A4;
    hence thesis by RLTOPSP1:def 14;
  end;

theorem Th43:
  for P,Q,R being non point_at_infty Point 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 = 1 & v`3 = 1 & w`3 = 1 holds
  P,Q,R are_collinear iff u,v,w are_collinear
  proof
    let P,Q,R be non point_at_infty Point of ProjectiveSpace TOP-REAL 3;
    let u,v,w be non zero Element of TOP-REAL 3;
    assume that
A1: P = Dir u & Q = Dir v & R = Dir w and
A2: u`3 = 1 & v`3 = 1 & w`3 = 1;
    reconsider i = 3 as Nat;
    hereby
      assume P,Q,R are_collinear;
      then consider u9,v9,w9 be Element of TOP-REAL 3 such that
A3:   P = Dir u9 & Q = Dir v9 & R = Dir w9 &
      u9 is not zero & v9 is not zero & w9 is not zero and
A4:   ex a,b,c be Real st a*u9+b*v9+c*w9=0.TOP-REAL 3 &
      (a <> 0 or b <> 0 or c <> 0) by ANPROJ_8:11;
A5:   |{u9,v9,w9}| = 0 by A4,ANPROJ_8:41;
      are_Prop u,u9 by A1,A3,ANPROJ_1:22;
      then consider a be Real such that
A6:   a <> 0 and
A7:   u9 = a * u by ANPROJ_1:1;
      are_Prop v,v9 by A1,A3,ANPROJ_1:22;
      then consider b be Real such that
A8:   b <> 0 and
A9:   v9 = b * v by ANPROJ_1:1;
      are_Prop w,w9 by A1,A3,ANPROJ_1:22;
      then consider c be Real such that
A10:  c <> 0 and
A11:  w9 = c * w by ANPROJ_1:1;
      reconsider d = a * (b * c) as non zero Real by A6,A8,A10;
      0 = a * |{u,b * v,c * w}| by ANPROJ_8:31,A5,A7,A9,A11
       .= a * (b * |{u,v,c * w}|) by ANPROJ_8:32
       .= a * (b * (c * |{u,v,w}|)) by ANPROJ_8:33
       .= d * |{u,v,w}|;
      then |{u,v,w}| = 0;
      then consider  a,b,c be Real such that
A12:  a * u + b * v + c * w = 0.TOP-REAL 3 and
A13:  a <> 0 or b <> 0 or c <> 0 by ANPROJ_8:43,ANPROJ_1:def 2;
      reconsider aubv = a * u + b * v,cw = c * w,au = a * u,
        bv = b * v as Element of TOP-REAL 3;
A14:  cw is Element of REAL 3 by EUCLID:22;
A15:  aubv is Element of REAL 3 by EUCLID:22;
      au is Element of REAL 3 & bv is Element of REAL 3 by EUCLID:22;
      then
A16:  aubv.3 = au.3 + bv.3 by RVSUM_1:11
            .= a * u.3 + bv.3 by RVSUM_1:44
            .= a * u.3 + b * v.3 by RVSUM_1:44;
A17:  cw.3 = c * w.3 by RVSUM_1:44;
      |[(aubv + cw)`1,(aubv + cw)`2,(aubv+cw)`3]| = |[0,0,0]|
        by A12,EUCLID_5:3,4;
      then
A18:  0 = (aubv + cw)`3 by FINSEQ_1:78
       .= (aubv + cw).3 by EUCLID_5:def 3
       .= aubv.3+cw.3 by A14,A15,RVSUM_1:11
       .= a * u`3 + b * v.3 + c * w.3 by A16,A17,EUCLID_5:def 3
       .= a * u`3 + b * v`3 + c * w.3 by EUCLID_5:def 3
       .= a * u`3 + b * v`3 + c * w`3 by EUCLID_5:def 3
       .= a + b + c by A2;
      thus u,v,w are_collinear
      proof
        per cases by A13;
        suppose
A19:      a <> 0;
          reconsider L = Line(v,w) as line of TOP-REAL 3;
          u in L & v in L & w in L by A18,A12,Th42,A19,RLTOPSP1:72;
          hence thesis by RLTOPSP1:def 16;
        end;
        suppose
A20:      b <> 0;
A21:      b * v + c * w + a * u = 0.TOP-REAL 3 by A12,RVSUM_1:15;
A22:      b + c + a = 0 by A18;
          reconsider L = Line(w,u) as line of TOP-REAL 3;
          v in L & w in L & u in L by A22,A20,A21,Th42,RLTOPSP1:72;
          hence thesis by RLTOPSP1:def 16;
        end;
        suppose
A23:      c <> 0;
A24:      c * w + a * u + b * v = 0.TOP-REAL 3 by A12,RVSUM_1:15;
A25:      c + a + b = 0 by A18;
          reconsider L = Line(u,v) as line of TOP-REAL 3;
          w in L & u in L & v in L by A25,A23,A24,Th42,RLTOPSP1:72;
          hence thesis by RLTOPSP1:def 16;
        end;
      end;
    end;
    assume u,v,w are_collinear;
    then per cases by TOPREAL9:67;
    suppose u in LSeg(v,w);
      then consider r be Real such that 0 <= r & r <= 1 and
A26:  u = (1 - r) * v + r * w by RLTOPSP1:76;
      reconsider a = 1,b = r - 1,c = -r as Real;
      1 * u + (r - 1) * v + (-r) * w = 0.TOP-REAL 3
      proof
        reconsider vw = v + w as Element of REAL 3 by EUCLID:22;
        1 * u = (1 - r) * v + r * w by A26,RVSUM_1:52;
        then 1 * u + (r - 1) * v + (-r) * w
          = r * w + ((1 - r) * v + (r - 1) * v) + (-r) * w by RVSUM_1:15
         .= r * w + ((1 - r) + (r - 1)) * v + (-r) * w by RVSUM_1:50
         .= 0 * v + (r * w + (-r) * w) by RVSUM_1:15
         .= 0 * v + (r + (-r)) * w by RVSUM_1:50
         .= 0 * vw by RVSUM_1:51
         .= i|->0 by RVSUM_1:53
         .= 0.TOP-REAL 3 by EUCLID_5:4,FINSEQ_2:62;
        hence thesis;
      end;
      hence thesis by A1,ANPROJ_8:11;
    end;
    suppose v in LSeg(w,u);
      then consider r be Real such that 0 <= r & r <= 1 and
A27:  v = (1 - r) * w + r * u by RLTOPSP1:76;
      reconsider a = -r,b = 1,c = r - 1 as Real;
      (-r) * u + 1 * v + (r - 1) * w = 0.TOP-REAL 3
      proof
        reconsider uw = u + w as Element of REAL 3 by EUCLID:22;
        1 * v = (1 - r) * w + r * u by A27,RVSUM_1:52;
        then (-r) * u + 1 * v + (r - 1) * w
          = (-r) * u + r * u + (1 - r) * w + (r - 1) * w by RVSUM_1:15
         .= ((-r) + r) * u + (1 - r) * w + (r - 1) * w by RVSUM_1:50
         .= 0 * u + ((1 - r) * w + (r - 1) * w) by RVSUM_1:15
         .= 0 * u + (((1 - r) + (r - 1)) * w) by RVSUM_1:50
         .= 0 * uw by RVSUM_1:51
         .= i|->0 by RVSUM_1:53
         .= 0.TOP-REAL 3 by FINSEQ_2:62,EUCLID_5:4;
        hence thesis;
      end;
      hence thesis by A1,ANPROJ_8:11;
    end;
    suppose w in LSeg(u,v);
      then consider r be Real such that 0 <= r & r <= 1 and
A28:  w = (1 - r) * u + r * v by RLTOPSP1:76;
      reconsider a = r - 1,b = -r,c = 1 as Real;
      (r - 1) * u + (-r) * v + 1 * w = 0.TOP-REAL 3
      proof
        reconsider vu = v + u as Element of REAL 3 by EUCLID:22;
        1 * w = (1 - r) * u + r * v by A28,RVSUM_1:52;
        then (r - 1) * u + (-r) * v + 1 * w
          = (r - 1) * u + ((-r) * v + (r * v + (1 - r) * u)) by RVSUM_1:15
         .= (r - 1) * u + ((-r) * v + r * v + (1 - r) * u) by RVSUM_1:15
         .= (r - 1) * u + (((-r) + r) * v + (1 - r) * u) by RVSUM_1:50
         .= 0 * v + ((r - 1) * u + (1 - r) * u) by RVSUM_1:15
         .= 0 * v + (((r - 1) + (1 - r)) * u) by RVSUM_1:50
         .= 0 * vu by RVSUM_1:51
         .= i|->0 by RVSUM_1:53
         .= 0.TOP-REAL 3 by FINSEQ_2:62,EUCLID_5:4;
        hence thesis;
      end;
      hence thesis by A1,ANPROJ_8:11;
    end;
  end;

theorem Th44:
  for u,v,w being Element of TOP-REAL 3 st u in LSeg(v,w) holds
  |[u`1,u`2]| in LSeg ( |[v`1,v`2]| , |[w`1,w`2]| )
  proof
    let u,v,w be Element of TOP-REAL 3;
    assume u in LSeg(v,w);
    then consider r be Real such that
A1: 0 <= r and
A2: r <= 1 and
A3: u = (1 - r) * v + r * w by RLTOPSP1:76;
    reconsider rv = (1 - r) * v,rw = r * w as Element of TOP-REAL 3;
    rv = |[ (1 - r) * v`1, (1 - r) * v`2, (1 - r) * v`3 ]| &
      rw = |[r * w`1,r * w`2, r * w`3]| by EUCLID_5:7;
    then |[ (1 - r) * v`1 + r * w`1,
      (1 - r) * v`2 + r * w`2,(1 - r) * v`3 + r * w`3 ]| = u by A3,EUCLID_5:6
                                                        .= |[u`1,u`2,u`3]|
                                                          by EUCLID_5:3;
    then
A4: u`1 = (1 - r) * v`1 + r * w`1 &
    u`2 = (1 - r) * v`2 + r  *w`2 by FINSEQ_1:78;
    reconsider u9 = |[u`1,u`2]|, v9 = |[v`1,v`2]|,
               w9 = |[w`1,w`2]| as Element of TOP-REAL 2;
A5: u9`1 = u`1 & u9`2 = u`2 & v9`1 = v`1 & v9`2 = v`2 & w9`1 = w`1 &
    w9`2 = w`2 by EUCLID:52;
    reconsider rv9 = (1 - r) * v9, rw9 = r * w9 as Element of TOP-REAL 2;
    rv9 = |[ (1 - r) * v9`1,(1 - r) * v9`2 ]| &
      rw9 = |[ r * w9`1, r * w9`2 ]| by EUCLID:57;
    then rv9 + rw9 = |[ u`1,u`2 ]| by A4,A5,EUCLID:56;
    then u9 in {(1-r)*v9+r*w9 where r is Real : 0 <= r & r <= 1} by A1,A2;
    hence thesis by RLTOPSP1:def 2;
  end;

theorem Th45:
  for u,v,w being Element of TOP-REAL 2 st u in LSeg(v,w) holds
  |[u`1,u`2,1]| in LSeg(|[v`1,v`2,1]|,|[w`1,w`2,1]|)
  proof
    let u,v,w be Element of TOP-REAL 2;
    assume u in LSeg(v,w);
    then consider r be Real such that
A1: 0 <= r and
A2: r <= 1 and
A3: u = (1 - r) * v + r * w by RLTOPSP1:76;
    reconsider u9 = |[u`1,u`2,1]|,
    v9 = |[v`1,v`2,1]|,
    w9 = |[w`1,w`2,1]| as Element of TOP-REAL 3;
    reconsider rv = (1 - r) * v,
    rw = r * w as Element of REAL 2 by EUCLID:22;
A4: rv.1 = (1 - r) * v.1 & rv.2 = (1 - r) * v.2 &
      rw.1 = r * w.1 & rw.2 = r * w.2 by RVSUM_1:44;
A5: u`2 = (1 - r) * v.2 + r * w.2 by A4,A3,RVSUM_1:11;
    reconsider rv9 = (1 - r) * v9,rw9 = r * w9 as Element of TOP-REAL 3;
    u9 = (1 - r) * v9 + r * w9
    proof
      u9 = |[(1 - r) * v.1 + r * w.1,
             (1 - r) * v.2 + r * w.2, (1 - r) * 1 + r * 1]|
             by A5,A3,A4,RVSUM_1:11
        .= |[(1 - r) * v.1,(1 - r) * v.2,(1 - r) * 1]|
             + |[r * w.1, r * w.2, r * 1]| by EUCLID_5:6
        .= (1 - r) * |[v.1,v.2,1]|
             + |[r * w.1, r * w.2, r * 1]| by EUCLID_5:8
        .= (1 - r) * |[v`1,v`2,1]|
             + r * |[w`1,w`2,1]| by EUCLID_5:8;
      hence thesis;
    end;
    then u9 in {(1 - r) * v9 + r * w9 where r is Real: 0 <= r & r <= 1}
      by A1,A2;
    hence thesis by RLTOPSP1:def 2;
  end;

theorem Th46:
  for P,Q,R being non point_at_infty Point of ProjectiveSpace TOP-REAL 3
  holds P,Q,R are_collinear iff Collinear RP3_to_T2 P,RP3_to_T2 Q,RP3_to_T2 R
  proof
    let P,Q,R be non point_at_infty Point of ProjectiveSpace TOP-REAL 3;
    reconsider p = RP3_to_T2 P,q = RP3_to_T2 Q,
    r = RP3_to_T2 R as POINT of TarskiEuclid2Space;
    consider u be non zero Element of TOP-REAL 3 such that
A1: P = Dir u & u`3 = 1 & RP3_to_REAL2 P = |[u`1,u`2]| by Def05;
    consider v be non zero Element of TOP-REAL 3 such that
A2: Q = Dir v & v`3 = 1 & RP3_to_REAL2 Q = |[v`1,v`2]| by Def05;
    consider w be non zero Element of TOP-REAL 3 such that
A3: R = Dir w & w`3 = 1 & RP3_to_REAL2 R = |[w`1,w`2]| by Def05;
    hereby
      assume
A4:   P,Q,R are_collinear;
      u,v,w are_collinear by A4,A1,A2,A3,Th43;
      then per cases by TOPREAL9:67;
      suppose u in LSeg(v,w);
        then Tn2TR p in LSeg ( Tn2TR q, Tn2TR r ) by A1,A2,A3,Th44;
        hence Collinear RP3_to_T2 P,RP3_to_T2 Q,RP3_to_T2 R by GTARSKI2:20;
      end;
      suppose v in LSeg(w,u);
        then Tn2TR q in LSeg ( Tn2TR r, Tn2TR p ) by A1,A2,A3,Th44;
        hence Collinear RP3_to_T2 P,RP3_to_T2 Q,RP3_to_T2 R by GTARSKI2:20;
      end;
      suppose w in LSeg(u,v);
        then Tn2TR r in LSeg ( Tn2TR p, Tn2TR q ) by A1,A2,A3,Th44;
        hence Collinear RP3_to_T2 P,RP3_to_T2 Q,RP3_to_T2 R by GTARSKI2:20;
      end;
    end;
    assume Collinear RP3_to_T2 P,RP3_to_T2 Q,RP3_to_T2 R;
    then
A5: Tn2TR q in LSeg( Tn2TR p, Tn2TR r) or
    Tn2TR r in LSeg( Tn2TR q, Tn2TR p) or
    Tn2TR p in LSeg( Tn2TR r, Tn2TR q) by GTARSKI2:20;
    reconsider u1 = Tn2TR p, v1 = Tn2TR q,
               w1 = Tn2TR r as Element of TOP-REAL 2;
    reconsider u9 = |[u1`1,u1`2,1]|,v9 = |[v1`1,v1`2,1]|,
               w9 = |[w1`1,w1`2,1]| as Element of TOP-REAL 3;
    now
      u1`1 = u`1 & u1`2 = u`2 & v1`1 = v`1 &
        v1`2 = v`2 & w1`1 = w`1 & w1`2 = w`2 by A1,A2,A3,EUCLID:52;
      hence Dir u9 = P & Dir v9 = Q & Dir w9 = R by A1,A2,A3,EUCLID_5:3;
      thus u9`3 = 1 & v9`3 = 1 & w9`3 = 1 by EUCLID_5:2;
      v9 in LSeg(u9,w9) or w9 in LSeg(v9,u9) or u9 in LSeg(w9,v9) by A5,Th45;
      hence u9,v9,w9 are_collinear by TOPREAL9:67;
    end;
    hence P,Q,R are_collinear by Th43;
  end;

theorem
  for u,v,w being Element of TOP-REAL 2 st u,v,w are_collinear holds
  |[u`1,u`2,1]|,|[v`1,v`2,1]|,|[w`1,w`2,1]| are_collinear
  proof
    let u,v,w be Element of TOP-REAL 2;
    assume
A1: u,v,w are_collinear;
    reconsider u1 = |[u`1,u`2,1]|, v1 = |[v`1,v`2,1]|,
               w1 = |[w`1,w`2,1]| as non zero Point of TOP-REAL 3;
    u in LSeg(v,w) or v in LSeg(w,u) or w in LSeg(u,v) by A1,TOPREAL9:67;
    then u1 in LSeg(v1,w1) or v1 in LSeg(w1,u1) or w1 in LSeg(u1,v1) by Th45;
    hence thesis by TOPREAL9:67;
  end;

theorem Th47:
  for P,Q,P1 being non point_at_infty Element of ProjectiveSpace TOP-REAL 3 st
  P in BK_model & Q in BK_model & P1 in absolute :::& P,Q,P1 are_collinear
    holds
  not between RP3_to_T2 Q,RP3_to_T2 P1,RP3_to_T2 P
  proof
    let P,Q,P1 be non point_at_infty Element of ProjectiveSpace TOP-REAL 3;
    assume
A1: P in BK_model & Q in BK_model & P1 in absolute;
    set P9 = RP3_to_T2 P, Q9 = RP3_to_T2 Q, P19 = RP3_to_T2 P1;
    assume
A2: between Q9,P19,P9;
    consider u be non zero Element of TOP-REAL 3 such that
A3: P = Dir u & u`3 = 1 & RP3_to_REAL2 P = |[u`1,u`2]| by Def05;
    consider v be non zero Element of TOP-REAL 3 such that
A4: Q = Dir v & v`3 = 1 & RP3_to_REAL2 Q = |[v`1,v`2]| by Def05;
    consider w1 be non zero Element of TOP-REAL 3 such that
A5: P1 = Dir w1 & w1`3 = 1 & RP3_to_REAL2 P1 = |[w1`1,w1`2]| by Def05;
A6: Tn2TR P19 in LSeg(Tn2TR Q9,Tn2TR P9) by A2,GTARSKI2:20;
    reconsider u9 = Tn2TR P19, v9 = Tn2TR Q9,
               w9 = Tn2TR P9 as Element of TOP-REAL 2;
    |[u9`1,u9`2]| = |[w1`1,w1`2]| by A5,EUCLID:53;
    then
A7: u9`1 = w1`1 & u9`2 = w1`2 by FINSEQ_1:77;
    |[v9`1,v9`2]| = |[v`1,v`2]| by A4,EUCLID:53;
    then
A8: v9`1 = v`1 & v9`2 = v`2 by FINSEQ_1:77;
    |[w9`1,w9`2]| = |[u`1,u`2]| by A3,EUCLID:53;
    then
A9: w9`1 = u`1 & w9`2 = u`2 by FINSEQ_1:77;
    reconsider pu = |[u9`1,u9`2,1]|, pv = |[v9`1,v9`2,1]|,
               pw = |[w9`1,w9`2,1]| as non zero Element of TOP-REAL 3;
    pu in LSeg(pw,pv) by A6,Th45;
    then consider r be Real such that
A10: 0 <= r & r <= 1 and
A11: pu = (1 - r) * pw + r * pv by RLTOPSP1:76;
    now
      thus Q = Dir pv by A4,A8,EUCLID_5:3;
      thus P = Dir pw by A3,A9,EUCLID_5:3;
      thus P1 = Dir pu by A5,A7,EUCLID_5:3;
      thus pv.3 = pv`3 by EUCLID_5:def 3
               .= 1 by EUCLID_5:2;
      thus pw.3 = pw`3 by EUCLID_5:def 3
               .= 1 by EUCLID_5:2;
      thus pu = r * pv + (1 - r) * pw by A11;
    end;
    then P1 is Element of BK_model by A1,A10,Th17;
    hence contradiction by A1,BKMODEL2:1,XBOOLE_0:def 4;
  end;

definition
  func Dir001 -> non point_at_infty Element of
    ProjectiveSpace TOP-REAL 3 equals
    Dir |[0,0,1]|;
  coherence
  proof
    reconsider P = Dir |[0,0,1]| as Element of ProjectiveSpace TOP-REAL 3
      by ANPROJ_1:26;
    for u be non zero Element of TOP-REAL 3 st P = Dir u holds u`3 <> 0
    proof
      let u be non zero Element of TOP-REAL 3;
      assume P = Dir u;
      then are_Prop u,|[0,0,1]| by ANPROJ_1:22;
      then consider a be Real such that
A1:   a <> 0 and
A2:   u = a * |[0,0,1]| by ANPROJ_1:1;
      u = |[ a * 0,a * 0,a * 1]| by A2,EUCLID_5:8;
      hence thesis by A1,EUCLID_5:2;
    end;
    hence thesis by Def04;
  end;
end;

definition
  func Dir101 -> non point_at_infty Element of
    ProjectiveSpace TOP-REAL 3 equals
    Dir |[1,0,1]|;
  coherence
  proof
    reconsider P = Dir |[1,0,1]| as Element of ProjectiveSpace TOP-REAL 3
      by ANPROJ_1:26;
    for u be non zero Element of TOP-REAL 3 st P = Dir u holds u`3 <> 0
    proof
      let u be non zero Element of TOP-REAL 3;
      assume P = Dir u;
      then are_Prop u,|[1,0,1]| by ANPROJ_1:22;
      then consider a be Real such that
A1:   a <> 0 and
A2:   u = a * |[1,0,1]| by ANPROJ_1:1;
      u = |[ a * 1,a * 0,a * 1]| by A2,EUCLID_5:8;
      hence thesis by A1,EUCLID_5:2;
    end;
    hence thesis by Def04;
  end;
end;

theorem
  for P,Q being non point_at_infty Element of ProjectiveSpace TOP-REAL 3 st
  P in absolute & Q in absolute
  holds RP3_to_T2 Dir001, RP3_to_T2 P equiv RP3_to_T2 Dir001,RP3_to_T2 Q
  proof
    let P,Q be non point_at_infty Element of ProjectiveSpace TOP-REAL 3;
    assume that
A1: P in absolute and
A2: Q in absolute;
    reconsider p = RP3_to_T2 P, q = RP3_to_T2 Q,
               r = RP3_to_T2 Dir001 as Element of TarskiEuclid2Space;
    consider u be non zero Element of TOP-REAL 3 such that
A3: P = Dir u & u`3 = 1 & RP3_to_REAL2 P = |[u`1,u`2]| by Def05;
    consider v be non zero Element of TOP-REAL 3 such that
A4: Q = Dir v & v`3 = 1 & RP3_to_REAL2 Q = |[v`1,v`2]| by Def05;
    consider w be non zero Element of TOP-REAL 3 such that
A5: Dir001 = Dir w & w`3 = 1 & RP3_to_REAL2 Dir001 = |[w`1,w`2]| by Def05;
    are_Prop |[0,0,1]|,w by A5,ANPROJ_1:22;
    then consider a be Real such that a <> 0 and
A6: w = a * |[0,0,1]| by ANPROJ_1:1;
    w = |[ a * 0, a * 0, a * 1]| by A6,EUCLID_5:8;
    then
A8: w`1 = 0 & w`2 = 0 by EUCLID_5:2;
    reconsider u1=u`1,u2=u`2,v1=v`1,v2=v`2,w1=w`1,w2=w`2 as Real;
    now
A9:   (Tn2TR RP3_to_T2 P)`1 = u`1 & (Tn2TR RP3_to_T2 P)`2 = u`2 &
        (Tn2TR RP3_to_T2 Q)`1 = v`1 & (Tn2TR RP3_to_T2 Q)`2 = v`2 &
        (Tn2TR RP3_to_T2 Dir001)`1 = w`1 & (Tn2TR RP3_to_T2 Dir001)`2 = w`2
        by A3,A4,A5,EUCLID:52;
      reconsider uP = |[u`1,u`2,1]| as non zero Element of TOP-REAL 3;
      now
        thus P in absolute by A1;
        thus P = Dir uP by A3,EUCLID_5:3;
        uP`3 = 1 by EUCLID_5:2;
        hence uP.3 = 1 by EUCLID_5:def 3;
      end;
      then |[uP.1,uP.2]| in circle(0,0,1) by BKMODEL1:84;
      then (uP.1)^2+(uP.2)^2 = 1 by BKMODEL1:13;
      then (uP`1)^2+(uP.2)^2 = 1 by EUCLID_5:def 1;
      then (uP`1)^2+(uP`2)^2 = 1 by EUCLID_5:def 2;
      then (u`1)^2+(uP`2)^2 = 1 by EUCLID_5:2;
      then
A10:  (u`1)^2+(u`2)^2 = 1 by EUCLID_5:2;
      reconsider vQ = |[v`1,v`2,1]| as non zero Element of TOP-REAL 3;
      now
        thus Q in absolute by A2;
        thus Q = Dir vQ by A4,EUCLID_5:3;
        vQ`3 = 1 by EUCLID_5:2;
        hence vQ.3 = 1 by EUCLID_5:def 3;
      end;
      then |[vQ.1,vQ.2]| in circle(0,0,1) by BKMODEL1:84;
      then (vQ.1)^2+(vQ.2)^2 = 1 by BKMODEL1:13;
      then (vQ`1)^2+(vQ.2)^2 = 1 by EUCLID_5:def 1;
      then (vQ`1)^2+(vQ`2)^2 = 1 by EUCLID_5:def 2;
      then (v`1)^2+(vQ`2)^2 = 1 by EUCLID_5:2;
      then
A11:  (v`1)^2+(v`2)^2 = 1 by EUCLID_5:2;
      now
        thus dist(RP3_to_T2 Dir001,RP3_to_T2 P)
          = sqrt((( 0 )-(u`1))^2+(( 0 )-(u`2))^2) by A9,A8,GTARSKI2:16
         .= sqrt ((u`1)^2+(-u`2)^2) by SQUARE_1:3
         .= 1 by A10,SQUARE_1:3,18;
        thus dist(RP3_to_T2 Dir001,RP3_to_T2 Q)
          = sqrt(((w`1)-(v`1))^2+((w`2)-(v`2))^2) by A9,GTARSKI2:16
         .= sqrt ((v`1)^2+(-v`2)^2) by A8,SQUARE_1:3
         .= 1 by A11,SQUARE_1:3,18;
      end;
      hence dist(RP3_to_T2 Dir001,RP3_to_T2 P)
        = dist(RP3_to_T2 Dir001,RP3_to_T2 Q);
      thus dist(RP3_to_T2 Dir001,RP3_to_T2 P)
        = |. Tn2TR RP3_to_T2 Dir001 - Tn2TR RP3_to_T2 P .| by GTARSKI2:17;
      thus dist(RP3_to_T2 Dir001,RP3_to_T2 Q)
        = |. Tn2TR RP3_to_T2 Dir001 - Tn2TR RP3_to_T2 Q .| by GTARSKI2:17;
    end;
    hence thesis by GTARSKI2:18;
  end;

theorem Th48:
  for P,Q,R being non point_at_infty Element of ProjectiveSpace TOP-REAL 3
  for u,v,w being non zero Element of TOP-REAL 3 st
  P in absolute & Q in absolute & P <> Q & P = Dir u & Q = Dir v & R = Dir w &
  u`3 = 1 & v`3 = 1 & w = |[ (u`1 + v`1) / 2,(u`2 + v`2) / 2,1]| holds
  R in BK_model
  proof
    let P,Q,R be non point_at_infty Element of ProjectiveSpace TOP-REAL 3;
    let u,v,w be non zero Element of TOP-REAL 3;
    assume that
A1: P in absolute and
A2: Q in absolute and
A3: P <> Q and
A4: P = Dir u & Q = Dir v & R = Dir w and
A5: u`3 = 1 & v`3 = 1 and
A6: w = |[ (u`1 + v`1) / 2,(u`2 + v`2) / 2, 1]|;
A7: u.3 = 1 & v.3 = 1 by A5,EUCLID_5:def 3;
    reconsider u9 = |[u.1,u.2]|,v9 = |[v.1,v.2]| as Element of TOP-REAL 2;
    set M = the_midpoint_of_the_segment(u9,v9);
A8: w`1 = (u`1+v`1)*1/2 & w`2=(u`2+v`2)*1/2 by A6,EUCLID_5:2;
A9: M = 1/2 * (u9 + v9) by EUCLID12:29
     .= 1/2 * |[u.1 + v.1,u.2 + v.2]| by EUCLID:56
     .= |[(u.1+v.1)*1/2,(u.2+v.2)*1/2]| by EUCLID:58
     .= |[(u`1+v.1)*1/2,(u.2+v.2)*1/2]| by EUCLID_5:def 1
     .= |[(u`1+v.1)*1/2,(u`2+v.2)*1/2]| by EUCLID_5:def 2
     .= |[(u`1+v`1)*1/2,(u`2+v.2)*1/2]| by EUCLID_5:def 1
     .= |[w`1,w`2]| by A8,EUCLID_5:def 2;
    u9 in circle(0,0,1) & v9 in circle(0,0,1) by A7,A1,A2,A4,BKMODEL1:84;
    then
A10: LSeg(u9,v9) \ {u9,v9} c= inside_of_circle(0,0,1) by TOPREAL9:60;
    u9 <> v9
    proof
      assume u9 = v9;
      then u.1 = v.1 & u.2 = v.2 by FINSEQ_1:77;
      then u`1 = v.1 & u`2 = v.2 by EUCLID_5:def 1,def 2;
      then u`1 = v`1 & u`2 = v`2 by EUCLID_5:def 1,def 2;
      then u = |[v`1,v`2,v`3]| by A5,EUCLID_5:3
            .= v by EUCLID_5:3;
      hence contradiction by A4,A3;
    end;
    then M <> u9 & M <> v9 by EUCLID12:32,33;
    then
A11: not M in {u9,v9} by TARSKI:def 2;
    M in LSeg(u9,v9) by EUCLID12:28;
    then M in LSeg(u9,v9) \ {u9,v9} by A11,XBOOLE_0:def 5;
    then reconsider rw = |[w`1,w`2]| as Element of inside_of_circle(0,0,1)
      by A10,A9;
   consider RW2 be Element of TOP-REAL 2 such that
A12: RW2 = rw & REAL2_to_BK rw = Dir |[RW2`1,RW2`2,1]| by BKMODEL2:def 3;
A13: rw`1 = w`1 & rw`2 = w`2 by EUCLID:52;
   |[RW2`1,RW2`2,1]| = |[w`1,w`2,w`3]| by A12,A13,A6,EUCLID_5:2
                    .= w by EUCLID_5:3;
    hence thesis by A12,A4;
  end;

theorem Th49:
  for R1,R2 being Point of TarskiEuclid2Space st
  Tn2TR R1 in circle(0,0,1) & Tn2TR R2 in circle(0,0,1) & R1 <> R2 holds
  ex P being Element of BK-model-Plane st between R1,BK_to_T2 P,R2
  proof
    let R1,R2 be Point of TarskiEuclid2Space;
    assume
A1: Tn2TR R1 in circle(0,0,1) & Tn2TR R2 in circle(0,0,1) & R1 <> R2;
    reconsider P = Tn2TR R1, Q = Tn2TR R2 as Element of TOP-REAL 2;
A2: P = |[P`1,P`2]| & Q = |[Q`1,Q`2]| by EUCLID:53;
    reconsider w = |[ (P`1+Q`1)/2,(P`2+Q`2)/2 ]| as Element of TOP-REAL 2;
    reconsider u9 = |[P`1,P`2,1]|,
               v9 = |[Q`1,Q`2,1]| as non zero Element of TOP-REAL 3;
    reconsider w9 = |[w`1,w`2,1]| as non zero Element of TOP-REAL 3;
    reconsider P9 = Dir u9, Q9 = Dir v9,
               R9 = Dir w9 as Point of ProjectiveSpace TOP-REAL 3
                 by ANPROJ_1:26;
    u9`3 = 1 & v9`3 = 1 by EUCLID_5:2;
    then reconsider P9,Q9 as
      non point_at_infty Point of ProjectiveSpace TOP-REAL 3 by Th40;
    w9`3 <> 0 by EUCLID_5:2;
    then reconsider R9 as
      non point_at_infty Point of ProjectiveSpace TOP-REAL 3 by Th40;
    reconsider R99 = RP3_to_T2 R9 as Point of TarskiEuclid2Space;
    consider w99 be non zero Element of TOP-REAL 3 such that
A3: R9 = Dir w99 & w99`3 = 1 & RP3_to_REAL2 R9 = |[w99`1,w99`2]|  by Def05;
A4: w9`1 = w`1 & w9`2 = w`2 by EUCLID_5:2;
    w99.3 = 1 & w9`3 = 1 by A3,EUCLID_5:2,def 3;
    then w99.3 = w9.3 & w9.3 <> 0 by EUCLID_5:def 3;
    then
A5: w99 = w9 by A3,BKMODEL1:43;
A6: Tn2TR R99 = w by A3,A5,A4,EUCLID:53;
    w = |[ P`1 / 2 + Q`1 / 2, P`2 / 2 + Q`2 / 2]|
     .= |[ P`1/2 ,P`2/2]| + |[Q`1/2,Q`2/2]| by EUCLID:56
     .= 1/2 * |[P`1,P`2]| + |[Q`1/2,Q`2/2]| by EUCLID:58
     .= (1 - 1/2) * P + 1/2 * Q by A2,EUCLID:58;
    then w in {(1-r)*P + r * Q where r is Real: 0 <= r & r <= 1};
    then
A7: w in LSeg(Tn2TR R1,Tn2TR R2) by RLTOPSP1:def 2;
    now
      now
        thus P9 = Dir u9;
        u9`3 = 1 by EUCLID_5:2;
        hence u9.3 = 1 by EUCLID_5:def 3;
        thus |[P`1,P`2]| in circle(0,0,1) by A1,EUCLID:53;
        u9`1 = P`1 & u9`2 = P`2 by EUCLID_5:2;
        then P`1 = u9.1 & P`2 = u9.2 by EUCLID_5:def 1,def 2;
        hence |[u9.1,u9.2]| in circle(0,0,1) by A1,EUCLID:53;
      end;
      then P9 is Element of absolute by BKMODEL1:86;
      hence P9 in absolute;
      now
        thus Q9 = Dir v9;
        v9`3 = 1 by EUCLID_5:2;
        hence v9.3 = 1 by EUCLID_5:def 3;
        v9`1 = Q`1 & v9`2 = Q`2 by EUCLID_5:2;
        then Q`1 = v9.1 & Q`2 = v9.2 by EUCLID_5:def 1,def 2;
        hence |[v9.1,v9.2]| in circle(0,0,1) by A1,EUCLID:53;
      end;
      then Q9 is Element of absolute by BKMODEL1:86;
      hence Q9 in absolute;
      thus P9 <> Q9
      proof
        assume
A8:     P9 = Q9;
        now
          thus Dir u9 = Dir v9 by A8;
          thus u9.3 = u9`3 by EUCLID_5:def 3
                   .= 1 by EUCLID_5:2;
          thus v9.3 = v9`3 by EUCLID_5:def 3
                   .= 1 by EUCLID_5:2;
        end;
        then u9 = v9 by BKMODEL1:43;
        then P`1 = Q`1 & P`2 = Q`2 by FINSEQ_1:78;
        then |[P`1,P`2]| = Q by EUCLID:53;
        hence contradiction by A1,EUCLID:53;
      end;
      thus u9`3 = 1 & v9`3 = 1 by EUCLID_5:2;
      thus w9 = |[(u9`1+ v9`1)/2,(u9`2+v9`2)/2,1]|
      proof
        u9`1 = P`1 & v9`1 = Q`1 & u9`2 = P`2 & v9`2 = Q`2 &
          w`1 = (P`1+Q`1)/2 & w`2 = (P`2+Q`2)/2 by EUCLID:52,EUCLID_5:2;
        hence thesis;
      end;
    end;
    then reconsider AR9 = R9 as Element of BK-model-Plane by Th48;
    consider r be Element of BK_model such that
A9: AR9 = r and
A10: BK_to_T2 AR9 = BK_to_REAL2 r by Def01;
    take AR9;
    now
      thus R99 = RP3_to_T2 R9;
      consider x be non zero Element of TOP-REAL 3 such that
A11:  Dir x = r & x.3 = 1 & BK_to_REAL2 r = |[x.1,x.2]| by BKMODEL2:def 2;
      now
        thus Dir x = Dir w9 by A11,A9;
        thus x.3 <> 0 by A11;
        w9.3 = w9`3 by EUCLID_5:def 3
            .= 1 by EUCLID_5:2;
        hence x.3 = w9.3 by A11;
      end;
      then x = w9 by Th16;
      then BK_to_REAL2 r = |[w9`1,w9.2]| by A11,EUCLID_5:def 1
                        .= |[w`1,w`2]| by A4,EUCLID_5:def 2
                        .= w by EUCLID:53;
      hence RP3_to_T2 R9 = BK_to_T2 AR9 by A3,A5,A4,EUCLID:53,A10;
    end;
    hence
    between R1,BK_to_T2 AR9,R2 by A7,A6,GTARSKI2:20;
  end;

theorem Th50:
  for P,Q being non point_at_infty Element of ProjectiveSpace TOP-REAL 3 st
  RP3_to_T2 P = RP3_to_T2 Q holds P = Q
  proof
    let P,Q be non point_at_infty Element of ProjectiveSpace TOP-REAL 3;
    assume
A1: RP3_to_T2 P = RP3_to_T2 Q;
    consider u be non zero Element of TOP-REAL 3 such that
A2: P = Dir u and
A3: u`3 = 1 and
A4: RP3_to_REAL2 P = |[u`1,u`2]| by Def05;
    consider v be non zero Element of TOP-REAL 3 such that
A5: Q = Dir v and
A6: v`3 = 1 and
A7: RP3_to_REAL2 Q = |[v`1,v`2]| by Def05;
    v`1 = u`1 & v`2 = u`2 & v`3 = u`3 by A1,A4,A7,A3,A6,FINSEQ_1:77;
    then |[u`1,u`2,u`3]| = v by EUCLID_5:3;
    hence thesis by A2,A5,EUCLID_5:3;
  end;

theorem Th51:
  for R1,R2 being non point_at_infty Element of ProjectiveSpace TOP-REAL 3
  st R1 in absolute & R2 in absolute & R1 <> R2 holds
  ex P being Element of BK-model-Plane st
  between RP3_to_T2 R1,BK_to_T2 P,RP3_to_T2 R2
  proof
    let R1,R2 be non point_at_infty Element of ProjectiveSpace TOP-REAL 3;
    assume that
A1: R1 in absolute & R2 in absolute and
A2: R1 <> R2;
    consider u1 be non zero Element of TOP-REAL 3 such that
A3: R1 = Dir u1 and
A4: u1`3 = 1 and
A5: RP3_to_REAL2 R1 = |[u1`1,u1`2]| by Def05;
    u1.3 = 1 by A4,EUCLID_5:def 3;
    then |[u1.1,u1.2]| in circle(0,0,1) by A1,A3,BKMODEL1:84;
    then
A6: |[u1`1,u1.2]| in circle(0,0,1) by EUCLID_5:def 1;
    consider u2 be non zero Element of TOP-REAL 3 such that
A7: R2 = Dir u2 and
A8: u2`3 = 1 and
A9: RP3_to_REAL2 R2 = |[u2`1,u2`2]| by Def05;
    u2.3 = 1 by A8,EUCLID_5:def 3;
    then |[u2.1,u2.2]| in circle(0,0,1) by A1,A7,BKMODEL1:84;
    then
A10: |[u2`1,u2.2]| in circle(0,0,1) by EUCLID_5:def 1;
    reconsider P1 = RP3_to_T2 R1,
    P2 = RP3_to_T2 R2 as Point of TarskiEuclid2Space;
    Tn2TR P1 in circle(0,0,1) & Tn2TR P2 in circle(0,0,1) & P1 <> P2
      by A2,Th50,A6,A5,A9,A10,EUCLID_5:def 2;
    hence thesis by Th49;
  end;

theorem Th52:
  for P,Q,R being Point of TarskiEuclid2Space st between P,Q,R &
  Tn2TR P in inside_of_circle(0,0,1) & Tn2TR R in inside_of_circle(0,0,1)
  holds Tn2TR Q in inside_of_circle(0,0,1)
  proof
    let P,Q,R be Point of TarskiEuclid2Space;
    assume that
A1: between P,Q,R and
A2: Tn2TR P in inside_of_circle(0,0,1) & Tn2TR R in inside_of_circle(0,0,1);
    LSeg(Tn2TR P,Tn2TR R) c= inside_of_circle(0,0,1) by A2,RLTOPSP1:22;
    hence thesis by A1,GTARSKI2:20;
  end;

theorem Th53:
  for P being non point_at_infty Element of ProjectiveSpace TOP-REAL 3
  st P in absolute holds RP3_to_REAL2 P in circle(0,0,1)
  proof
    let P be non point_at_infty Element of ProjectiveSpace TOP-REAL 3;
    assume
A1: P in absolute;
    consider u be non zero Element of TOP-REAL 3 such that
A2: P = Dir u & u`3 = 1 & RP3_to_REAL2 P = |[u`1,u`2]| by Def05;
    u.3 = 1 by A2,EUCLID_5:def 3;
    then |[u.1,u.2]| in circle(0,0,1) by A1,A2,BKMODEL1:84;
    then |[u`1,u.2]| in circle(0,0,1) by EUCLID_5:def 1;
    hence thesis by A2,EUCLID_5:def 2;
  end;

theorem
  for P being non point_at_infty Element of ProjectiveSpace TOP-REAL 3
  st P in BK_model holds RP3_to_REAL2 P in inside_of_circle(0,0,1)
  proof
    let P be non point_at_infty Element of ProjectiveSpace TOP-REAL 3;
    assume P in BK_model;
    then reconsider P1 = P as Element of BK_model;
    consider u be non zero Element of TOP-REAL 3 such that
A1: Dir u = P1 & u.3 = 1 and
A2: BK_to_REAL2 P1 = |[u.1,u.2]| by BKMODEL2:def 2;
    |[u`1,u.2]| is Element of inside_of_circle(0,0,1) by A2,EUCLID_5:def 1;
    then
A3: |[u`1,u`2]| is Element of inside_of_circle(0,0,1) by EUCLID_5:def 2;
    consider v be non zero Element of TOP-REAL 3 such that
A4: P = Dir v & v`3 = 1 & RP3_to_REAL2 P = |[v`1,v`2]| by Def05;
    Dir v = Dir u & u.3 <> 0 & u.3 = v.3 by A1,A4,EUCLID_5:def 3;
    then u = v by Th16;
    hence thesis by A4,A3;
  end;

theorem Th54:
  for P being non point_at_infty Point of ProjectiveSpace TOP-REAL 3
  for Q being Element of BK_model st P = Q holds RP3_to_REAL2 P = BK_to_REAL2 Q
  proof
    let P be non point_at_infty Point of ProjectiveSpace TOP-REAL 3;
    let Q be Element of BK_model;
    assume
A1: P = Q;
    consider u be non zero Element of TOP-REAL 3 such that
A2: P = Dir u & u`3 = 1 & RP3_to_REAL2 P = |[u`1,u`2]| by Def05;
    consider v be non zero Element of TOP-REAL 3 such that
A3: Dir v = Q & v.3 = 1 & BK_to_REAL2 Q = |[v.1,v.2]| by BKMODEL2:def 2;
    Dir v = Dir u & u.3 <> 0 & u.3 = v.3 by A1,A2,A3,EUCLID_5:def 3;
    then u = v by Th16;
    then BK_to_REAL2 Q = |[u`1,u.2]| by A3,EUCLID_5:def 1
                      .= |[u`1,u`2]| by EUCLID_5:def 2;
    hence thesis by A2;
  end;

theorem Th55:
  for P,Q,R1,R2 being non point_at_infty Element of ProjectiveSpace
  TOP-REAL 3 st P <> Q & P in BK_model & R1 in absolute &
  R2 in absolute & between RP3_to_T2 P,RP3_to_T2 Q,RP3_to_T2 R1 &
  between RP3_to_T2 P,RP3_to_T2 Q,RP3_to_T2 R2 holds R1 = R2
  proof
    let P,Q,R1,R2 be non point_at_infty Element of ProjectiveSpace TOP-REAL 3;
    assume that
A1: P <> Q and
A2: P in BK_model and
A3: R1 in absolute and
A4: R2 in absolute and
A5: between RP3_to_T2 P,RP3_to_T2 Q,RP3_to_T2 R1 and
A6: between RP3_to_T2 P,RP3_to_T2 Q,RP3_to_T2 R2;
    assume R1 <> R2;
    then consider S be Element of BK-model-Plane such that
A7: between RP3_to_T2 R1,BK_to_T2 S,RP3_to_T2 R2 by A3,A4,Th51;
    set p = RP3_to_T2 P, q = RP3_to_T2 Q, r1 = RP3_to_T2 R1,
      r2 = RP3_to_T2 R2, s = BK_to_T2 S;
    (between p,r1,r2 or between p,r2,r1) & between r1,s,r2 & between r2,s,r1
      by A7,GTARSKI1:16,A1,A5,A6,Th50,GTARSKI3:56;
    then per cases by GTARSKI1:19;
    suppose
A8:   between p,r1,s;
A9:   RP3_to_REAL2 R1 in circle(0,0,1) by A3,Th53;
      now
        thus between p,r1,s by A8;
        reconsider P9 = P as Element of BK_model by A2;
        BK_to_REAL2 P9 = RP3_to_REAL2 P by Th54;
        hence Tn2TR p in inside_of_circle(0,0,1);
        thus Tn2TR s in inside_of_circle(0,0,1) by Th02;
      end;
      then Tn2TR r1 in inside_of_circle(0,0,1) by Th52;
      then RP3_to_REAL2 R1 in inside_of_circle(0,0,1) /\ circle(0,0,1)
        by A9,XBOOLE_0:def 4;
      hence contradiction by XBOOLE_0:def 7,TOPREAL9:54;
    end;
    suppose
A10:  between p,r2,s;
A11:  RP3_to_REAL2 R2 in circle(0,0,1) by A4,Th53;
      now
        thus between p,r2,s by A10;
        reconsider P9 = P as Element of BK_model by A2;
        reconsider P99 = P9 as POINT of BK-model-Plane;
        BK_to_REAL2 P9 = RP3_to_REAL2 P by Th54;
        hence Tn2TR p in inside_of_circle(0,0,1);
        thus Tn2TR s in inside_of_circle(0,0,1) by Th02;
      end;
      then Tn2TR r2 in inside_of_circle(0,0,1) by Th52;
      then RP3_to_REAL2 R2 in inside_of_circle(0,0,1) /\ circle(0,0,1)
        by A11,XBOOLE_0:def 4;
      hence contradiction by XBOOLE_0:def 7,TOPREAL9:54;
    end;
  end;

theorem Th56:
  for P,Q,P1,P2 being non point_at_infty Element of ProjectiveSpace
  TOP-REAL 3 st P <> Q & P in BK_model & Q in BK_model & P1 in absolute &
  P2 in absolute & P1 <> P2 & P,Q,P1 are_collinear & P,Q,P2 are_collinear
  holds between RP3_to_T2 Q,RP3_to_T2 P,RP3_to_T2 P1 or
  between RP3_to_T2 Q,RP3_to_T2 P,RP3_to_T2 P2
  proof
    let P,Q,P1,P2 be non point_at_infty Element of ProjectiveSpace TOP-REAL 3;
    assume that
A1: P <> Q and
A2: P in BK_model and
A3: Q in BK_model and
A4: P1 in absolute and
A5: P2 in absolute and
A6: P1 <> P2 and
A7: P,Q,P1 are_collinear and
A8: P,Q,P2 are_collinear;
    set  P9 = RP3_to_T2 P, Q9 = RP3_to_T2 Q, P19 = RP3_to_T2 P1,
        P29 = RP3_to_T2 P2;
    Collinear P9,Q9,P19 & Collinear P9,Q9,P29 &
      not between Q9,P19,P9 & not between Q9,P29,P9
      by A2,A3,A4,A5,A7,A8,Th47,Th46;
    hence thesis by A1,A2,A4,A5,A6,Th55,GTARSKI1:16;
  end;

theorem Th57:
  for P,Q being Element of BK_model st P <> Q holds
  ex R being Element of absolute st
  (for p,q,r being non point_at_infty Element of ProjectiveSpace TOP-REAL 3 st
  p = P & q = Q & r = R holds between RP3_to_T2 q,RP3_to_T2 p,RP3_to_T2 r)
  proof
    let P,Q be Element of BK_model;
    assume
A1: P <> Q;
    then consider P1,P2 be Element of absolute such that
A2: P1 <> P2 and
A3: P,Q,P1 are_collinear & P,Q,P2 are_collinear by BKMODEL2:20;
    reconsider p = P,q = Q,p1 = P1,
               p2 = P2 as Element of ProjectiveSpace TOP-REAL 3;
    now
      consider u be Element of TOP-REAL 3 such that
A4:   u is not zero and
A5:   p = Dir u by ANPROJ_1:26;
      u.3 <> 0 by A4,A5,BKMODEL2:2;
      then u`3 <> 0 by EUCLID_5:def 3;
      hence p is non point_at_infty by A4,A5,Th40;
      consider v be Element of TOP-REAL 3 such that
A6:   v is not zero and
A7:   q = Dir v by ANPROJ_1:26;
      v.3 <> 0 by A6,A7,BKMODEL2:2;
      then v`3 <> 0 by EUCLID_5:def 3;
      hence q is non point_at_infty by A6,A7,Th40;
      consider w be non zero Element of TOP-REAL 3 such that
A8:   w.3 = 1 and
A9:   p1 = Dir w by BKMODEL3:30;
      w`3 <> 0 by A8,EUCLID_5:def 3;
      hence p1 is non point_at_infty by A9,Th40;
      consider x be non zero Element of TOP-REAL 3 such that
A10:  x.3 = 1 and
A11:  p2 = Dir x by BKMODEL3:30;
      x`3 <> 0 by A10,EUCLID_5:def 3;
      hence p2 is non point_at_infty by A11,Th40;
    end;
    then reconsider p,q,p1,p2 as
      non point_at_infty Element of ProjectiveSpace TOP-REAL 3;
    per cases by A1,A2,A3,Th56;
    suppose
A12:  between RP3_to_T2 q,RP3_to_T2 p,RP3_to_T2 p1;
      take P1;
      thus thesis by A12;
    end;
    suppose
A13:  between RP3_to_T2 q,RP3_to_T2 p,RP3_to_T2 p2;
      take P2;
      thus thesis by A13;
    end;
  end;

theorem Th58:
  for P,Q being Element of BK_model st P <> Q holds
  ex R being Element of absolute st
  (for p,q,r being non point_at_infty Element of ProjectiveSpace TOP-REAL 3 st
  p = P & q = Q & r = R holds between RP3_to_T2 p,RP3_to_T2 q,RP3_to_T2 r)
  proof
    let P,Q be Element of BK_model;
    assume P <> Q;
    then consider R be Element of absolute such that
A1: (for p,q,r being non point_at_infty Element of ProjectiveSpace TOP-REAL 3
      st p = Q & q = P & r = R holds
      between RP3_to_T2 q,RP3_to_T2 p,RP3_to_T2 r) by Th57;
    take R;
    thus thesis by A1;
  end;

theorem Th59:
  Dir |[1,0,1]| is Element of absolute
  proof
    reconsider u = |[1,0,1]| as non zero Element of TOP-REAL 3;
    reconsider P = Dir u as Element of ProjectiveSpace TOP-REAL 3
      by ANPROJ_1:26;
    now
      thus u.3 = u`3 by EUCLID_5:def 3
              .= 1 by EUCLID_5:2;
      now
        thus u.1 = u`1 by EUCLID_5:def 1
                .= 1 by EUCLID_5:2;
        thus u.2 = u`2 by EUCLID_5:def 2
                .= 0 by EUCLID_5:2;
      end;
      then u.1 * u.1 = 1 & u.2 * u.2 = 0;
      then (u.1)^2 = 1 & (u.2)^2 = 0 by SQUARE_1:def 1;
      then (u.1)^2 + (u.2)^2 = 1;
      hence |[u.1,u.2]| in circle(0,0,1) by BKMODEL1:13;
    end;
    then P is Element of absolute by BKMODEL1:86;
    hence thesis;
  end;

theorem Th60:
  for a,b being POINT of BK-model-Plane holds a,a equiv b,b
  proof
    let a,b be POINT of BK-model-Plane;
    reconsider A = a, B = b as Element of BK_model;
    reconsider P = Dir |[1,0,1]| as Element of absolute by Th59;
    consider N be 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 the set of all homography(N) where
    N is invertible Matrix of 3,F_Real;
    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 st
      ex N being invertible Matrix of 3,F_Real st h = homography(N) &
      homography(N).a = b & homography(N).a = b
    proof
      take h;
      take N;
      thus thesis by A2;
    end;
    hence thesis by BKMODEL3:def 8;
  end;

theorem Th61:
  for P being Element of BK_model holds
  P is non point_at_infty Element of ProjectiveSpace TOP-REAL 3
  proof
    let P be Element of BK_model;
    reconsider p = P as Element of ProjectiveSpace TOP-REAL 3;
    consider u be Element of TOP-REAL 3 such that
    P1: u is not zero and
    P2: p = Dir u by ANPROJ_1:26;
    u.3 <> 0 by P1,P2,BKMODEL2:2;
    then u`3 <> 0 by EUCLID_5:def 3;
    hence thesis by P1,P2,Th40;
  end;

theorem Th62:
  for P being Element of absolute holds
  P is non point_at_infty Element of ProjectiveSpace TOP-REAL 3
  proof
    let P be Element of absolute;
    consider u be non zero Element of TOP-REAL 3 such that
A1: u.3 = 1 and
A2: P = Dir u by BKMODEL3:30;
    u`3 = 1 by A1,EUCLID_5:def 3;
    hence thesis by A2,Th40;
  end;

theorem Th63:
  for P being Element of BK_model
  for P9 being non point_at_infty Element of ProjectiveSpace TOP-REAL 3 st
  P = P9 holds RP3_to_REAL2 P9 = BK_to_REAL2 P
  proof
    let P be Element of BK_model;
    let P9 be non point_at_infty Element of ProjectiveSpace TOP-REAL 3;
    assume
A1: P = P9;
    consider u be non zero Element of TOP-REAL 3 such that
A2: P9 = Dir u & u`3 = 1 & RP3_to_REAL2 P9 = |[u`1,u`2]| by Def05;
    consider v be non zero Element of TOP-REAL 3 such that
A3: Dir v = P & v.3 = 1 & BK_to_REAL2 P = |[v.1,v.2]| by BKMODEL2:def 2;
    Dir u = Dir v & u.3 = v.3 & u.3 <> 0 by A1,A2,A3,EUCLID_5:def 3;
    then u = v by Th16;
    then u`1 = v.1 & u`2 = v.2 by EUCLID_5:def 1,def 2;
    hence thesis by A2,A3;
  end;

theorem Th64:
  for a, q, b, c being POINT of BK-model-Plane holds
  ex x being POINT of BK-model-Plane st between q,a,x & a,x equiv b,c
  proof
    let A,Q,B,C be POINT of BK-model-Plane;
    consider a be Element of BK_model such that
A1: A = a and
    BK_to_T2 A = BK_to_REAL2 a by Def01;
    consider q be Element of BK_model such that
A2: Q = q and
    BK_to_T2 Q = BK_to_REAL2 q by Def01;
    consider b be Element of BK_model such that
A3: B = b and
    BK_to_T2 B = BK_to_REAL2 b by Def01;
    consider c be Element of BK_model such that
A4: C = c and
    BK_to_T2 C = BK_to_REAL2 c by Def01;
    per cases;
    suppose b <> c;
A5:   for q1,a1,b1,c1 being POINT of BK-model-Plane st q1 <> a1 holds
      ex x being POINT of BK-model-Plane st between q1,a1,x & a1,x equiv b1,c1
      proof
        let q1,a1,b1,c1 be POINT of BK-model-Plane;
        assume
A6:     q1 <> a1;
        reconsider Q1 = q1, A1 = a1, B1 = b1, C1 = c1 as Element of BK_model;
        reconsider pQ1=Q1,pA1=A1,pB1=B1,pC1=C1 as
          non point_at_infty Element of ProjectiveSpace TOP-REAL 3 by Th61;
        consider qaR be Element of absolute such that
A7:     (for p,q,r being non point_at_infty Element of
          ProjectiveSpace TOP-REAL 3 st p = q1 & q = a1 & r = qaR holds
          between RP3_to_T2 p,RP3_to_T2 q,RP3_to_T2 r)
          by A6,Th58;
        reconsider pqaR = qaR as
          non point_at_infty Element of ProjectiveSpace TOP-REAL 3 by Th62;
        per cases;
        suppose
A8:       B1 = C1;
          reconsider x = a1 as Element of BK_model;
          reconsider x as POINT of BK-model-Plane;
          take x;
          Tn2TR BK_to_T2 a1 in LSeg(Tn2TR BK_to_T2 q1,Tn2TR BK_to_T2 x)
            by RLTOPSP1:68;
          then between BK_to_T2 q1,BK_to_T2 a1,BK_to_T2 x by GTARSKI2:20;
          hence between q1,a1,x by Th05;
          thus a1,x equiv b1,c1 by A8,Th60;
        end;
        suppose
A9:       B1 <> C1;
          consider bcP be Element of absolute such that
A10:      (for p,q,r being non point_at_infty Element of ProjectiveSpace
            TOP-REAL 3 st p = b1 & q = c1 & r = bcP holds
            between RP3_to_T2 p,RP3_to_T2 q,RP3_to_T2 r) by A9,Th58;
          reconsider pbcP = bcP as non point_at_infty Element of
            ProjectiveSpace TOP-REAL 3 by Th62;
          consider N be invertible Matrix of 3,F_Real such that
A11:      homography(N).:absolute = absolute and
A12:      (homography(N)).B1 = A1 and
A13:      (homography(N)).bcP = qaR by BKMODEL2:56;
          homography(N) in the set of all homography(N) where
          N is invertible Matrix of 3,F_Real;
          then reconsider h = homography(N) as Element of EnsHomography3
            by ANPROJ_9:def 1;
          h is_K-isometry by A11,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;
          h = homography(N);
          then reconsider x = (homography(N)).C1 as Element of BK_model
            by BKMODEL3:36;
          reconsider x as POINT of BK-model-Plane;
          reconsider px = x as non point_at_infty Element of
          ProjectiveSpace TOP-REAL 3 by Th61;
          take x;
          now
            thus between q1,a1,x
            proof
A14:          between RP3_to_T2 pQ1,RP3_to_T2 pA1,RP3_to_T2 pqaR by A7;
              between RP3_to_T2 pB1,RP3_to_T2 pC1,RP3_to_T2 pbcP &
                h = homography(N) & pB1 in BK_model & pC1 in BK_model &
                pbcP in absolute by A10;
              then
A15:          between RP3_to_T2 pA1,RP3_to_T2 px,RP3_to_T2 pqaR
                by A12,A13,Th41;
              set tq = RP3_to_T2 pQ1, ta = RP3_to_T2 pA1,
                  tx = RP3_to_T2 px, tr = RP3_to_T2 pqaR;
A16:          between tq,ta,tx by A15,A14,GTARSKI3:17;
              now
                consider pp1 be Element of BK_model such that
A17:            q1 = pp1 and
A18:            BK_to_T2 q1 = BK_to_REAL2 pp1 by Def01;
                consider pp2 be Element of BK_model such that
A19:            a1 = pp2 and
A20:            BK_to_T2 a1 = BK_to_REAL2 pp2 by Def01;
                consider pp3 be Element of BK_model such that
A21:            x = pp3 and
A22:            BK_to_T2 x = BK_to_REAL2 pp3 by Def01;
                thus tq = BK_to_T2 q1 by A17,A18,Th63;
                thus ta = BK_to_T2 a1 by A19,A20,Th63;
                thus tx = BK_to_T2 x by Th63,A21,A22;
              end;
              hence thesis by A16,Th05;
            end;
            ex h being Element of SubGroupK-isometry st
            ex N being invertible Matrix of 3,F_Real st
            h = homography(N) & homography(N).a1 = b1 & homography(N).x = c1
            proof
A23:          h = homography(N);
              reconsider M = N~ as invertible Matrix of 3,F_Real;
              reconsider g = homography(M) as Element of SubGroupK-isometry
                by A23,BKMODEL2:47;
              take g;
              ex N being invertible Matrix of 3,F_Real st
                g = homography(N) & homography(N).a1 = b1 &
                homography(N).x = c1
              proof
                take M;
                thus thesis by A12,ANPROJ_9:15;
              end;
              hence thesis;
            end;
            hence a1,x equiv b1,c1 by BKMODEL3:def 8;
          end;
          hence thesis;
        end;
      end;
      q = a implies ex x being POINT of BK-model-Plane st between Q,A,x &
        A,x equiv B,C
      proof
        assume
A24:    q = a;
        consider Q3 be Element of BK_model such that
A25:    a <> Q3 by BKMODEL3:11;
        reconsider q3 = Q3 as Element of BK-model-Plane;
        consider x be POINT of BK-model-Plane such that
        between q3,A,x and
A26:    A,x equiv B,C by A25,A1,A5;
        take x;
        between BK_to_T2 A,BK_to_T2 A,BK_to_T2 x by GTARSKI1:17;
        hence thesis by A26,A1,A24,A2,Th05;
      end;
      hence thesis by A1,A2,A5;
    end;
    suppose
A27:  b = c;
      set X = A;
      take X;
      between BK_to_T2 Q,BK_to_T2 A,BK_to_T2 X by GTARSKI1:14;
      hence between Q,A,X by Th05;
      thus A,A equiv B,C by A27,A3,A4,Th60;
    end;
  end;

theorem Th65:
  for P,Q being POINT of BK-model-Plane st BK_to_T2 P = BK_to_T2 Q holds P = Q
  proof
    let P,Q be POINT of BK-model-Plane;
    assume
A1: BK_to_T2 P = BK_to_T2 Q;
    (ex q be Element of BK_model st Q = q &
      BK_to_T2 Q = BK_to_REAL2 q) &
      (ex p be Element of BK_model st P = p &
      BK_to_T2 P = BK_to_REAL2 p) by Def01;
    hence thesis by A1,BKMODEL2:4;
  end;

theorem
  for a,b,r being Real
  for P,Q,R being Element of TOP-REAL 2 st
  P in inside_of_circle(a,b,r) & R in inside_of_circle(a,b,r) holds
  LSeg(P,R) c= inside_of_circle(a,b,r) by Th15;

begin :: SegmentConstruction

theorem
  BK-model-Plane is satisfying_SegmentConstruction by Th64;

begin :: BetweennessIdentity

theorem
  BK-model-Plane is satisfying_BetweennessIdentity
  proof
    let P,Q be POINT of BK-model-Plane;
    assume
A1: between P,Q,P;
    reconsider P2 = BK_to_T2 P, Q2 = BK_to_T2 Q as POINT of TarskiEuclid2Space;
    between P2,Q2,P2 by A1,Th05;
    hence thesis by GTARSKI1:def 10,Th65;
  end;

begin :: Pasch

theorem
  BK-model-Plane is satisfying_Pasch
  proof
    let A,B,P,Q,Z be POINT of BK-model-Plane;
    assume that
A1: between A,P,Z and
A2: between B,Q,Z;
    reconsider a = A,b = B,p = P,q = Q,z = Z as Element of BK_model;
    reconsider A2 = BK_to_T2 A, B2 = BK_to_T2 B, P2 = BK_to_T2 P,
    Q2 = BK_to_T2 Q, Z2 = BK_to_T2 Z as POINT of TarskiEuclid2Space;
    between A2,P2,Z2 & between B2,Q2,Z2 by A1,A2,Th05;
    then consider X2 be POINT of TarskiEuclid2Space such that
A3: between P2,X2,B2 and
A4: between Q2,X2,A2 by GTARSKI1:def 11;
    reconsider X = T2_to_BK X2 as POINT of BK-model-Plane;
A5: Tn2TR X2 in LSeg(Tn2TR P2,Tn2TR B2) by A3,GTARSKI2:20;
    set P9 = Tn2TR P2, B9 = Tn2TR B2;
    P9 in inside_of_circle(0,0,1) & B9 in inside_of_circle(0,0,1) by Th02;
    then Tn2TR X2 is Element of inside_of_circle(0,0,1) by A5,Th15;
    then X2 = BK_to_T2 X by Th03;
    then between P,X,B & between Q,X,A by A3,A4,Th05;
    hence thesis;
  end;

subset_name: curated