:: Article AFPROJ, MML version 4.100.1011
:: AFPROJ:th 1
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2 being Element of bool the carrier of B1
      st (B1 is non empty non trivial AffinSpace-like 2-dimensional AffinStruct & B2 = the carrier of B1)
   holds B2 is being_plane(B1);

:: AFPROJ:th 2
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2 being Element of bool the carrier of B1
      st (B1 is non empty non trivial AffinSpace-like 2-dimensional AffinStruct & B2 is being_plane(B1))
   holds B2 = the carrier of B1;

:: AFPROJ:th 3
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2, B3 being Element of bool the carrier of B1 holds
((B1 is non empty non trivial AffinSpace-like 2-dimensional AffinStruct & B2 is being_plane(B1) & B3 is being_plane(B1)) implies B2 = B3);

:: AFPROJ:th 4
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2 being Element of bool the carrier of B1
      st (B2 = the carrier of B1 & B2 is being_plane(B1))
   holds B1 is non empty non trivial AffinSpace-like 2-dimensional AffinStruct;

:: AFPROJ:th 5
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2, B3, B4, B5 being Element of bool the carrier of B1 holds
((not (B2 // B3) & B2 '||' B4 & B2 '||' B5 & B3 '||' B4 & B3 '||' B5 & B2 is being_line(B1) & B3 is being_line(B1) & B4 is being_plane(B1) & B5 is being_plane(B1)) implies B4 '||' B5);

:: AFPROJ:th 6
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2, B3, B4 being Element of bool the carrier of B1 holds
((B2 is being_plane(B1) & B3 '||' B2 & B2 '||' B4) implies B3 '||' B4);

:: AFPROJ:funcnot 1
definition
  let a<sub>1</sub> be non empty non trivial AffinSpace-like AffinStruct;
  func AfLines A1 -> Element of bool bool the carrier of a<sub>1</sub> equals
    {b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of a<sub>1</sub>: b<sub>1</sub> is being_line(a<sub>1</sub>)};
end;

:: AFPROJ:def 1
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct holds
   AfLines B1 = {B2 where B2 is Element of bool the carrier of B1: B2 is being_line(B1)};

:: AFPROJ:funcnot 2
definition
  let a<sub>1</sub> be non empty non trivial AffinSpace-like AffinStruct;
  func AfPlanes A1 -> Element of bool bool the carrier of a<sub>1</sub> equals
    {b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of a<sub>1</sub>: b<sub>1</sub> is being_plane(a<sub>1</sub>)};
end;

:: AFPROJ:def 2
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct holds
   AfPlanes B1 = {B2 where B2 is Element of bool the carrier of B1: B2 is being_plane(B1)};

:: AFPROJ:th 7
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2 being set holds
      B2 in AfLines B1
   iff
      ex B3 being Element of bool the carrier of B1 st
         (B2 = B3 & B3 is being_line(B1));

:: AFPROJ:th 8
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2 being set holds
      B2 in AfPlanes B1
   iff
      ex B3 being Element of bool the carrier of B1 st
         (B2 = B3 & B3 is being_plane(B1));

:: AFPROJ:funcnot 3
definition
  let a<sub>1</sub> be non empty non trivial AffinSpace-like AffinStruct;
  func LinesParallelity A1 -> symmetric transitive total Relation of AfLines a<sub>1</sub>,AfLines a<sub>1</sub> equals
    {[b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub> is Element of bool the carrier of a<sub>1</sub>, b<sub>2</sub> is Element of bool the carrier of a<sub>1</sub>: b<sub>1</sub> is being_line(a<sub>1</sub>) & b<sub>2</sub> is being_line(a<sub>1</sub>) & b<sub>1</sub> '||' b<sub>2</sub>};
end;

:: AFPROJ:def 3
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct holds
   LinesParallelity B1 = {[B2,B3] where B2 is Element of bool the carrier of B1, B3 is Element of bool the carrier of B1: (B2 is being_line(B1) & B3 is being_line(B1) & B2 '||' B3)};

:: AFPROJ:funcnot 4
definition
  let a<sub>1</sub> be non empty non trivial AffinSpace-like AffinStruct;
  func PlanesParallelity A1 -> symmetric transitive total Relation of AfPlanes a<sub>1</sub>,AfPlanes a<sub>1</sub> equals
    {[b<sub>1</sub>,b<sub>2</sub>] where b<sub>1</sub> is Element of bool the carrier of a<sub>1</sub>, b<sub>2</sub> is Element of bool the carrier of a<sub>1</sub>: b<sub>1</sub> is being_plane(a<sub>1</sub>) & b<sub>2</sub> is being_plane(a<sub>1</sub>) & b<sub>1</sub> '||' b<sub>2</sub>};
end;

:: AFPROJ:def 4
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct holds
   PlanesParallelity B1 = {[B2,B3] where B2 is Element of bool the carrier of B1, B3 is Element of bool the carrier of B1: (B2 is being_plane(B1) & B3 is being_plane(B1) & B2 '||' B3)};

:: AFPROJ:funcnot 5
definition
  let a<sub>1</sub> be non empty non trivial AffinSpace-like AffinStruct;
  let a<sub>2</sub> be Element of bool the carrier of a<sub>1</sub>;
  assume a<sub>2</sub> is being_line(a<sub>1</sub>);
  func LDir A2 -> Element of bool AfLines a<sub>1</sub> equals
    Class(LinesParallelity a<sub>1</sub>,a<sub>2</sub>);
end;

:: AFPROJ:def 5
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2 being Element of bool the carrier of B1
      st B2 is being_line(B1)
   holds LDir B2 = Class(LinesParallelity B1,B2);

:: AFPROJ:funcnot 6
definition
  let a<sub>1</sub> be non empty non trivial AffinSpace-like AffinStruct;
  let a<sub>2</sub> be Element of bool the carrier of a<sub>1</sub>;
  assume a<sub>2</sub> is being_plane(a<sub>1</sub>);
  func PDir A2 -> Element of bool AfPlanes a<sub>1</sub> equals
    Class(PlanesParallelity a<sub>1</sub>,a<sub>2</sub>);
end;

:: AFPROJ:def 6
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2 being Element of bool the carrier of B1
      st B2 is being_plane(B1)
   holds PDir B2 = Class(PlanesParallelity B1,B2);

:: AFPROJ:th 9
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2 being Element of bool the carrier of B1
   st B2 is being_line(B1)
for B3 being set holds
      B3 in LDir B2
   iff
      ex B4 being Element of bool the carrier of B1 st
         (B3 = B4 & B4 is being_line(B1) & B2 '||' B4);

:: AFPROJ:th 10
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2 being Element of bool the carrier of B1
   st B2 is being_plane(B1)
for B3 being set holds
      B3 in PDir B2
   iff
      ex B4 being Element of bool the carrier of B1 st
         (B3 = B4 & B4 is being_plane(B1) & B2 '||' B4);

:: AFPROJ:th 11
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2, B3 being Element of bool the carrier of B1 holds
((B2 is being_line(B1) & B3 is being_line(B1)) implies    LDir B2 = LDir B3
iff
   B2 // B3);

:: AFPROJ:th 12
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2, B3 being Element of bool the carrier of B1 holds
((B2 is being_line(B1) & B3 is being_line(B1)) implies    LDir B2 = LDir B3
iff
   B2 '||' B3);

:: AFPROJ:th 13
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2, B3 being Element of bool the carrier of B1 holds
((B2 is being_plane(B1) & B3 is being_plane(B1)) implies    PDir B2 = PDir B3
iff
   B2 '||' B3);

:: AFPROJ:funcnot 7
definition
  let a<sub>1</sub> be non empty non trivial AffinSpace-like AffinStruct;
  func Dir_of_Lines A1 -> non empty set equals
    Class LinesParallelity a<sub>1</sub>;
end;

:: AFPROJ:def 7
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct holds
   Dir_of_Lines B1 = Class LinesParallelity B1;

:: AFPROJ:funcnot 8
definition
  let a<sub>1</sub> be non empty non trivial AffinSpace-like AffinStruct;
  func Dir_of_Planes A1 -> non empty set equals
    Class PlanesParallelity a<sub>1</sub>;
end;

:: AFPROJ:def 8
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct holds
   Dir_of_Planes B1 = Class PlanesParallelity B1;

:: AFPROJ:th 14
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2 being set holds
      B2 in Dir_of_Lines B1
   iff
      ex B3 being Element of bool the carrier of B1 st
         (B2 = LDir B3 & B3 is being_line(B1));

:: AFPROJ:th 15
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2 being set holds
      B2 in Dir_of_Planes B1
   iff
      ex B3 being Element of bool the carrier of B1 st
         (B2 = PDir B3 & B3 is being_plane(B1));

:: AFPROJ:th 16
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct holds
   the carrier of B1 misses Dir_of_Lines B1;

:: AFPROJ:th 17
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
      st B1 is non empty non trivial AffinSpace-like 2-dimensional AffinStruct
   holds AfLines B1 misses Dir_of_Planes B1;

:: AFPROJ:th 18
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2 being set holds
      B2 in [:AfLines B1,{1}:]
   iff
      ex B3 being Element of bool the carrier of B1 st
         (B2 = [B3,1] & B3 is being_line(B1));

:: AFPROJ:th 19
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2 being set holds
      B2 in [:Dir_of_Planes B1,{2}:]
   iff
      ex B3 being Element of bool the carrier of B1 st
         (B2 = [PDir B3,2] & B3 is being_plane(B1));

:: AFPROJ:funcnot 9
definition
  let a<sub>1</sub> be non empty non trivial AffinSpace-like AffinStruct;
  func ProjectivePoints A1 -> non empty set equals
    (the carrier of a<sub>1</sub>) \/ Dir_of_Lines a<sub>1</sub>;
end;

:: AFPROJ:def 9
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct holds
   ProjectivePoints B1 = (the carrier of B1) \/ Dir_of_Lines B1;

:: AFPROJ:funcnot 10
definition
  let a<sub>1</sub> be non empty non trivial AffinSpace-like AffinStruct;
  func ProjectiveLines A1 -> non empty set equals
    [:AfLines a<sub>1</sub>,{1}:] \/ [:Dir_of_Planes a<sub>1</sub>,{2}:];
end;

:: AFPROJ:def 10
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct holds
   ProjectiveLines B1 = [:AfLines B1,{1}:] \/ [:Dir_of_Planes B1,{2}:];

:: AFPROJ:funcnot 11
definition
  let a<sub>1</sub> be non empty non trivial AffinSpace-like AffinStruct;
  func Proj_Inc A1 -> Relation of ProjectivePoints a<sub>1</sub>,ProjectiveLines a<sub>1</sub> means
    for b<sub>1</sub>, b<sub>2</sub> being set holds
       [b<sub>1</sub>,b<sub>2</sub>] in it
    iff
       (for b<sub>3</sub> being Element of bool the carrier of a<sub>1</sub>
             st b<sub>3</sub> is being_line(a<sub>1</sub>) & b<sub>2</sub> = [b<sub>3</sub>,1]
          holds (b<sub>1</sub> in the carrier of a<sub>1</sub> implies not b<sub>1</sub> in b<sub>3</sub>) & <!--ANTONYM-->b<sub>1</sub> <> LDir b<sub>3</sub> implies ex b<sub>3</sub>, b<sub>4</sub> being Element of bool the carrier of a<sub>1</sub> st
          b<sub>3</sub> is being_line(a<sub>1</sub>) & b<sub>4</sub> is being_plane(a<sub>1</sub>) & b<sub>1</sub> = LDir b<sub>3</sub> & b<sub>2</sub> = [PDir b<sub>4</sub>,2] & b<sub>3</sub> '||' b<sub>4</sub>);
end;

:: AFPROJ:def 11
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2 being Relation of ProjectivePoints B1,ProjectiveLines B1 holds
      B2 = Proj_Inc B1
   iff
      for B3, B4 being set holds
         [B3,B4] in B2
      iff
         (for B5 being Element of bool the carrier of B1
               st (B5 is being_line(B1) & B4 = [B5,1])
            holds ((B3 in the carrier of B1 implies not (B3 in B5)) & not (B3 = LDir B5)) implies ex B5 being Element of bool the carrier of B1 st
            ex B6 being Element of bool the carrier of B1 st
               (B5 is being_line(B1) & B6 is being_plane(B1) & B3 = LDir B5 & B4 = [PDir B6,2] & B5 '||' B6));

:: AFPROJ:funcnot 12
definition
  let a<sub>1</sub> be non empty non trivial AffinSpace-like AffinStruct;
  func Inc_of_Dir A1 -> Relation of Dir_of_Lines a<sub>1</sub>,Dir_of_Planes a<sub>1</sub> means
    for b<sub>1</sub>, b<sub>2</sub> being set holds
       [b<sub>1</sub>,b<sub>2</sub>] in it
    iff
       ex b<sub>3</sub>, b<sub>4</sub> being Element of bool the carrier of a<sub>1</sub> st
          b<sub>1</sub> = LDir b<sub>3</sub> & b<sub>2</sub> = PDir b<sub>4</sub> & b<sub>3</sub> is being_line(a<sub>1</sub>) & b<sub>4</sub> is being_plane(a<sub>1</sub>) & b<sub>3</sub> '||' b<sub>4</sub>;
end;

:: AFPROJ:def 12
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2 being Relation of Dir_of_Lines B1,Dir_of_Planes B1 holds
      B2 = Inc_of_Dir B1
   iff
      for B3, B4 being set holds
         [B3,B4] in B2
      iff
         ex B5 being Element of bool the carrier of B1 st
            ex B6 being Element of bool the carrier of B1 st
               (B3 = LDir B5 & B4 = PDir B6 & B5 is being_line(B1) & B6 is being_plane(B1) & B5 '||' B6);

:: AFPROJ:funcnot 13
definition
  let a<sub>1</sub> be non empty non trivial AffinSpace-like AffinStruct;
  func IncProjSp_of A1 -> strict IncProjStr equals
    IncProjStr(#ProjectivePoints a<sub>1</sub>,ProjectiveLines a<sub>1</sub>,Proj_Inc a<sub>1</sub>#);
end;

:: AFPROJ:def 13
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct holds
   IncProjSp_of B1 = IncProjStr(#ProjectivePoints B1,ProjectiveLines B1,Proj_Inc B1#);

:: AFPROJ:funcnot 14
definition
  let a<sub>1</sub> be non empty non trivial AffinSpace-like AffinStruct;
  func ProjHorizon A1 -> strict IncProjStr equals
    IncProjStr(#Dir_of_Lines a<sub>1</sub>,Dir_of_Planes a<sub>1</sub>,Inc_of_Dir a<sub>1</sub>#);
end;

:: AFPROJ:def 14
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct holds
   ProjHorizon B1 = IncProjStr(#Dir_of_Lines B1,Dir_of_Planes B1,Inc_of_Dir B1#);

:: AFPROJ:th 20
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2 being set holds
      B2 is Element of the Points of IncProjSp_of B1
   iff
      (not (B2 is Element of the carrier of B1) implies ex B3 being Element of bool the carrier of B1 st
         (B2 = LDir B3 & B3 is being_line(B1)));

:: AFPROJ:th 21
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2 being set holds
      B2 is Element of the Points of ProjHorizon B1
   iff
      ex B3 being Element of bool the carrier of B1 st
         (B2 = LDir B3 & B3 is being_line(B1));

:: AFPROJ:th 22
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2 being set
      st B2 is Element of the Points of ProjHorizon B1
   holds B2 is Element of the Points of IncProjSp_of B1;

:: AFPROJ:th 23
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2 being set holds
      B2 is Element of the Lines of IncProjSp_of B1
   iff
      ex B3 being Element of bool the carrier of B1 st
         (B2 = [B3,1] & B3 is being_line(B1)) or (B2 = [PDir B3,2] & B3 is being_plane(B1));

:: AFPROJ:th 24
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2 being set holds
      B2 is Element of the Lines of ProjHorizon B1
   iff
      ex B3 being Element of bool the carrier of B1 st
         (B2 = PDir B3 & B3 is being_plane(B1));

:: AFPROJ:th 25
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2 being set
      st B2 is Element of the Lines of ProjHorizon B1
   holds [B2,2] is Element of the Lines of IncProjSp_of B1;

:: AFPROJ:th 26
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2 being Element of the carrier of B1
for B3 being Element of bool the carrier of B1
for B4 being Element of the Points of IncProjSp_of B1
for B5 being Element of the Lines of IncProjSp_of B1
      st (B2 = B4 & [B3,1] = B5)
   holds    B4 on B5
   iff
      (B3 is being_line(B1) & B2 in B3);

:: AFPROJ:th 27
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2 being Element of the carrier of B1
for B3 being Element of bool the carrier of B1
for B4 being Element of the Points of IncProjSp_of B1
for B5 being Element of the Lines of IncProjSp_of B1
      st (B2 = B4 & [PDir B3,2] = B5 & B3 is being_plane(B1))
   holds not (B4 on B5);

:: AFPROJ:th 28
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2, B3 being Element of bool the carrier of B1
for B4 being Element of the Points of IncProjSp_of B1
for B5 being Element of the Lines of IncProjSp_of B1
      st (B4 = LDir B2 & [B3,1] = B5 & B2 is being_line(B1) & B3 is being_line(B1))
   holds    B4 on B5
   iff
      B2 '||' B3;

:: AFPROJ:th 29
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2, B3 being Element of bool the carrier of B1
for B4 being Element of the Points of IncProjSp_of B1
for B5 being Element of the Lines of IncProjSp_of B1
      st (B4 = LDir B2 & B5 = [PDir B3,2] & B2 is being_line(B1) & B3 is being_plane(B1))
   holds    B4 on B5
   iff
      B2 '||' B3;

:: AFPROJ:th 30
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2 being Element of bool the carrier of B1
for B3 being Element of the Points of IncProjSp_of B1
for B4 being Element of the Lines of IncProjSp_of B1
      st (B2 is being_line(B1) & B3 = LDir B2 & B4 = [B2,1])
   holds B3 on B4;

:: AFPROJ:th 31
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2, B3 being Element of bool the carrier of B1
for B4 being Element of the Points of IncProjSp_of B1
for B5 being Element of the Lines of IncProjSp_of B1
      st (B2 is being_line(B1) & B3 is being_plane(B1) & B2 c= B3 & B4 = LDir B2 & B5 = [PDir B3,2])
   holds B4 on B5;

:: AFPROJ:th 32
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2, B3, B4 being Element of bool the carrier of B1
for B5 being Element of the Points of IncProjSp_of B1
for B6 being Element of the Lines of IncProjSp_of B1
      st (B2 is being_plane(B1) & B3 c= B2 & B4 // B3 & B5 = LDir B4 & B6 = [PDir B2,2])
   holds B5 on B6;

:: AFPROJ:th 33
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2 being Element of bool the carrier of B1
for B3 being Element of the Points of IncProjSp_of B1
for B4 being Element of the Lines of IncProjSp_of B1
      st (B4 = [PDir B2,2] & B2 is being_plane(B1) & B3 on B4)
   holds not (B3 is Element of the carrier of B1);

:: AFPROJ:th 34
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2 being Element of bool the carrier of B1
for B3 being Element of the Points of IncProjSp_of B1
for B4 being Element of the Lines of IncProjSp_of B1
      st (B4 = [B2,1] & B2 is being_line(B1) & B3 on B4 & not (B3 is Element of the carrier of B1))
   holds B3 = LDir B2;

:: AFPROJ:th 35
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2 being Element of bool the carrier of B1
for B3, B4 being Element of the Points of IncProjSp_of B1
for B5 being Element of the Lines of IncProjSp_of B1
      st (B5 = [B2,1] & B2 is being_line(B1) & B3 on B5 & B4 on B5 & not (B4 = B3) & not (B3 is Element of the carrier of B1))
   holds B4 is Element of the carrier of B1;

:: AFPROJ:th 36
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2, B3 being Element of bool the carrier of B1
for B4 being Element of the Points of ProjHorizon B1
for B5 being Element of the Lines of ProjHorizon B1
      st (B4 = LDir B2 & B5 = PDir B3 & B2 is being_line(B1) & B3 is being_plane(B1))
   holds    B4 on B5
   iff
      B2 '||' B3;

:: AFPROJ:th 37
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2 being Element of the Points of ProjHorizon B1
for B3 being Element of the Points of IncProjSp_of B1
for B4 being Element of the Lines of ProjHorizon B1
for B5 being Element of the Lines of IncProjSp_of B1
      st (B3 = B2 & B5 = [B4,2])
   holds    B2 on B4
   iff
      B3 on B5;

:: AFPROJ:th 38
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2, B3 being Element of the Points of ProjHorizon B1
for B4, B5 being Element of the Lines of ProjHorizon B1 holds
((B2 on B4 & B2 on B5 & B3 on B4 & B3 on B5 & not (B2 = B3)) implies B4 = B5);

:: AFPROJ:th 39
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2 being Element of the Lines of ProjHorizon B1 holds
   ex B3 being Element of the Points of ProjHorizon B1 st
      ex B4 being Element of the Points of ProjHorizon B1 st
         ex B5 being Element of the Points of ProjHorizon B1 st
            (B3 on B2 & B4 on B2 & B5 on B2 & not (B3 = B4) & not (B4 = B5) & not (B5 = B3));

:: AFPROJ:th 40
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2, B3 being Element of the Points of ProjHorizon B1 holds
ex B4 being Element of the Lines of ProjHorizon B1 st
   (B2 on B4 & B3 on B4);

:: AFPROJ:th 41
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2, B3 being Element of the Points of ProjHorizon B1
for B4 being Element of the Lines of IncProjSp_of B1
      st (not (B2 = B3) & [B2,B4] in the Inc of IncProjSp_of B1 & [B3,B4] in the Inc of IncProjSp_of B1)
   holds ex B5 being Element of the Lines of ProjHorizon B1 st
      B4 = [B5,2];

:: AFPROJ:th 42
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2 being Element of the Points of IncProjSp_of B1
for B3 being Element of the Lines of ProjHorizon B1
      st [B2,[B3,2]] in the Inc of IncProjSp_of B1
   holds B2 is Element of the Points of ProjHorizon B1;

:: AFPROJ:th 43
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2, B3, B4 being Element of bool the carrier of B1
for B5, B6 being Element of the Lines of IncProjSp_of B1 holds
((B2 is being_plane(B1) & B3 is being_line(B1) & B4 is being_line(B1) & B3 c= B2 & B4 c= B2 & B5 = [B3,1] & B6 = [B4,1]) implies ex B7 being Element of the Points of IncProjSp_of B1 st
   (B7 on B5 & B7 on B6));

:: AFPROJ:th 44
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2, B3, B4, B5, B6 being Element of the Points of ProjHorizon B1
for B7, B8, B9, B10 being Element of the Lines of ProjHorizon B1 holds
((B2 on B7 & B3 on B7 & B4 on B8 & B5 on B8 & B6 on B7 & B6 on B8 & B2 on B9 & B4 on B9 & B3 on B10 & B5 on B10 & not (B6 on B9) & not (B6 on B10) & not (B7 = B8)) implies ex B11 being Element of the Points of ProjHorizon B1 st
   (B11 on B9 & B11 on B10));

:: AFPROJ:funcreg 1
registration
  let A1 be non empty non trivial AffinSpace-like AffinStruct;
  cluster IncProjSp_of A1 ->  strict linear partial up-2-dimensional up-3-rank Vebleian;
end;

:: AFPROJ:exreg 1
registration
  cluster strict linear partial up-2-dimensional up-3-rank Vebleian 2-dimensional IncProjStr;
end;

:: AFPROJ:funcreg 2
registration
  let A1 be non empty non trivial AffinSpace-like 2-dimensional AffinStruct;
  cluster IncProjSp_of A1 ->  strict 2-dimensional;
end;

:: AFPROJ:th 45
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
      st IncProjSp_of B1 is 2-dimensional
   holds B1 is non empty non trivial AffinSpace-like 2-dimensional AffinStruct;

:: AFPROJ:th 46
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
      st not (B1 is non empty non trivial AffinSpace-like 2-dimensional AffinStruct)
   holds ProjHorizon B1 is linear partial up-2-dimensional up-3-rank Vebleian IncProjStr;

:: AFPROJ:th 47
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
      st ProjHorizon B1 is linear partial up-2-dimensional up-3-rank Vebleian IncProjStr
   holds not (B1 is non empty non trivial AffinSpace-like 2-dimensional AffinStruct);

:: AFPROJ:th 48
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2, B3 being Element of bool the carrier of B1
for B4, B5, B6, B7, B8, B9, B10 being Element of the carrier of B1 holds
((B2 is being_line(B1) & B3 is being_line(B1) & not (B2 = B3) & B4 in B2 & B4 in B3 & not (B4 = B5) & not (B4 = B8) & not (B4 = B6) & not (B4 = B9) & not (B4 = B7) & not (B4 = B10) & B5 in B2 & B6 in B2 & B7 in B2 & B8 in B3 & B9 in B3 & B10 in B3 & B5,B9 // B6,B8 & B6,B10 // B7,B9 & ((not (B5 = B6) & not (B6 = B7)) implies B5 = B7)) implies B5,B10 // B7,B8);

:: AFPROJ:th 49
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
      st IncProjSp_of B1 is Pappian
   holds B1 is Pappian;

:: AFPROJ:th 50
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
for B2, B3, B4 being Element of bool the carrier of B1
for B5, B6, B7, B8, B9, B10, B11 being Element of the carrier of B1 holds
((B5 in B2 & B5 in B3 & B5 in B4 & not (B5 = B6) & not (B5 = B7) & not (B5 = B8) & B6 in B2 & B9 in B2 & B7 in B3 & B10 in B3 & B8 in B4 & B11 in B4 & B2 is being_line(B1) & B3 is being_line(B1) & B4 is being_line(B1) & not (B2 = B3) & not (B2 = B4) & B6,B7 // B9,B10 & B6,B8 // B9,B11 & B5 = B9 or B6 = B9) implies B7,B8 // B10,B11);

:: AFPROJ:th 51
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
      st IncProjSp_of B1 is Desarguesian
   holds B1 is Desarguesian;

:: AFPROJ:th 52
theorem
for B1 being non empty non trivial AffinSpace-like AffinStruct
      st IncProjSp_of B1 is Fanoian
   holds B1 is Fanoian;