:: Principle of Duality in Real Projective Plane: a Proof of the Converse 
:: of {D}esargues' Theorem and a Proof of the Converse of {P}appus' 
:: Theorem by Transport
::  by Roland Coghetto
:: 
:: Received September 30, 2021
:: Copyright (c) 2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies INCSP_1, ANPROJ11, REAL_1, XCMPLX_0, ANPROJ_1, ANPROJ_2,
      PENCIL_1, MCART_1, EUCLID_5, ARYTM_1, ARYTM_3, CARD_1, EUCLID, FUNCT_1,
      NUMBERS, PRE_TOPC, RELAT_1, SUBSET_1, SUPINF_2, ANPROJ_9, TARSKI,
      INCPROJ, RVSUM_1, BKMODEL1, CARD_FIL, PROJRED2, PBOOLE, RELAT_2, AFF_2,
      VECTSP_1, ANALOAF;
 notations TARSKI, SUBSET_1, XCMPLX_0, PRE_TOPC, RVSUM_1, COLLSP, INCPROJ,
      ANPROJ_9, XREAL_0, NUMBERS, FUNCT_1, FINSEQ_2, EUCLID, ANPROJ_1,
      BKMODEL1, STRUCT_0, RLVECT_1, EUCLID_5, INCSP_1, PROJRED2, ANPROJ_2;
 constructors MONOID_0, EUCLID_5, ANPROJ_9, BKMODEL1, EUCLID_8, PROJRED2;
 registrations BKMODEL3, ORDINAL1, ANPROJ_1, STRUCT_0, XREAL_0, MONOID_0,
      EUCLID, VALUED_0, ANPROJ_2, FUNCT_1, FINSEQ_1, XCMPLX_0, INCPROJ, PASCAL;
 requirements SUBSET, NUMERALS, ARITHM, BOOLE;


begin ::Preliminaries

theorem :: ANPROJ11:1
  for a,b,c,d,e,f,g,h,i being Real holds
  |{ |[a,b,c]|,
     |[d,e,f]|,
     |[g,h,i]| }| = a * e * i + b * f * g + c * d * h
                    - g * e * c - h * f * a - i * d * b;

theorem :: ANPROJ11:2
  for a,b,c,d,e being Real holds
  |{ |[a,1,0]|,
     |[b,0,1]|,
     |[c,d,e]| }| = c - a * d - e * b;

theorem :: ANPROJ11:3
  for a,b,c,d,e being Real holds
  |{ |[1,a,0]|,
     |[0,b,1]|,
     |[c,d,e]| }| = b * e + a * c - d;

theorem :: ANPROJ11:4
  for a,b,c,d,e being Real holds
  |{ |[1,0,a]|,
     |[0,1,b]|,
     |[c,d,e]| }| = e - c * a - d * b;

theorem :: ANPROJ11:5
  for u being Element of TOP-REAL 3 holds u is zero iff |( u, u )| = 0;

theorem :: ANPROJ11:6
  for u,v,w being non zero Element of TOP-REAL 3 st |{u,v,w}| = 0
  holds ex p being non zero Element of TOP-REAL 3 st
  |(p,u)| = 0 & |(p,v)| = 0 & |(p,w)| = 0;

theorem :: ANPROJ11:7
  for u,v,w being non zero Element of TOP-REAL 3 st
  |(u,v)| = 0 & are_Prop w,v holds |(u,w)| = 0;

theorem :: ANPROJ11:8
  for a,u,v being non zero Element of TOP-REAL 3 st not are_Prop u,v &
  |(a,u)| = 0 & |(a,v)| = 0 holds are_Prop a,u <X> v;

theorem :: ANPROJ11:9
  for u,v being non zero Element of TOP-REAL 3
  for r being Real st r <> 0 & are_Prop u,v holds are_Prop r * u,v;

begin :: Alignment of definitions

definition
  let P being Point of ProjectiveSpace TOP-REAL 3;
  attr P is zero_proj1 means
:: ANPROJ11:def 1

  for u being non zero Element of TOP-REAL 3 st P = Dir u holds u.1 = 0;
end;

registration
  cluster zero_proj1 for Point of ProjectiveSpace TOP-REAL 3;
end;

registration
  cluster non zero_proj1 for Point of ProjectiveSpace TOP-REAL 3;
end;

theorem :: ANPROJ11:10
  for P being non zero_proj1 Point of ProjectiveSpace TOP-REAL 3
  for u being non zero Element of TOP-REAL 3 st P = Dir u holds
  u.1 <> 0;

definition
  let P being non zero_proj1 Point of ProjectiveSpace TOP-REAL 3;
  func normalize_proj1(P) -> non zero Element of TOP-REAL 3 means
:: ANPROJ11:def 2

  Dir it = P & it.1 = 1;
end;

theorem :: ANPROJ11:11
  for P being non zero_proj1 Point of ProjectiveSpace TOP-REAL 3
  for u being non zero Element of TOP-REAL 3 st P = Dir u holds
  normalize_proj1 P = |[1, u.2/u.1,u.3/u.1]|;

theorem :: ANPROJ11:12
  for P being non zero_proj1 Point of ProjectiveSpace TOP-REAL 3
  for Q being Point of ProjectiveSpace TOP-REAL 3 st
  Q = Dir normalize_proj1(P) holds Q is non zero_proj1;

definition
  let P being Point of ProjectiveSpace TOP-REAL 3;
  attr P is zero_proj2 means
:: ANPROJ11:def 3

  for u being non zero Element of TOP-REAL 3 st P = Dir u holds u.2 = 0;
end;

registration
  cluster zero_proj2 for Point of ProjectiveSpace TOP-REAL 3;
end;

registration
  cluster non zero_proj2 for Point of ProjectiveSpace TOP-REAL 3;
end;

theorem :: ANPROJ11:13
  for P being non zero_proj2 Point of ProjectiveSpace TOP-REAL 3
  for u being non zero Element of TOP-REAL 3 st P = Dir u holds
  u.2 <> 0;

definition
  let P being non zero_proj2 Point of ProjectiveSpace TOP-REAL 3;
  func normalize_proj2(P) -> non zero Element of TOP-REAL 3 means
:: ANPROJ11:def 4

  Dir it = P & it.2 = 1;
end;

theorem :: ANPROJ11:14
  for P being non zero_proj2 Point of ProjectiveSpace TOP-REAL 3
  for u being non zero Element of TOP-REAL 3 st P = Dir u holds
  normalize_proj2 P = |[u.1/u.2,1,u.3/u.2]|;

theorem :: ANPROJ11:15
  for P being non zero_proj2 Point of ProjectiveSpace TOP-REAL 3
  for Q being Point of ProjectiveSpace TOP-REAL 3 st
  Q = Dir normalize_proj2(P) holds Q is non zero_proj2;

definition
  let P being Point of ProjectiveSpace TOP-REAL 3;
  attr P is zero_proj3 means
:: ANPROJ11:def 5

  for u being non zero Element of TOP-REAL 3 st P = Dir u holds u.3 = 0;
end;

registration
  cluster zero_proj3 for Point of ProjectiveSpace TOP-REAL 3;
end;

registration
  cluster non zero_proj3 for Point of ProjectiveSpace TOP-REAL 3;
end;

theorem :: ANPROJ11:16
  for P being non zero_proj3 Point of ProjectiveSpace TOP-REAL 3
  for u being non zero Element of TOP-REAL 3 st P = Dir u holds
  u.3 <> 0;

definition
  let P being non zero_proj3 Point of ProjectiveSpace TOP-REAL 3;
  func normalize_proj3(P) -> non zero Element of TOP-REAL 3 means
:: ANPROJ11:def 6

  Dir it = P & it.3 = 1;
end;

theorem :: ANPROJ11:17
  for P being non zero_proj3 Point of ProjectiveSpace TOP-REAL 3
  for u being non zero Element of TOP-REAL 3 st P = Dir u holds
  normalize_proj3 P = |[u.1/u.3,u.2/u.3,1]|;

theorem :: ANPROJ11:18
  for P being non zero_proj3 Point of ProjectiveSpace TOP-REAL 3
  for Q being Point of ProjectiveSpace TOP-REAL 3 st
  Q = Dir normalize_proj3(P) holds Q is non zero_proj3;

registration
  cluster non zero_proj1 non zero_proj2 for Point of
    ProjectiveSpace TOP-REAL 3;
end;
registration
  cluster non zero_proj1 non zero_proj3 for Point of
    ProjectiveSpace TOP-REAL 3;
end;
registration
  cluster non zero_proj2 non zero_proj3 for Point of
    ProjectiveSpace TOP-REAL 3;
end;

registration
  cluster non zero_proj1 non zero_proj2 non zero_proj3 for Point of
    ProjectiveSpace TOP-REAL 3;
end;

definition
  let P being non zero_proj1 Point of ProjectiveSpace TOP-REAL 3;
  func dir1a(P) -> non zero Element of TOP-REAL 3 equals
:: ANPROJ11:def 7
  |[- (normalize_proj1(P)).2,1,0]|;
end;
definition
  let P being non zero_proj1 Point of ProjectiveSpace TOP-REAL 3;
  func Pdir1a P -> Point of ProjectiveSpace TOP-REAL 3 equals
:: ANPROJ11:def 8
  Dir (dir1a P);
end;

definition
  let P being non zero_proj1 Point of ProjectiveSpace TOP-REAL 3;
  func dir1b(P) -> non zero Element of TOP-REAL 3 equals
:: ANPROJ11:def 9
  |[- (normalize_proj1(P)).3,0,1]|;
end;

definition
  let P being non zero_proj1 Point of ProjectiveSpace TOP-REAL 3;
  func Pdir1b P -> Point of ProjectiveSpace TOP-REAL 3 equals
:: ANPROJ11:def 10
  Dir (dir1b P);
end;

theorem :: ANPROJ11:19
  for P being non zero_proj1 Point of ProjectiveSpace TOP-REAL 3 holds
  dir1a(P) <> dir1b(P);

theorem :: ANPROJ11:20
  for P being non zero_proj1 Point of ProjectiveSpace TOP-REAL 3 holds
  Dir dir1a(P) <> Dir dir1b(P);

theorem :: ANPROJ11:21
  for P being non zero_proj1 Element of ProjectiveSpace TOP-REAL 3
  for u being non zero Element of TOP-REAL 3
  for v being Element of TOP-REAL 3 st u = normalize_proj1 P holds
  |{ dir1a P,dir1b P,v }| = |(u,v)|;

theorem :: ANPROJ11:22
  for P being non zero_proj1 Element of ProjectiveSpace TOP-REAL 3
  for u being non zero Element of TOP-REAL 3 st u = normalize_proj1 P holds
  |{ dir1a P,dir1b P,normalize_proj1 P }| = 1 + u.2 * u.2 + u.3 * u.3;

definition
  let P being non zero_proj2 Point of ProjectiveSpace TOP-REAL 3;
  func dir2a(P) -> non zero Element of TOP-REAL 3 equals
:: ANPROJ11:def 11
  |[1, - (normalize_proj2(P)).1,0]|;
end;
definition
  let P being non zero_proj2 Point of ProjectiveSpace TOP-REAL 3;
  func Pdir2a P -> Point of ProjectiveSpace TOP-REAL 3 equals
:: ANPROJ11:def 12
  Dir (dir2a P);
end;

definition
  let P being non zero_proj2 Point of ProjectiveSpace TOP-REAL 3;
  func dir2b(P) -> non zero Element of TOP-REAL 3 equals
:: ANPROJ11:def 13
  |[0, - (normalize_proj2(P)).3,1]|;
end;

definition
  let P being non zero_proj2 Point of ProjectiveSpace TOP-REAL 3;
  func Pdir2b P -> Point of ProjectiveSpace TOP-REAL 3 equals
:: ANPROJ11:def 14
  Dir (dir2b P);
end;

theorem :: ANPROJ11:23
  for P being non zero_proj2 Point of ProjectiveSpace TOP-REAL 3 holds
  dir2a(P) <> dir2b(P);

theorem :: ANPROJ11:24
  for P being non zero_proj2 Point of ProjectiveSpace TOP-REAL 3 holds
  Dir dir2a(P) <> Dir dir2b(P);

theorem :: ANPROJ11:25
  for P being non zero_proj2 Element of ProjectiveSpace TOP-REAL 3
  for u being non zero Element of TOP-REAL 3
  for v being Element of TOP-REAL 3 st u = normalize_proj2 P holds
  |{ dir2a P,dir2b P,v }| = - |(u,v)|;

theorem :: ANPROJ11:26
  for P being non zero_proj2 Element of ProjectiveSpace TOP-REAL 3
  for u being non zero Element of TOP-REAL 3 st u = normalize_proj2 P holds
  |{ dir2a P,dir2b P,normalize_proj2 P }| = - (u.1 * u.1 + 1 + u.3 * u.3);

definition
  let P being non zero_proj3 Point of ProjectiveSpace TOP-REAL 3;
  func dir3a(P) -> non zero Element of TOP-REAL 3 equals
:: ANPROJ11:def 15
  |[1,0,- (normalize_proj3(P)).1]|;
end;

definition
  let P being non zero_proj3 Point of ProjectiveSpace TOP-REAL 3;
  func Pdir3a P -> Point of ProjectiveSpace TOP-REAL 3 equals
:: ANPROJ11:def 16
  Dir (dir3a P);
end;

definition
  let P being non zero_proj3 Point of ProjectiveSpace TOP-REAL 3;
  func dir3b(P) -> non zero Element of TOP-REAL 3 equals
:: ANPROJ11:def 17
  |[0,1,- (normalize_proj3(P)).2]|;
end;

definition
  let P being non zero_proj3 Point of ProjectiveSpace TOP-REAL 3;
  func Pdir3b P -> Point of ProjectiveSpace TOP-REAL 3 equals
:: ANPROJ11:def 18
  Dir (dir3b P);
end;

theorem :: ANPROJ11:27
  for P being non zero_proj3 Point of ProjectiveSpace TOP-REAL 3 holds
  dir3a(P) <> dir3b(P);

theorem :: ANPROJ11:28
  for P being non zero_proj3 Point of ProjectiveSpace TOP-REAL 3 holds
  Dir dir3a(P) <> Dir dir3b(P);

theorem :: ANPROJ11:29
  for P being non zero_proj3 Element of ProjectiveSpace TOP-REAL 3
  for u being non zero Element of TOP-REAL 3
  for v being Element of TOP-REAL 3 st u = normalize_proj3 P holds
  |{ dir3a P,dir3b P,v }| = |(u,v)|;

theorem :: ANPROJ11:30
  for P being non zero_proj3 Element of ProjectiveSpace TOP-REAL 3
  for u being non zero Element of TOP-REAL 3 st u = normalize_proj3 P holds
  |{ dir3a P,dir3b P,normalize_proj3 P }| = u.1 * u.1 + u.2 * u.2 + 1;

definition
  let P being non zero_proj1 Point of ProjectiveSpace TOP-REAL 3;
  func dual1 P -> Element of ProjectiveLines real_projective_plane equals
:: ANPROJ11:def 19
  Line(Pdir1a P,Pdir1b P);
end;

definition
  let P being non zero_proj2 Point of ProjectiveSpace TOP-REAL 3;
  func dual2 P -> Element of ProjectiveLines real_projective_plane equals
:: ANPROJ11:def 20
  Line(Pdir2a P,Pdir2b P);
end;

definition
  let P being non zero_proj3 Point of ProjectiveSpace TOP-REAL 3;
  func dual3 P -> Element of ProjectiveLines real_projective_plane equals
:: ANPROJ11:def 21
  Line(Pdir3a P,Pdir3b P);
end;

theorem :: ANPROJ11:31
  for P being non zero_proj1 non zero_proj2 Point of ProjectiveSpace TOP-REAL 3
  for u being non zero Element of TOP-REAL 3 st P = Dir u holds
  normalize_proj1 P = |[1, u.2/u.1, u.3/u.1]| &
  normalize_proj2 P = |[u.1/u.2, 1, u.3/u.2]|;

theorem :: ANPROJ11:32
  for P being non zero_proj1 non zero_proj2 Point of ProjectiveSpace TOP-REAL 3
  for u being non zero Element of TOP-REAL 3 st P = Dir u holds
  normalize_proj1 P = u.2/u.1 * normalize_proj2 P &
  normalize_proj2 P = u.1/u.2 * normalize_proj1 P;

theorem :: ANPROJ11:33
  for P being non zero_proj1 non zero_proj2 Point of ProjectiveSpace
  TOP-REAL 3 holds dual1 P = dual2 P;

theorem :: ANPROJ11:34
  for P being non zero_proj2 non zero_proj3 Point of ProjectiveSpace
  TOP-REAL 3 holds dual2 P = dual3 P;

theorem :: ANPROJ11:35
  for P being non zero_proj1 non zero_proj3 Point of ProjectiveSpace
  TOP-REAL 3 holds dual1 P = dual3 P;

theorem :: ANPROJ11:36
  for P being non zero_proj1 non zero_proj2 non zero_proj3 Point of
  ProjectiveSpace TOP-REAL 3 holds dual1 P = dual2 P & dual1 P = dual3 P &
  dual2 P = dual3 P;

theorem :: ANPROJ11:37
  for P being Element of ProjectiveSpace TOP-REAL 3 holds
  P is non zero_proj1 or P is non zero_proj2 or P is non zero_proj3;

definition
  let P being Point of ProjectiveSpace TOP-REAL 3;
  func dual P -> Element of ProjectiveLines real_projective_plane means
:: ANPROJ11:def 22

   ex P9 being non zero_proj1 Point of ProjectiveSpace TOP-REAL 3 st P9 = P &
   it = dual1 P9
if P is non zero_proj1,
  ex P9 being non zero_proj2 Point of ProjectiveSpace TOP-REAL 3 st P9 = P &
  it = dual2 P9
if (P is zero_proj1 & P is non zero_proj2),
  ex P9 being non zero_proj3 Point of ProjectiveSpace TOP-REAL 3 st P9 = P &
  it = dual3 P9
if (P is zero_proj1 & P is zero_proj2 & P is non zero_proj3);
end;

definition
  let P being Point of real_projective_plane;
  func # P -> Element of ProjectiveSpace TOP-REAL 3 equals
:: ANPROJ11:def 23
P;
end;

definition
  let P being Point of real_projective_plane;
  func dual P -> Element of ProjectiveLines real_projective_plane equals
:: ANPROJ11:def 24
  dual #P;
end;

theorem :: ANPROJ11:38
  for P being Element of real_projective_plane st #P is non zero_proj1 holds
  ex P9 being non zero_proj1 Point of ProjectiveSpace TOP-REAL 3 st
  P = P9 & dual P = dual1 P9;

theorem :: ANPROJ11:39
  for P being Element of real_projective_plane st #P is non zero_proj2 holds
  ex P9 being non zero_proj2 Point of ProjectiveSpace TOP-REAL 3 st
  P = P9 & dual P = dual2 P9;

theorem :: ANPROJ11:40
  for P being Element of real_projective_plane st #P is non zero_proj3 holds
  ex P9 being non zero_proj3 Point of ProjectiveSpace TOP-REAL 3 st
  P = P9 & dual P = dual3 P9;

theorem :: ANPROJ11:41
  for P being non zero_proj1 Element of ProjectiveSpace TOP-REAL 3 holds
  not P in Line(Pdir1a P,Pdir1b P);

theorem :: ANPROJ11:42
  for P being non zero_proj2 Element of ProjectiveSpace TOP-REAL 3 holds
  not P in Line(Pdir2a P,Pdir2b P);

theorem :: ANPROJ11:43
  for P being non zero_proj3 Element of ProjectiveSpace TOP-REAL 3 holds
  not P in Line(Pdir3a P,Pdir3b P);

theorem :: ANPROJ11:44
  for P being Point of real_projective_plane holds not P in dual P;

definition
  let l being Element of ProjectiveLines real_projective_plane;
  func dual l -> Point of real_projective_plane means
:: ANPROJ11:def 25

  ex P,Q being Point of real_projective_plane st P <> Q &
  l = Line(P,Q) & it = L2P(P,Q);
end;

theorem :: ANPROJ11:45
  for P being Point of real_projective_plane holds dual dual P = P;

theorem :: ANPROJ11:46
  for l being Element of ProjectiveLines real_projective_plane holds
  dual dual l = l;

theorem :: ANPROJ11:47
  for P,Q being Point of real_projective_plane holds
  (P <> Q iff dual P <> dual Q);

theorem :: ANPROJ11:48
  for l,m being Element of ProjectiveLines real_projective_plane holds
  (l <> m iff dual l <> dual m);

begin

definition
  let l1,l2,l3 being Element of ProjectiveLines real_projective_plane;
  pred l1,l2,l3 are_concurrent means
:: ANPROJ11:def 26
  ex P being Point of real_projective_plane st P in l1 & P in l2 & P in l3;
end;

definition
  let l being Element of ProjectiveLines real_projective_plane;
  func #l -> LINE of IncProjSp_of real_projective_plane equals
:: ANPROJ11:def 27
l;
end;

definition
  let l being LINE of IncProjSp_of real_projective_plane;
  func #l -> Element of ProjectiveLines real_projective_plane equals
:: ANPROJ11:def 28
l;
end;

theorem :: ANPROJ11:49
  for l1,l2,l3 being Element of ProjectiveLines real_projective_plane holds
  l1,l2,l3 are_concurrent iff #l1,#l2,#l3 are_concurrent;

theorem :: ANPROJ11:50
  for l1,l2,l3 being LINE of IncProjSp_of real_projective_plane holds
  l1,l2,l3 are_concurrent iff #l1,#l2,#l3 are_concurrent;

theorem :: ANPROJ11:51
  for P,Q,R being Element of real_projective_plane st P,Q,R are_collinear holds
  Q,R,P are_collinear & R,P,Q are_collinear &
  P,R,Q are_collinear & R,Q,P are_collinear &
  Q,P,R are_collinear;

theorem :: ANPROJ11:52
  for l1,l2,l3 being Element of ProjectiveLines real_projective_plane st
  l1,l2,l3 are_concurrent holds l2,l1,l3 are_concurrent &
  l1,l3,l2 are_concurrent & l3,l2,l1 are_concurrent &
  l3,l2,l1 are_concurrent & l2,l3,l1 are_concurrent;

theorem :: ANPROJ11:53
  for P,Q being Point of real_projective_plane
  for P9,Q9 being Element of ProjectiveSpace TOP-REAL 3 st
  P = P9 & Q = Q9 holds Line(P,Q) = Line(P9,Q9);

theorem :: ANPROJ11:54
  for P being Point of real_projective_plane
  for l being Element of ProjectiveLines real_projective_plane st P in l holds
  dual l in dual P;

theorem :: ANPROJ11:55
  for P being Point of real_projective_plane
  for l being Element of ProjectiveLines real_projective_plane st
  dual l in dual P holds P in l;

theorem :: ANPROJ11:56
  for P,Q,R being Point of real_projective_plane st P,Q,R are_collinear holds
  dual P,dual Q, dual R are_concurrent;

theorem :: ANPROJ11:57
  for l being Element of ProjectiveLines real_projective_plane
  for P,Q,R being Point of real_projective_plane st
  P in l & Q in l & R in l holds P,Q,R are_collinear;

theorem :: ANPROJ11:58
  for l1,l2,l3 being Element of ProjectiveLines real_projective_plane st
  l1,l2,l3 are_concurrent holds dual l1,dual l2,dual l3 are_collinear;

theorem :: ANPROJ11:59
  for P,Q,R being Point of real_projective_plane holds
  P,Q,R are_collinear iff dual P,dual Q,dual R are_concurrent;

theorem :: ANPROJ11:60
  for l1,l2,l3 being Element of ProjectiveLines real_projective_plane holds
  l1,l2,l3 are_concurrent iff dual l1, dual l2, dual l3 are_collinear;

begin :: Some converse theorems

theorem :: ANPROJ11:61
  real_projective_plane is reflexive &
  real_projective_plane is transitive &
  real_projective_plane is Vebleian &
  real_projective_plane is at_least_3rank &
  real_projective_plane is Fanoian &
  real_projective_plane is Desarguesian &
  real_projective_plane is Pappian &
  real_projective_plane is 2-dimensional;

::$N Converse reflexive
theorem :: ANPROJ11:62
  for l,m,n being Element of ProjectiveLines real_projective_plane holds
  l,m,l are_concurrent & l,l,m are_concurrent & l,m,m are_concurrent;

::$N Converse transitive
theorem :: ANPROJ11:63
  for l,m,n,n1,n2 being Element of ProjectiveLines real_projective_plane st
  l <> m & l,m,n are_concurrent & l,m,n1 are_concurrent &
  l,m,n2 are_concurrent holds n,n1,n2 are_concurrent;

::$N Converse Vebliean
theorem :: ANPROJ11:64
  for l,l1,l2,n,n1 being Element of ProjectiveLines real_projective_plane st
  l,l1,n are_concurrent & l1,l2,n1 are_concurrent
  ex n2 being Element of ProjectiveLines real_projective_plane st
  l,l2,n2 are_concurrent & n,n1,n2 are_concurrent;

::$N Converse at_least_3rank
theorem :: ANPROJ11:65
  for l,m being Element of ProjectiveLines real_projective_plane holds
  ex n being Element of ProjectiveLines real_projective_plane st
  l <> n & m <> n & l,m,n are_concurrent;

::$N Converse Fanoian
theorem :: ANPROJ11:66
  for l1,n2,m,n1,m1,l,n being Element of ProjectiveLines
  real_projective_plane holds
  (l1,n2,m are_concurrent & n1,m1,m are_concurrent & l1,n1,l are_concurrent &
  n2,m1,l are_concurrent & l1,m1,n are_concurrent & n2,n1,n are_concurrent &
  l,m,n are_concurrent implies
  (l1,n2,m1 are_concurrent or l1,n2,n1 are_concurrent or
  l1,n1,m1 are_concurrent or n2,n1,m1 are_concurrent));

::$N Converse Desarguesian
theorem :: ANPROJ11:67
  for k,l1,l2,l3,m1,m2,m3,n1,n2,n3 being Element of ProjectiveLines
  real_projective_plane st
  k <> m1 & l1 <> m1 & k <> m2 & l2 <> m2 & k <> m3 & l3 <> m3 &
  not k,l1,l2 are_concurrent & not k,l1,l3 are_concurrent &
  not k,l2,l3 are_concurrent &
  l1,l2,n3 are_concurrent & m1,m2,n3 are_concurrent &
  l2,l3,n1 are_concurrent & m2,m3,n1 are_concurrent &
  l1,l3,n2 are_concurrent & m1,m3,n2 are_concurrent &
  k,l1,m1 are_concurrent & k,l2,m2 are_concurrent &
  k,l3,m3 are_concurrent holds n1,n2,n3 are_concurrent;

::$N Converse Pappian
theorem :: ANPROJ11:68
  for k,l1,l2,l3,m1,m2,m3,n1,n2,n3 being Element of ProjectiveLines
    real_projective_plane st
  k <> l2 & k <> l3 & l2 <> l3 & l1 <> l2 & l1 <> l3 & k <> m2 &
  k <> m3 & m2 <> m3 & m1 <> m2 & m1 <> m3 &
  not k,l1,m1 are_concurrent & k,l1,l2 are_concurrent &
  k,l1,l3 are_concurrent & k,m1,m2 are_concurrent &
  k,m1,m3 are_concurrent & l1,m2,n3 are_concurrent &
  m1,l2,n3 are_concurrent & l1,m3,n2 are_concurrent &
  l3,m1,n2 are_concurrent & l2,m3,n1 are_concurrent &
  l3,m2,n1 are_concurrent holds n1,n2,n3 are_concurrent;

::$N Converse 2_dimensional
theorem :: ANPROJ11:69
  for l,l1,m,m1 being Element of ProjectiveLines
  real_projective_plane holds ex n being Element of ProjectiveLines
  real_projective_plane st l,l1,n are_concurrent &
  m,m1,n are_concurrent;