PROJRED2

:: On Projections in Projective Planes. Part II
::  by Eugeniusz Kusak, Wojciech Leo\'nczuk and Krzysztof Pra\.zmowski
::
:: Received October 31, 1990
:: Copyright (c) 1990-2026 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 INCPROJ, INCSP_1, SUBSET_1, AFF_2, ANALOAF, PARTFUN1, PROJRED1,
      FUNCT_1, RELAT_1, TARSKI, ZFMISC_1, PROJRED2;
 notations TARSKI, ZFMISC_1, SUBSET_1, DOMAIN_1, RELAT_1, RELSET_1, INCSP_1,
      INCPROJ, PARTFUN1, FUNCT_1, PROJRED1;
 constructors DOMAIN_1, PROJRED1, RELSET_1;
 registrations FUNCT_1, RELSET_1, INCPROJ;
 requirements SUBSET, BOOLE;
 theorems TARSKI, INCPROJ, FUNCT_1, PROJRED1, ZFMISC_1, INCSP_1, RELAT_1;

begin

reserve IPS for IncProjSp,
  z for POINT of IPS;

definition
  let IPS;
  let A,B,C be LINE of IPS;
  pred A,B,C are_concurrent means

  ex o being Element of the Points of IPS st o on A & o on B & o on C;
end;

definition
  let IPS;
  let Z be LINE of IPS;
  func CHAIN(Z) -> Subset of the Points of IPS equals
  {z: z on Z};
  correctness
  proof
    set X = {z: z on Z};
    now
      let x be object;
      assume x in X;
      then ex z st z=x & z on Z;
      hence x in the Points of IPS;
    end;
    hence thesis by TARSKI:def 3;
  end;
end;

reserve IPP for Desarguesian 2-dimensional IncProjSp,
  a,b,c,d,p,pp9,q,o,o9,o99 ,oo9 for POINT of IPP,
  r,s,x,y,o1,o2 for POINT of IPP,
  O1,O2,O3,O4,A,B,C,O,Q,Q1 ,Q2,Q3,R,S,X for LINE of IPP;

definition
  let IPP;
  mode Projection of IPP -> PartFunc of the Points of IPP,the Points of IPP
    means
    :Def3:
    ex a,A,B st not a on A & not a on B & it = IncProj(A,a,B);
  existence
  proof
    set A = the LINE of IPP;
    consider a such that
A1: ( not a on A)& not a on A by PROJRED1:6;
    take IncProj(A,a,A);
    thus thesis by A1;
  end;
end;

theorem Th1:
  A=B or B=C or C=A implies A,B,C are_concurrent
proof
A1: ( ex a st a on B & a on C)& ex b st b on C & b on A by INCPROJ:def 9;
  assume A=B or B=C or C=A;
  hence thesis by A1;
end;

theorem
  A,B,C are_concurrent implies A,C,B are_concurrent & B,A,C
  are_concurrent & B,C,A are_concurrent & C,A,B are_concurrent & C,B,A
  are_concurrent;

theorem Th3:
  not o on A & not o on B & y on B implies ex x st x on A & IncProj
  (A,o,B).x = y
proof
  consider X such that
A1: o on X & y on X by INCPROJ:def 5;
  consider x such that
A2: x on X and
A3: x on A by INCPROJ:def 9;
  assume ( not o on A)& not o on B & y on B;
  then IncProj(A,o,B).x = y by A1,A2,A3,PROJRED1:def 1;
  hence thesis by A3;
end;

theorem Th4:
  not o on A & not o on B implies dom IncProj(A,o,B) = CHAIN(A)
proof
  assume
A1: ( not o on A)& not o on B;
A2: now
    let x be object;
    assume
A3: x in dom IncProj(A,o,B);
    then reconsider x9 = x as POINT of IPP;
    x9 on A by A1,A3,PROJRED1:def 1;
    hence x in CHAIN(A);
  end;
  now
    let x be object;
    assume x in CHAIN(A);
    then ex b st b=x & b on A;
    hence x in dom IncProj(A,o,B) by A1,PROJRED1:def 1;
  end;
  hence thesis by A2,TARSKI:2;
end;

theorem Th5:
  not o on A & not o on B implies rng IncProj(A,o,B) = CHAIN(B)
proof
  assume
A1: ( not o on A)& not o on B;
A2: now
    let x be object;
    assume
A3: x in CHAIN(B);
    then reconsider x9 = x as Element of the Points of IPP;
    ex b st b=x & b on B by A3;
    then consider y such that
A4: y on A and
A5: IncProj(A,o,B).y = x9 by A1,Th3;
    y in CHAIN(A) by A4;
    then y in dom IncProj (A,o,B) by A1,Th4;
    hence x in rng IncProj(A,o,B) by A5,FUNCT_1:def 3;
  end;
  now
    let x be object such that
A6: x in rng IncProj(A,o,B);
    rng IncProj(A,o,B) c= the Points of IPP by RELAT_1:def 19;
    then reconsider x9 = x as POINT of IPP by A6;
    x9 on B by A1,A6,PROJRED1:21;
    hence x in CHAIN(B);
  end;
  hence thesis by A2,TARSKI:2;
end;

theorem
  for x being set holds x in CHAIN(A) iff ex a st x=a & a on A;

theorem Th7:
  not o on A & not o on B implies IncProj(A,o,B) is one-to-one
proof
  set f = IncProj(A,o,B);
  assume
A1: ( not o on A)& not o on B;
  now
    let x1,x2 be object;
    assume that
A2: x1 in dom f and
A3: x2 in dom f and
A4: f.x1 = f.x2;
    x1 in CHAIN(A) by A1,A2,Th4;
    then consider a such that
A5: x1=a and
A6: a on A;
    x2 in CHAIN(A) by A1,A3,Th4;
    then consider b such that
A7: x2=b and
A8: b on A;
    reconsider x = f.a,y = f.b as POINT of IPP by A1,A6,A8,PROJRED1:19;
    x=y by A4,A5,A7;
    hence x1 = x2 by A1,A5,A6,A7,A8,PROJRED1:23;
  end;
  hence thesis by FUNCT_1:def 4;
end;

theorem Th8:
  not o on A & not o on B implies IncProj(A,o,B)" = IncProj(B,o,A)
proof
  set f=IncProj(A,o,B), g=IncProj (B,o,A);
  assume
A1: ( not o on A)& not o on B;
  then
A2: rng f = CHAIN(B) by Th5;
A3: dom f = CHAIN(A) by A1,Th4;
A4: now
    let y,x be object;
A5: now
      assume that
A6:   x in dom f and
A7:   y=f.x;
      consider x9 being POINT of IPP such that
A8:   x = x9 & x9 on A by A3,A6;
      reconsider y9=y as POINT of IPP by A1,A7,A8,PROJRED1:19;
A9:   y9 on B by A1,A7,A8,PROJRED1:20;
      then
A10:  y in CHAIN(B);
      ex O st o on O & x9 on O & y9 on O by A1,A7,A8,A9,PROJRED1:def 1;
      hence y in rng f & x=g.y by A1,A8,A9,A10,Th5,PROJRED1:def 1;
    end;
    now
      assume that
A11:  y in rng f and
A12:  x=g.y;
      consider y9 being POINT of IPP such that
A13:  y = y9 & y9 on B by A2,A11;
      reconsider x9=x as POINT of IPP by A1,A12,A13,PROJRED1:19;
A14:  x9 on A by A1,A12,A13,PROJRED1:20;
      then ex O st o on O & y9 on O & x9 on O by A1,A12,A13,PROJRED1:def 1;
      hence x in dom f & y=f.x by A1,A13,A14,PROJRED1:def 1;
    end;
    hence y in rng f & x=g.y iff x in dom f & y=f.x by A5;
  end;
A15: f is one-to-one by A1,Th7;
  dom g = CHAIN(B) by A1,Th4
    .= rng f by A1,Th5;
  hence thesis by A15,A4,FUNCT_1:32;
end;

theorem
  for f being Projection of IPP holds f" is Projection of IPP
proof
  let f be Projection of IPP;
  consider a,A,B such that
A1: ( not a on A)& not a on B and
A2: f = IncProj(A,a,B) by Def3;
  f" = IncProj (B,a,A) by A1,A2,Th8;
  hence thesis by A1,Def3;
end;

theorem Th10:
  not o on A implies IncProj(A,o,A) = id CHAIN(A)
proof
  set f = IncProj(A,o,A);
  assume
A1: not o on A;
A2: for x being object st x in CHAIN(A) holds f.x=x
  proof
    let x be object;
    assume x in CHAIN(A);
    then ex x9 being Element of the Points of IPP st x = x9 & x9 on A;
    hence thesis by A1,PROJRED1:24;
  end;
  dom f = CHAIN(A) by A1,Th4;
  hence thesis by A2,FUNCT_1:17;
end;

theorem
  id CHAIN(A) is Projection of IPP
proof
  consider o such that
A1: not o on A by PROJRED1:1;
  (id CHAIN(A)) = IncProj(A,o,A) by A1,Th10;
  hence thesis by A1,Def3;
end;

theorem
  not o on A & not o on B & not o on C implies IncProj(C,o,B)*IncProj(A,
  o,C) = IncProj(A,o,B)
proof
  assume that
A1: not o on A and
A2: not o on B and
A3: not o on C;
  set f=IncProj(A,o,B),g=IncProj(C,o,B),h=IncProj(A,o,C);
A4: dom f= CHAIN(A) by A1,A2,Th4;
  set X = CHAIN(A);
A5: dom h = CHAIN(A) by A1,A3,Th4;
A6: for x st x on A holds IncProj(A,o,B).x = (IncProj(C,o,B)*IncProj(A,o,C)) .x
  proof
    let x such that
A7: x on A;
    consider Q1 such that
A8: o on Q1 and
A9: x on Q1 by INCPROJ:def 5;
    consider x9 being POINT of IPP such that
A10: x9 on Q1 & x9 on C by INCPROJ:def 9;
A11: h.x = x9 by A1,A3,A7,A8,A9,A10,PROJRED1:def 1;
    consider y being POINT of IPP such that
A12: y on Q1 & y on B by INCPROJ:def 9;
A13: f.x = y by A1,A2,A7,A8,A9,A12,PROJRED1:def 1;
    x in dom h by A5,A7;
    then (g*h).x = g.(h.x) by FUNCT_1:13
      .= f.x by A2,A3,A8,A10,A12,A13,A11,PROJRED1:def 1;
    hence thesis;
  end;
A14: now
    let y be object;
    assume y in X;
    then ex x st y=x & x on A;
    hence (g*h).y = f.y by A6;
  end;
  dom (g*h) = X by A1,A2,A3,A5,PROJRED1:22;
  hence thesis by A4,A14,FUNCT_1:2;
end;

theorem
  not o1 on O1 & not o1 on O2 & not o2 on O2 & not o2 on O3 & O1,O2,O3
are_concurrent & O1<>O3 implies ex o st not o on O1 & not o on O3 & IncProj(O2,
  o2,O3)*IncProj(O1,o1,O2) = IncProj(O1,o,O3)
by PROJRED1:25;

theorem Th14:
  not a on A & not b on B & not a on C & not b on C & not A,B,C
are_concurrent & c on A & c on C & c on Q & not b on Q & A<>Q & a on O & b on O
  & not B,C,O are_concurrent & d on C & d on B & a on O1 & d on O1 & p on A & p
on O1 & q on O & q on O2 & p on O2 & pp9 on O2 & d on O3 & b on O3 & pp9 on O3
& pp9 on Q & q<>a & not q on A & not q on Q implies IncProj(C,b,B)*IncProj(A,a,
  C) = IncProj(Q,b,B)*IncProj(A,q,Q)
proof
  assume that
A1: not a on A and
A2: not b on B and
A3: not a on C and
A4: not b on C and
A5: not A,B,C are_concurrent and
A6: c on A and
A7: c on C and
A8: c on Q and
A9: not b on Q and
A10: A<>Q and
A11: a on O and
A12: b on O and
A13: not B,C,O are_concurrent and
A14: d on C and
A15: d on B and
A16: a on O1 and
A17: d on O1 and
A18: p on A and
A19: p on O1 and
A20: q on O and
A21: q on O2 and
A22: p on O2 & pp9 on O2 and
A23: d on O3 & b on O3 and
A24: pp9 on O3 and
A25: pp9 on Q and
A26: q<>a and
A27: not q on A and
A28: not q on Q;
  set f=IncProj(A,a,C),g=IncProj(C,b,B),g1=IncProj(Q,b,B),f1=IncProj (A,q,Q);
A29: dom f= CHAIN(A) by A1,A3,Th4;
  set X = CHAIN(A);
A30: dom f1 = CHAIN(A) by A27,A28,Th4;
  then
A31: dom (g1*f1) = X by A2,A9,A27,A28,PROJRED1:22;
A32: O1<>O2
  proof
    assume not thesis;
    then d on O by A11,A16,A17,A20,A21,A26,INCPROJ:def 4;
    hence contradiction by A13,A14,A15;
  end;
  c <>d by A5,A6,A7,A15;
  then p<>c by A3,A7,A14,A16,A17,A19,INCPROJ:def 4;
  then
A33: pp9<>p by A6,A8,A10,A18,A25,INCPROJ:def 4;
A34: for x st x on A holds (IncProj(C,b,B)*IncProj(A,a,C)).x = (IncProj(Q,b,
  B)* IncProj(A,q,Q)).x
  proof
    let x such that
A35: x on A;
    consider Q3 such that
A36: q on Q3 & x on Q3 by INCPROJ:def 5;
    consider Q1 such that
A37: a on Q1 & x on Q1 by INCPROJ:def 5;
    consider y being POINT of IPP such that
A38: y on Q3 and
A39: y on Q by INCPROJ:def 9;
    consider x9 being POINT of IPP such that
A40: x9 on Q1 and
A41: x9 on C by INCPROJ:def 9;
A42: now
A43:  {pp9,y,c} on Q & {d,x9,c} on C by A7,A8,A14,A25,A41,A39,INCSP_1:2;
A44:  {p,pp9,q} on O2 & {pp9,d,b} on O3 by A21,A22,A23,A24,INCSP_1:2;
A45:  {b,a,q} on O & {x,y,q} on Q3 by A11,A12,A20,A36,A38,INCSP_1:2;
A46:  {p,x,c} on A & {p,d,a} on O1 by A6,A16,A17,A18,A19,A35,INCSP_1:2;
      assume
A47:  p<>x;
      {x,x9,a} on Q1 & A,O1,O2 are_mutually_distinct by A1,A16,A21,A27,A32,A37
,A40,INCSP_1:2,ZFMISC_1:def 5;
      then consider R such that
A48:  {y,x9,b} on R by A1,A3,A14,A18,A33,A47,A46,A44,A43,A45,PROJRED1:12;
A49:  b on R by A48,INCSP_1:2;
      consider x99 being POINT of IPP such that
A50:  x99 on R & x99 on B by INCPROJ:def 9;
      x9 on R by A48,INCSP_1:2;
      then
A51:  g.x9 = x99 by A2,A4,A41,A50,A49,PROJRED1:def 1;
A52:  x in dom f1 by A30,A35;
      y on R by A48,INCSP_1:2;
      then
A53:  g1.y = x99 by A2,A9,A39,A50,A49,PROJRED1:def 1;
A54:  x in dom f by A29,A35;
      f.x = x9 & f1.x = y by A1,A3,A27,A28,A35,A37,A40,A41,A36,A38,A39,
PROJRED1:def 1;
      then (g*f).x = g1.(f1.x) by A51,A53,A54,FUNCT_1:13
        .= (g1*f1).x by A52,FUNCT_1:13;
      hence thesis;
    end;
    now
A55:  f1.p=pp9 & g1.pp9=d by A2,A9,A15,A18,A21,A22,A23,A24,A25,A27,A28,
PROJRED1:def 1;
      assume
A56:  p=x;
A57:  x in dom f1 by A30,A35;
A58:  x in dom f by A29,A35;
      f.p=d & g.d=d by A1,A2,A3,A4,A14,A15,A16,A17,A18,A19,A23,PROJRED1:def 1;
      then (g*f).x = g1.(f1.x) by A56,A55,A58,FUNCT_1:13
        .= (g1*f1).x by A57,FUNCT_1:13;
      hence thesis;
    end;
    hence thesis by A42;
  end;
A59: now
    let y be object;
    assume y in X;
    then ex x st y=x & x on A;
    hence (g*f).y = (g1*f1).y by A34;
  end;
  dom (g*f) = X by A1,A2,A3,A4,A29,PROJRED1:22;
  hence thesis by A31,A59,FUNCT_1:2;
end;

theorem Th15:
  not a on A & not a on C & not b on B & not b on C & not b on Q &
not A,B,C are_concurrent & a<>b & b<>q & A<>Q & {c,o} on A & {o,o99,d} on B & {
c,d,o9} on C & {a,b,d} on O & {c,oo9} on Q & {a,o,o9} on O1 & {b,o9,oo9} on O2
& {o,oo9,q} on O3 & q on O implies IncProj(C,b,B)*IncProj(A,a,C) = IncProj(Q,b,
  B)*IncProj(A,q,Q)
proof
  assume that
A1: not a on A and
A2: not a on C and
A3: not b on B and
A4: not b on C and
A5: not b on Q and
A6: not A,B,C are_concurrent and
A7: a<>b and
A8: b<>q and
A9: A<>Q and
A10: {c,o} on A and
A11: {o,o99,d} on B and
A12: {c,d,o9} on C and
A13: {a,b,d} on O and
A14: {c,oo9} on Q and
A15: {a,o,o9} on O1 and
A16: {b,o9,oo9} on O2 and
A17: {o,oo9,q} on O3 and
A18: q on O;
A19: o on A by A10,INCSP_1:1;
A20: c on A & c on Q by A10,A14,INCSP_1:1;
A21: o9 on C by A12,INCSP_1:2;
A22: oo9 on O2 by A16,INCSP_1:2;
A23: b on O by A13,INCSP_1:2;
A24: q on O3 by A17,INCSP_1:2;
A25: o on O3 & oo9 on O3 by A17,INCSP_1:2;
  set X = CHAIN(A);
  set f=IncProj(A,a,C),g=IncProj(C,b,B),f1=IncProj(A,q,Q),g1=IncProj (Q,b,B);
A26: o on B by A11,INCSP_1:2;
A27: dom f= CHAIN(A) by A1,A2,Th4;
A28: o9 on O2 by A16,INCSP_1:2;
A29: q on O3 by A17,INCSP_1:2;
A30: b on O2 by A16,INCSP_1:2;
A31: o on B by A11,INCSP_1:2;
A32: d on C by A12,INCSP_1:2;
  then
A33: o<>d by A6,A19,A31;
A34: d on O by A13,INCSP_1:2;
A35: o on O3 & oo9 on O3 by A17,INCSP_1:2;
A36: o9 on O1 by A15,INCSP_1:2;
A37: o on A by A10,INCSP_1:1;
A38: a on O1 by A15,INCSP_1:2;
A39: d on B by A11,INCSP_1:2;
  then
A40: q<>o by A3,A18,A31,A23,A34,A33,INCPROJ:def 4;
A41: c on C by A12,INCSP_1:2;
A42: oo9 on Q by A14,INCSP_1:1;
A43: o on O1 by A15,INCSP_1:2;
A44: c on A by A10,INCSP_1:1;
  then
A45: o<>c by A6,A31,A41;
  then
A46: o9<>c by A1,A44,A19,A38,A43,A36,INCPROJ:def 4;
  then
A47: c <>oo9 by A4,A41,A21,A30,A28,A22,INCPROJ:def 4;
A48: not q on A
  proof
    assume not thesis;
    then oo9 on A by A37,A35,A29,A40,INCPROJ:def 4;
    hence contradiction by A9,A20,A42,A47,INCPROJ:def 4;
  end;
A49: a on O by A13,INCSP_1:2;
  o9<>d
  proof
    assume not thesis;
    then O1=O by A2,A32,A49,A34,A38,A36,INCPROJ:def 4;
    hence contradiction by A3,A31,A39,A23,A34,A43,A33,INCPROJ:def 4;
  end;
  then O<>O2 by A2,A32,A21,A49,A34,A28,INCPROJ:def 4;
  then
A50: q<>oo9 by A8,A18,A23,A30,A22,INCPROJ:def 4;
A51: not q on Q
  proof
    assume not thesis;
    then o on Q by A42,A35,A29,A50,INCPROJ:def 4;
    hence contradiction by A9,A20,A37,A45,INCPROJ:def 4;
  end;
  then
A52: dom f1 = CHAIN(A) by A48,Th4;
  then
A53: dom (g1*f1) = X by A3,A5,A48,A51,PROJRED1:22;
A54: d on B & d on O by A11,A13,INCSP_1:2;
A55: O1<>O2
  proof
    assume not thesis;
    then o on O by A7,A49,A23,A38,A43,A30,INCPROJ:def 4;
    then O=B by A54,A26,A33,INCPROJ:def 4;
    hence contradiction by A3,A13,INCSP_1:2;
  end;
A56: c on Q & oo9 on Q by A14,INCSP_1:1;
A57: for x st x on A holds (IncProj(C,b,B)*IncProj(A,a,C)).x = (IncProj(Q,b,
  B)* IncProj(A,q,Q)).x
  proof
A58: {o9,b,oo9} on O2 & {o9,o,a} on O1 by A38,A43,A36,A30,A28,A22,INCSP_1:2;
A59: {o,q,oo9} on O3 & {b,q,a} on O by A18,A49,A23,A25,A24,INCSP_1:2;
A60: O2,O1,C are_mutually_distinct by A2,A4,A38,A30,A55,ZFMISC_1:def 5;
    let x such that
A61: x on A;
A62: {c,o,x} on A by A44,A19,A61,INCSP_1:2;
A63: x in dom f1 by A52,A61;
A64: x in dom f by A27,A61;
    consider Q1 such that
A65: a on Q1 & x on Q1 by INCPROJ:def 5;
    consider x9 being POINT of IPP such that
A66: x9 on Q1 and
A67: x9 on C by INCPROJ:def 9;
A68: {x,a,x9} on Q1 by A65,A66,INCSP_1:2;
A69: {o9,c,x9} on C by A41,A21,A67,INCSP_1:2;
    consider Q2 such that
A70: x9 on Q2 and
A71: b on Q2 by INCPROJ:def 5;
    consider y such that
A72: y on Q and
A73: y on Q2 by INCPROJ:def 9;
A74: {c,y,oo9} on Q by A56,A72,INCSP_1:2;
    {b,y,x9} on Q2 by A70,A71,A73,INCSP_1:2;
    then consider R such that
A75: {y,q,x} on R by A1,A2,A4,A19,A21,A46,A58,A69,A62,A74,A68,A59,A60,
PROJRED1:12;
A76: x on R by A75,INCSP_1:2;
    y on R & q on R by A75,INCSP_1:2;
    then
A77: f1.x = y by A48,A51,A61,A72,A76,PROJRED1:def 1;
    consider x99 being POINT of IPP such that
A78: x99 on Q2 & x99 on B by INCPROJ:def 9;
A79: g1.y = x99 by A3,A5,A71,A78,A72,A73,PROJRED1:def 1;
A80: g.x9 = x99 by A3,A4,A67,A70,A71,A78,PROJRED1:def 1;
    f.x = x9 by A1,A2,A61,A65,A66,A67,PROJRED1:def 1;
    then (g*f).x = g1.(f1.x) by A80,A77,A79,A64,FUNCT_1:13
      .= (g1*f1).x by A63,FUNCT_1:13;
    hence thesis;
  end;
A81: now
    let y be object;
    assume y in X;
    then ex x st y=x & x on A;
    hence (g*f).y = (g1*f1).y by A57;
  end;
  dom (g*f) = X by A1,A2,A3,A4,A27,PROJRED1:22;
  hence thesis by A53,A81,FUNCT_1:2;
end;

theorem Th16:
  not a on A & not a on C & not b on C & not b on Q & not A,B,C
are_concurrent & not B,C,O are_concurrent & A<>Q & Q<>C & a<>b & {c,p} on A & d
on B & {c,d} on C & {a,b,q} on O & {c,pp9} on Q & {a,d,p} on O1 & {q,p,pp9} on
  O2 & {b,d,pp9} on O3 implies q<>a & q<>b & not q on A & not q on Q
proof
  assume that
A1: not a on A and
A2: not a on C and
A3: not b on C and
A4: not b on Q and
A5: not A,B,C are_concurrent and
A6: not B,C,O are_concurrent and
A7: A<>Q and
A8: Q<>C and
A9: a<>b and
A10: {c,p} on A and
A11: d on B and
A12: {c,d} on C and
A13: {a,b,q} on O and
A14: {c,pp9} on Q and
A15: {a,d,p} on O1 and
A16: {q,p,pp9} on O2 and
A17: {b,d,pp9} on O3;
A18: d on C by A12,INCSP_1:1;
A19: c on C by A12,INCSP_1:1;
A20: c on A by A10,INCSP_1:1;
  then
A21: c <>d by A5,A11,A19;
A22: d on O1 by A15,INCSP_1:2;
A23: pp9 on Q by A14,INCSP_1:1;
A24: pp9 on O3 by A17,INCSP_1:2;
A25: pp9 on O2 by A16,INCSP_1:2;
A26: a on O1 by A15,INCSP_1:2;
A27: b on O3 by A17,INCSP_1:2;
A28: d on O3 by A17,INCSP_1:2;
A29: q on O by A13,INCSP_1:2;
A30: b on O by A13,INCSP_1:2;
A31: q<>pp9
  proof
    assume not thesis;
    then O3=O by A4,A30,A29,A27,A24,A23,INCPROJ:def 4;
    hence contradiction by A6,A11,A18,A28;
  end;
A32: pp9 on O2 & q on O2 by A16,INCSP_1:2;
A33: pp9 on Q & p on O2 by A14,A16,INCSP_1:1,2;
A34: p on A by A10,INCSP_1:1;
A35: c on Q by A14,INCSP_1:1;
  then
A36: pp9<>d by A8,A19,A18,A23,A21,INCPROJ:def 4;
A37: O1<>O2
  proof
    assume not thesis;
    then
A38: a on O3 by A26,A22,A25,A28,A24,A36,INCPROJ:def 4;
    a on O & b on O by A13,INCSP_1:2;
    then d on O by A9,A28,A27,A38,INCPROJ:def 4;
    hence contradiction by A6,A11,A18;
  end;
A39: p on O1 by A15,INCSP_1:2;
  then
A40: p<>c by A2,A19,A18,A26,A22,A21,INCPROJ:def 4;
A41: not q on Q
  proof
    assume not thesis;
    then p on Q by A33,A32,A31,INCPROJ:def 4;
    hence contradiction by A7,A20,A35,A34,A40,INCPROJ:def 4;
  end;
A42: a on O by A13,INCSP_1:2;
A43: q<>p
  proof
    assume not thesis;
    then O=O1 by A1,A42,A26,A34,A39,A29,INCPROJ:def 4;
    hence contradiction by A6,A11,A18,A22;
  end;
A44: p on O2 by A16,INCSP_1:2;
  pp9<>c by A3,A19,A18,A28,A27,A24,A21,INCPROJ:def 4;
  then
A45: A<>O2 by A7,A20,A35,A25,A23,INCPROJ:def 4;
A46: q on O2 by A16,INCSP_1:2;
A47: p<>d by A5,A11,A18,A34;
  q<>b
  proof
    assume not thesis;
    then O2=O3 by A4,A46,A25,A27,A24,A23,INCPROJ:def 4;
    hence contradiction by A22,A39,A44,A28,A47,A37,INCPROJ:def 4;
  end;
  hence thesis by A26,A34,A39,A46,A44,A45,A37,A43,A41,INCPROJ:def 4;
end;

theorem Th17:
  not a on A & not a on C & not b on B & not b on C & not b on Q &
not A,B,C are_concurrent & a<>b & A<>Q & {c,o} on A & {o,o99,d} on B & {c,d,o9}
on C & {a,b,d} on O & {c,oo9} on Q & {a,o,o9} on O1 & {b,o9,oo9} on O2 & {o,oo9
  ,q} on O3 & q on O implies not q on A & not q on Q & b<>q
proof
  assume that
A1: not a on A and
A2: not a on C and
A3: not b on B and
A4: not b on C and
A5: not b on Q and
A6: not A,B,C are_concurrent and
A7: a<>b and
A8: A<>Q and
A9: {c,o} on A and
A10: {o,o99,d} on B and
A11: {c,d,o9} on C and
A12: {a,b,d} on O and
A13: {c,oo9} on Q and
A14: {a,o,o9} on O1 and
A15: {b,o9,oo9} on O2 and
A16: {o,oo9,q} on O3 and
A17: q on O;
A18: o on B by A10,INCSP_1:2;
A19: c on A & c on Q by A9,A13,INCSP_1:1;
A20: o on A by A9,INCSP_1:1;
A21: oo9 on O2 by A15,INCSP_1:2;
A22: b on O2 & oo9 on O2 by A15,INCSP_1:2;
A23: oo9 on Q by A13,INCSP_1:1;
A24: b on O2 by A15,INCSP_1:2;
A25: o on O1 by A14,INCSP_1:2;
A26: o on A by A9,INCSP_1:1;
A27: d on C by A11,INCSP_1:2;
  then
A28: o<>d by A6,A26,A18;
A29: d on B by A10,INCSP_1:2;
A30: b on O by A12,INCSP_1:2;
A31: oo9 on Q by A13,INCSP_1:1;
A32: o9 on O2 by A15,INCSP_1:2;
A33: q on O3 by A16,INCSP_1:2;
A34: a on O1 by A14,INCSP_1:2;
A35: d on O by A12,INCSP_1:2;
A36: a on O by A12,INCSP_1:2;
A37: O1<>O2
  proof
    assume not thesis;
    then o on O by A7,A36,A30,A34,A25,A24,INCPROJ:def 4;
    hence contradiction by A3,A18,A29,A30,A35,A28,INCPROJ:def 4;
  end;
A38: o on O3 & oo9 on O3 by A16,INCSP_1:2;
A39: o9 on C by A11,INCSP_1:2;
  then
A40: o<>o9 by A6,A26,A18;
A41: b<>q
  proof
    assume not thesis;
    then
A42: o on O2 by A5,A23,A22,A38,A33,INCPROJ:def 4;
A43: o9 on O2 by A15,INCSP_1:2;
    o on O1 & o9 on O1 by A14,INCSP_1:2;
    hence contradiction by A37,A40,A42,A43,INCPROJ:def 4;
  end;
A44: c on A by A9,INCSP_1:1;
A45: c on C by A11,INCSP_1:2;
  then
A46: o<>c by A6,A44,A18;
A47: o9 on O1 by A14,INCSP_1:2;
  then o9<>c by A1,A44,A26,A34,A25,A46,INCPROJ:def 4;
  then
A48: c <>oo9 by A4,A45,A39,A24,A32,A21,INCPROJ:def 4;
  o9<>d
  proof
    assume not thesis;
    then O1=O by A2,A27,A36,A35,A34,A47,INCPROJ:def 4;
    hence contradiction by A3,A18,A29,A30,A35,A25,A28,INCPROJ:def 4;
  end;
  then O<>O2 by A2,A27,A39,A36,A35,A32,INCPROJ:def 4;
  then
A49: q<>oo9 by A5,A17,A30,A31,A24,A21,INCPROJ:def 4;
A50: c on Q by A13,INCSP_1:1;
A51: not q on Q
  proof
    assume not thesis;
    then o on Q by A23,A38,A33,A49,INCPROJ:def 4;
    hence contradiction by A8,A44,A26,A50,A46,INCPROJ:def 4;
  end;
A52: q<>o by A3,A17,A18,A29,A30,A35,A28,INCPROJ:def 4;
  not q on A
  proof
    assume not thesis;
    then oo9 on A by A20,A38,A33,A52,INCPROJ:def 4;
    hence contradiction by A8,A19,A23,A48,INCPROJ:def 4;
  end;
  hence thesis by A51,A41;
end;

theorem Th18:
  not a on A & not a on C & not b on C & not q on A & not A,B,C
are_concurrent & not B,C,O are_concurrent & a<>b & b<>q & q<>a & {c,p} on A & d
on B & {c,d} on C & {a,b,q} on O & {c,pp9} on Q & {a,d,p} on O1 & {q,p,pp9} on
  O2 & {b,d,pp9} on O3 implies Q<>A & Q<>C & not q on Q & not b on Q
proof
  assume that
A1: not a on A and
A2: not a on C and
A3: not b on C and
A4: not q on A and
A5: not A,B,C are_concurrent and
A6: not B,C,O are_concurrent and
A7: a<>b and
A8: b<>q and
A9: q<>a and
A10: {c,p} on A and
A11: d on B and
A12: {c,d} on C and
A13: {a,b,q} on O and
A14: {c,pp9} on Q and
A15: {a,d,p} on O1 and
A16: {q,p,pp9} on O2 and
A17: {b,d,pp9} on O3;
A18: d on C by A12,INCSP_1:1;
A19: c on C by A12,INCSP_1:1;
A20: c on A by A10,INCSP_1:1;
  then
A21: c <>d by A5,A11,A19;
A22: pp9 on O3 by A17,INCSP_1:2;
A23: p on O2 by A16,INCSP_1:2;
A24: pp9 on Q by A14,INCSP_1:1;
A25: q on O by A13,INCSP_1:2;
A26: a on O by A13,INCSP_1:2;
A27: b on O3 by A17,INCSP_1:2;
A28: d on O1 by A15,INCSP_1:2;
  then
A29: O<>O1 by A6,A11,A18;
A30: p on O1 by A15,INCSP_1:2;
A31: p on O2 by A16,INCSP_1:2;
A32: a on O1 by A15,INCSP_1:2;
A33: pp9 on O2 by A16,INCSP_1:2;
A34: q on O2 by A16,INCSP_1:2;
A35: p on A by A10,INCSP_1:1;
  then
A36: p<>d by A5,A11,A18;
A37: pp9<>d
  proof
    assume not thesis;
    then
A38: q on O1 by A28,A30,A34,A31,A33,A36,INCPROJ:def 4;
    a on O & q on O by A13,INCSP_1:2;
    hence contradiction by A9,A32,A29,A38,INCPROJ:def 4;
  end;
A39: d on O3 by A17,INCSP_1:2;
A40: b on O by A13,INCSP_1:2;
A41: p<>pp9
  proof
    assume not thesis;
    then O1=O3 by A28,A30,A39,A22,A36,INCPROJ:def 4;
    hence contradiction by A7,A26,A40,A32,A27,A29,INCPROJ:def 4;
  end;
A42: c on Q by A14,INCSP_1:1;
  then
A43: O3<>Q by A3,A19,A18,A39,A27,A21,INCPROJ:def 4;
A44: not b on Q
  proof
    assume not thesis;
    then
A45: b on O2 by A33,A27,A22,A24,A43,INCPROJ:def 4;
A46: q on O by A13,INCSP_1:2;
    q on O2 & b on O by A13,A16,INCSP_1:2;
    then p on O by A8,A23,A45,A46,INCPROJ:def 4;
    hence contradiction by A1,A26,A32,A35,A30,A29,INCPROJ:def 4;
  end;
  p<>c by A2,A19,A18,A32,A28,A30,A21,INCPROJ:def 4;
  then
A47: O2<>Q by A4,A20,A42,A35,A34,A31,INCPROJ:def 4;
A48: O<>O3 by A6,A11,A18,A39;
  not q on Q
  proof
    assume not thesis;
    then q=pp9 by A34,A33,A24,A47,INCPROJ:def 4;
    hence contradiction by A8,A40,A25,A27,A22,A48,INCPROJ:def 4;
  end;
  hence thesis by A18,A35,A34,A31,A33,A39,A27,A22,A24,A41,A37,A44,INCPROJ:def 4
;
end;

theorem Th19:
  not a on A & not a on C & not b on B & not b on C & not q on A &
not A,B,C are_concurrent & a<>b & b<>q & {c,o} on A & {o,o99,d} on B & {c,d,o9}
on C & {a,b,d} on O & {c,oo9} on Q & {a,o,o9} on O1 & {b,o9,oo9} on O2 & {o,oo9
  ,q} on O3 & q on O implies not b on Q & not q on Q & A<>Q
proof
  assume that
A1: not a on A and
A2: not a on C and
A3: not b on B and
A4: not b on C and
A5: not q on A and
A6: not A,B,C are_concurrent and
A7: a<>b and
A8: b<>q and
A9: {c,o} on A and
A10: {o,o99,d} on B and
A11: {c,d,o9} on C and
A12: {a,b,d} on O and
A13: {c,oo9} on Q and
A14: {a,o,o9} on O1 and
A15: {b,o9,oo9} on O2 and
A16: {o,oo9,q} on O3 and
A17: q on O;
A18: o on A by A9,INCSP_1:1;
A19: d on B & d on O by A10,A12,INCSP_1:2;
A20: o on B by A10,INCSP_1:2;
A21: o on B by A10,INCSP_1:2;
A22: d on C by A11,INCSP_1:2;
  then
A23: o<>d by A6,A18,A21;
A24: o on O3 by A16,INCSP_1:2;
A25: b<>oo9
  proof
    assume not thesis;
    then
A26: b on O3 by A16,INCSP_1:2;
    q on O3 & b on O by A12,A16,INCSP_1:2;
    then o on O by A8,A17,A24,A26,INCPROJ:def 4;
    then O=B by A19,A20,A23,INCPROJ:def 4;
    hence contradiction by A3,A12,INCSP_1:2;
  end;
A27: oo9 on O2 by A15,INCSP_1:2;
A28: C<>O2 by A4,A15,INCSP_1:2;
A29: o9 on O1 by A14,INCSP_1:2;
A30: oo9 on O2 by A15,INCSP_1:2;
A31: oo9 on Q by A13,INCSP_1:1;
A32: c on Q & b on O2 by A13,A15,INCSP_1:1,2;
A33: c on A by A9,INCSP_1:1;
A34: a on O1 by A14,INCSP_1:2;
A35: b on O by A12,INCSP_1:2;
A36: o on O1 by A14,INCSP_1:2;
  c on C by A11,INCSP_1:2;
  then
A37: o<>c by A6,A33,A21;
  then
A38: o9<>c by A1,A33,A18,A34,A36,A29,INCPROJ:def 4;
A39: not b on Q
  proof
    assume not thesis;
    then
A40: c on O2 by A32,A31,A30,A25,INCPROJ:def 4;
A41: o9 on O2 by A15,INCSP_1:2;
    o9 on C & c on C by A11,INCSP_1:2;
    hence contradiction by A38,A28,A41,A40,INCPROJ:def 4;
  end;
A42: c on Q by A13,INCSP_1:1;
A43: o9 on C by A11,INCSP_1:2;
A44: a on O by A12,INCSP_1:2;
A45: b on O2 by A15,INCSP_1:2;
A46: O1<>O2
  proof
    assume not thesis;
    then o on O by A7,A44,A35,A34,A36,A45,INCPROJ:def 4;
    then O=B by A19,A20,A23,INCPROJ:def 4;
    hence contradiction by A3,A12,INCSP_1:2;
  end;
A47: o on O3 & q on O3 by A16,INCSP_1:2;
A48: oo9 on Q & oo9 on O3 by A13,A16,INCSP_1:1,2;
A49: o9 on O2 by A15,INCSP_1:2;
A50: oo9 on O3 & q on O3 by A16,INCSP_1:2;
A51: d on O by A12,INCSP_1:2;
A52: d on B by A10,INCSP_1:2;
  o9<>d
  proof
    assume not thesis;
    then O1=O by A2,A22,A44,A51,A34,A29,INCPROJ:def 4;
    hence contradiction by A3,A21,A52,A35,A51,A36,A23,INCPROJ:def 4;
  end;
  then O<>O2 by A2,A22,A43,A44,A51,A49,INCPROJ:def 4;
  then
A53: q<>oo9 by A8,A17,A35,A45,A27,INCPROJ:def 4;
A54: not q on Q
  proof
    assume not thesis;
    then Q=O3 by A31,A50,A53,INCPROJ:def 4;
    hence contradiction by A5,A33,A18,A42,A47,A37,INCPROJ:def 4;
  end;
  o<>o9 by A6,A18,A21,A43;
  then o<>oo9 by A36,A29,A49,A27,A46,INCPROJ:def 4;
  hence thesis by A18,A48,A47,A39,A54,INCPROJ:def 4;
end;

Lm1: not a on A & not b on B & not a on C & not b on C & not A,B,C
are_concurrent & A,C,Q are_concurrent & not b on Q & A<>Q & a<>b & a on O & b
on O & not B,C,O are_concurrent implies ex q st q on O & not q on A & not q on
Q & IncProj(C,b,B)*IncProj(A,a,C) = IncProj(Q,b,B)*IncProj(A,q,Q)
proof
  assume that
A1: not a on A and
A2: not b on B and
A3: not a on C and
A4: ( not b on C)& not A,B,C are_concurrent and
A5: A,C,Q are_concurrent and
A6: ( not b on Q)& A<>Q and
A7: a<>b and
A8: a on O and
A9: b on O and
A10: not B,C,O are_concurrent;
  consider c such that
A11: c on A & c on C and
A12: c on Q by A5;
  consider d such that
A13: d on C and
A14: d on B by INCPROJ:def 9;
  consider O1 such that
A15: a on O1 & d on O1 by INCPROJ:def 5;
  consider O3 such that
A16: b on O3 & d on O3 by INCPROJ:def 5;
  consider pp9 being POINT of IPP such that
A17: pp9 on O3 and
A18: pp9 on Q by INCPROJ:def 9;
  consider p such that
A19: p on A and
A20: p on O1 by INCPROJ:def 9;
  consider O2 such that
A21: p on O2 & pp9 on O2 by INCPROJ:def 5;
  consider q such that
A22: q on O and
A23: q on O2 by INCPROJ:def 9;
  now
    assume
A24: Q<>C;
    take q;
A25: {b,d,pp9} on O3 by A16,A17,INCSP_1:2;
A26: {a,d,p} on O1 & {q,p,pp9} on O2 by A15,A20,A21,A23,INCSP_1:2;
A27: {c,p} on A & {c,d} on C by A11,A13,A19,INCSP_1:1;
A28: {a,b,q} on O & {c,pp9} on Q by A8,A9,A12,A18,A22,INCSP_1:1,2;
    then
A29: ( not q on A)& not q on Q by A1,A3,A4,A6,A7,A10,A14,A24,A27,A26,A25,Th16;
    q<>a by A1,A3,A4,A6,A7,A10,A14,A24,A27,A28,A26,A25,Th16;
    then IncProj(C,b,B)*IncProj(A,a,C) = IncProj(Q,b,B)*IncProj(A,q,Q) by A1,A2
,A3,A4,A6,A8,A9,A10,A11,A12,A13,A14,A15,A16,A19,A20,A17,A18,A21,A22,A23,A29
,Th14;
    hence thesis by A22,A29;
  end;
  hence thesis by A1,A3,A8;
end;

Lm2: not a on A & not b on B & not a on C & not b on C & not A,B,C
are_concurrent & A,C,Q are_concurrent & not b on Q & A<>Q & a<>b & a on O & b
on O & B,C,O are_concurrent implies ex q st q on O & not q on A & not q on Q &
IncProj(C,b,B)*IncProj(A,a,C) = IncProj(Q,b,B)*IncProj(A,q,Q)
proof
  assume that
A1: ( not a on A)& not b on B & ( not a on C)& not b on C & not A,B,C
  are_concurrent and
A2: A,C,Q are_concurrent and
A3: ( not b on Q)& A<>Q & a<>b and
A4: a on O & b on O and
A5: B,C,O are_concurrent;
  consider d such that
A6: d on B and
A7: d on C and
A8: d on O by A5;
A9: {a,b,d} on O by A4,A8,INCSP_1:2;
  consider o such that
A10: o on A and
A11: o on B by INCPROJ:def 9;
  consider O1 such that
A12: o on O1 & a on O1 by INCPROJ:def 5;
  consider o9 being POINT of IPP such that
A13: o9 on C and
A14: o9 on O1 by INCPROJ:def 9;
A15: {a,o,o9} on O1 by A12,A14,INCSP_1:2;
  consider c such that
A16: c on A and
A17: c on C and
A18: c on Q by A2;
A19: {c,o} on A by A16,A10,INCSP_1:1;
A20: {c,d,o9} on C by A17,A7,A13,INCSP_1:2;
A21: {c,o} on A by A16,A10,INCSP_1:1;
A22: {c,d,o9} on C by A17,A7,A13,INCSP_1:2;
  consider O2 such that
A23: b on O2 & o9 on O2 by INCPROJ:def 5;
  consider oo9 being POINT of IPP such that
A24: oo9 on Q and
A25: oo9 on O2 by INCPROJ:def 9;
A26: {b,o9,oo9} on O2 by A23,A25,INCSP_1:2;
  consider o99 being POINT of IPP such that
A27: o99 on B and
  o99 on O2 by INCPROJ:def 9;
  consider O3 such that
A28: o on O3 & oo9 on O3 by INCPROJ:def 5;
A29: {o,o99,d} on B by A6,A11,A27,INCSP_1:2;
A30: {b,o9,oo9} on O2 by A23,A25,INCSP_1:2;
A31: {a,o,o9} on O1 by A12,A14,INCSP_1:2;
A32: {a,b,d} on O by A4,A8,INCSP_1:2;
  consider q such that
A33: q on O3 and
A34: q on O by INCPROJ:def 9;
A35: {o,oo9,q} on O3 by A28,A33,INCSP_1:2;
A36: {c,oo9} on Q by A18,A24,INCSP_1:1;
A37: {o,o99,d} on B by A6,A11,A27,INCSP_1:2;
  then
A38: ( not q on A)& not q on Q by A1,A3,A34,A19,A22,A9,A36,A15,A26,A35,Th17;
A39: {o,oo9,q} on O3 by A28,A33,INCSP_1:2;
A40: {c,oo9} on Q by A18,A24,INCSP_1:1;
  b<>q by A1,A3,A34,A19,A37,A22,A9,A36,A15,A26,A35,Th17;
  then IncProj(C,b,B)*IncProj(A,a,C) = IncProj(Q,b,B)*IncProj(A,q,Q) by A1,A3
,A34,A21,A29,A20,A32,A40,A31,A30,A39,Th15;
  hence thesis by A34,A38;
end;

theorem Th20:
  not a on A & not b on B & not a on C & not b on C & not A,B,C
  are_concurrent & A,C,Q are_concurrent & not b on Q & A<>Q & a<>b & a on O & b
on O implies ex q st q on O & not q on A & not q on Q & IncProj(C,b,B)*IncProj(
  A,a,C) = IncProj(Q,b,B)*IncProj(A,q,Q)
proof
  assume
A1: ( not a on A)& not b on B & ( not a on C)& not b on C & ( not A,B,C
are_concurrent)& A,C,Q are_concurrent & ( not b on Q)& A<>Q & a<>b & a on O & b
  on O;
  then not B,C,O are_concurrent implies thesis by Lm1;
  hence thesis by A1,Lm2;
end;

theorem
  not a on A & not b on B & not a on C & not b on C & not A,B,C
  are_concurrent & B,C,Q are_concurrent & not a on Q & B<>Q & a<>b & a on O & b
on O implies ex q st q on O & not q on B & not q on Q & IncProj(C,b,B)*IncProj(
  A,a,C) = IncProj(Q,q,B)*IncProj(A,a,Q)
proof
  assume that
A1: not a on A and
A2: not b on B and
A3: not a on C and
A4: not b on C and
A5: not A,B,C are_concurrent and
A6: B,C,Q are_concurrent and
A7: not a on Q and
A8: B<>Q & a<>b & a on O & b on O;
A9: IncProj(B,b,C) is one-to-one & IncProj(C,a,A) is one-to-one by A1,A2,A3,A4
,Th7;
  not B,A,C are_concurrent
  by A5;
  then consider q such that
A10: q on O and
A11: ( not q on B)& not q on Q and
A12: IncProj(C,a,A)*IncProj(B,b,C) = IncProj(Q,a,A)*IncProj (B,q,Q) by A1,A2,A3
,A4,A6,A7,A8,Th20;
  take q;
  thus q on O & not q on B & not q on Q by A10,A11;
A13: IncProj(B,q,Q) is one-to-one by A11,Th7;
A14: IncProj(Q,a,A) is one-to-one by A1,A7,Th7;
  thus IncProj(C,b,B)*IncProj(A,a,C) = IncProj(B,b,C)"*IncProj(A,a,C) by A2,A4
,Th8
    .= IncProj(B,b,C)"*IncProj(C,a,A)" by A1,A3,Th8
    .= (IncProj(Q,a,A)*IncProj (B,q,Q))" by A12,A9,FUNCT_1:44
    .= (IncProj(B,q,Q))"*(IncProj(Q,a,A))" by A13,A14,FUNCT_1:44
    .= IncProj(Q,q,B)*(IncProj(Q,a,A))" by A11,Th8
    .= IncProj (Q,q,B)*IncProj(A,a,Q) by A1,A7,Th8;
end;

theorem
  not a on A & not b on B & not a on C & not b on C & not a on B & not b
on A & c on A & c on C & d on B & d on C & a on S & d on S & c on R & b on R &
s on A & s on S & r on B & r on R & s on Q & r on Q & not A,B,C are_concurrent
  implies IncProj(C,b,B)*IncProj(A,a,C) = IncProj(Q,a,B)*IncProj(A,b,Q)
proof
  assume that
A1: not a on A and
A2: not b on B and
A3: not a on C and
A4: not b on C and
A5: not a on B and
A6: not b on A and
A7: c on A and
A8: c on C and
A9: d on B and
A10: d on C and
A11: a on S and
A12: d on S and
A13: c on R and
A14: b on R and
A15: s on A and
A16: s on S and
A17: r on B and
A18: r on R and
A19: s on Q and
A20: r on Q and
A21: not A,B,C are_concurrent;
A22: c <>d by A7,A8,A9,A21;
  then
A23: c <>s by A3,A8,A10,A11,A12,A16,INCPROJ:def 4;
A24: now
    assume b on Q;
    then R=Q by A2,A14,A17,A18,A20,INCPROJ:def 4;
    hence contradiction by A6,A7,A13,A14,A15,A19,A23,INCPROJ:def 4;
  end;
A25: d<>r by A4,A8,A10,A13,A14,A18,A22,INCPROJ:def 4;
A26: now
    assume a on Q;
    then S=Q by A1,A11,A15,A16,A19,INCPROJ:def 4;
    hence contradiction by A5,A9,A11,A12,A17,A20,A25,INCPROJ:def 4;
  end;
  set X = CHAIN(A);
  set f=IncProj(A,a,C),g=IncProj(C,b,B),g1=IncProj(Q,a,B),f1=IncProj(A,b,Q);
A27: dom f= CHAIN(A) by A1,A3,Th4;
A28: dom f1 = CHAIN(A) by A6,A24,Th4;
  then
A29: dom (g1*f1) = X by A5,A6,A26,A24,PROJRED1:22;
  A<>C by A21,Th1;
  then
A30: C,A,R are_mutually_distinct by A4,A6,A14,ZFMISC_1:def 5;
A31: c <>d by A7,A8,A9,A21;
A32: for x st x on A holds (IncProj(C,b,B)*IncProj(A,a,C)).x = (IncProj(Q,a,
  B)* IncProj(A,b,Q)).x
  proof
    let x;
    assume
A33: x on A;
    then reconsider x9=f.x,y=f1.x as POINT of IPP by A1,A3,A6,A24,PROJRED1:19;
A34: x in dom f1 by A28,A33;
A35: x9 on C by A1,A3,A33,PROJRED1:20;
    then reconsider x99=g.x9 as POINT of IPP by A2,A4,PROJRED1:19;
    consider O1 such that
A36: a on O1 & x on O1 & x9 on O1 by A1,A3,A33,A35,PROJRED1:def 1;
A37: y on Q by A6,A24,A33,PROJRED1:20;
    then consider O3 such that
A38: b on O3 & x on O3 & y on O3 by A6,A24,A33,PROJRED1:def 1;
A39: x99 on B by A2,A4,A35,PROJRED1:20;
    then consider O2 such that
A40: b on O2 & x9 on O2 & x99 on O2 by A2,A4,A35,PROJRED1:def 1;
A41: now
A42:  {y,s,r} on Q & {d,x99,r} on B by A9,A17,A19,A20,A37,A39,INCSP_1:2;
      assume
A43:  s<>x;
A44:  {d,a,s} on S by A11,A12,A16,INCSP_1:2;
A45:  {c,b,r} on R & {b,x,y} on O3 by A13,A14,A18,A38,INCSP_1:2;
A46:  {b,x99,x9} on O2 & {x,a,x9} on O1 by A36,A40,INCSP_1:2;
      {c,d,x9} on C & {c,x,s} on A by A7,A8,A10,A15,A33,A35,INCSP_1:2;
      then consider O4 such that
A47:  {x99,a,y} on O4 by A6,A7,A31,A23,A30,A43,A45,A46,A42,A44,PROJRED1:12;
A48:  y on O4 by A47,INCSP_1:2;
      x99 on O4 & a on O4 by A47,INCSP_1:2;
      hence g.(f.x) = g1.(f1.x) by A5,A26,A37,A39,A48,PROJRED1:def 1;
    end;
A49: now
      assume
A50:  s=x;
      then x9=d by A1,A3,A10,A11,A12,A15,A16,PROJRED1:def 1;
      then
A51:  x99=d by A2,A4,A9,A10,PROJRED1:24;
      y=s by A6,A15,A19,A24,A50,PROJRED1:24;
      hence g.(f.x) = g1.(f1.x) by A5,A9,A11,A12,A16,A19,A26,A51,PROJRED1:def 1
;
    end;
    x in dom f by A27,A33;
    then (g*f).x = g1.(f1.x) by A49,A41,FUNCT_1:13
      .= (g1*f1).x by A34,FUNCT_1:13;
    hence thesis;
  end;
A52: now
    let y be object;
    assume y in X;
    then ex x st y=x & x on A;
    hence (g*f) . y = (g1*f1).y by A32;
  end;
  dom (g*f) = X by A1,A2,A3,A4,A27,PROJRED1:22;
  hence thesis by A29,A52,FUNCT_1:2;
end;

Lm3: not a on A & not b on B & not a on C & not b on C & c on A & c on C & a<>
b & a on O & b on O & q on O & not q on A & q<>b & not A,B,C are_concurrent &
not B,C,O are_concurrent implies ex Q st c on Q & not b on Q & not q on Q &
IncProj(C,b,B)*IncProj(A,a,C) = IncProj(Q,b,B)*IncProj(A,q,Q)
proof
  assume that
A1: not a on A and
A2: not b on B and
A3: ( not a on C)& not b on C and
A4: c on A and
A5: c on C and
A6: a<>b and
A7: a on O & b on O & q on O and
A8: not q on A and
A9: q<>b and
A10: ( not A,B,C are_concurrent)& not B,C,O are_concurrent;
  consider d such that
A11: d on C and
A12: d on B by INCPROJ:def 9;
  consider O1 such that
A13: a on O1 & d on O1 by INCPROJ:def 5;
  consider O3 such that
A14: b on O3 & d on O3 by INCPROJ:def 5;
  consider p such that
A15: p on A and
A16: p on O1 by INCPROJ:def 9;
  consider O2 such that
A17: q on O2 & p on O2 by INCPROJ:def 5;
  consider pp9 being POINT of IPP such that
A18: pp9 on O3 and
A19: pp9 on O2 by INCPROJ:def 9;
  consider Q such that
A20: c on Q and
A21: pp9 on Q by INCPROJ:def 5;
  now
A22: {a,b,q} on O & {c,pp9} on Q by A7,A20,A21,INCSP_1:1,2;
A23: {b,d,pp9} on O3 by A14,A18,INCSP_1:2;
A24: {a,d,p} on O1 & {q,p,pp9} on O2 by A13,A16,A17,A19,INCSP_1:2;
    assume
A25: q<>a;
A26: {c,p} on A & {c,d} on C by A4,A5,A11,A15,INCSP_1:1;
    then
A27: ( not q on Q)& not b on Q by A1,A3,A6,A8,A9,A10,A12,A25,A22,A24,A23,Th18;
    Q<>A by A1,A3,A6,A8,A9,A10,A12,A25,A26,A22,A24,A23,Th18;
    then
    IncProj(C,b,B)*IncProj(A,a,C) = IncProj(Q,b,B)*IncProj (A,q,Q) by A1,A2,A3
,A4,A5,A7,A8,A10,A11,A12,A13,A14,A15,A16,A17,A18,A19,A20,A21,A25,A27,Th14;
    hence thesis by A20,A27;
  end;
  hence thesis by A3,A5;
end;

Lm4: not a on A & not b on B & not a on C & not b on C & c on A & c on C & a<>
b & a on O & b on O & q on O & not q on A & q<>b & not A,B,C are_concurrent & B
,C,O are_concurrent implies ex Q st c on Q & not b on Q & not q on Q & IncProj(
C,b,B)*IncProj(A,a,C) = IncProj(Q,b,B)*IncProj(A,q,Q)
proof
  assume that
A1: ( not a on A)& not b on B & ( not a on C)& not b on C and
A2: c on A and
A3: c on C and
A4: a<>b and
A5: a on O & b on O and
A6: q on O and
A7: not q on A and
A8: q<>b & not A,B,C are_concurrent and
A9: B,C,O are_concurrent;
  consider d such that
A10: d on B and
A11: d on C and
A12: d on O by A9;
A13: {a,b,d} on O by A5,A12,INCSP_1:2;
  consider o such that
A14: o on A and
A15: o on B by INCPROJ:def 9;
  consider O1 such that
A16: o on O1 & a on O1 by INCPROJ:def 5;
  consider o9 being POINT of IPP such that
A17: o9 on C and
A18: o9 on O1 by INCPROJ:def 9;
A19: {a,o,o9} on O1 by A16,A18,INCSP_1:2;
A20: {a,o,o9} on O1 by A16,A18,INCSP_1:2;
A21: {c,d,o9} on C by A3,A11,A17,INCSP_1:2;
A22: {c,d,o9} on C by A3,A11,A17,INCSP_1:2;
  consider O2 such that
A23: b on O2 & o9 on O2 by INCPROJ:def 5;
A24: {a,b,d} on O by A5,A12,INCSP_1:2;
A25: {c,o} on A by A2,A14,INCSP_1:1;
A26: {c,o} on A by A2,A14,INCSP_1:1;
  consider O3 such that
A27: q on O3 & o on O3 by INCPROJ:def 5;
  consider o99 being POINT of IPP such that
A28: o99 on B and
  o99 on O2 by INCPROJ:def 9;
A29: {o,o99,d} on B by A10,A15,A28,INCSP_1:2;
  consider oo9 being POINT of IPP such that
A30: oo9 on O2 and
A31: oo9 on O3 by INCPROJ:def 9;
A32: {b,o9,oo9} on O2 by A23,A30,INCSP_1:2;
A33: {o,oo9,q} on O3 by A27,A31,INCSP_1:2;
A34: {o,oo9,q} on O3 by A27,A31,INCSP_1:2;
A35: {b,o9,oo9} on O2 by A23,A30,INCSP_1:2;
  consider Q such that
A36: c on Q and
A37: oo9 on Q by INCPROJ:def 5;
A38: {c,oo9} on Q by A36,A37,INCSP_1:1;
A39: {c,oo9} on Q by A36,A37,INCSP_1:1;
A40: {o,o99,d} on B by A10,A15,A28,INCSP_1:2;
  then ( not b on Q)& A<>Q by A1,A4,A6,A7,A8,A25,A21,A13,A38,A19,A32,A34,Th19;
  then
A41: IncProj(C,b,B)*IncProj(A,a,C) = IncProj(Q,b,B)*IncProj(A,q,Q) by A1,A4,A6
,A8,A26,A29,A22,A24,A39,A20,A35,A33,Th15;
  ( not b on Q)& not q on Q by A1,A4,A6,A7,A8,A25,A40,A21,A13,A38,A19,A32,A34
,Th19;
  hence thesis by A36,A41;
end;

theorem Th23:
  not a on A & not b on B & not a on C & not b on C & a<>b & a on
O & b on O & q on O & not q on A & q<>b & not A,B,C are_concurrent implies ex Q
st A,C,Q are_concurrent & not b on Q & not q on Q & IncProj(C,b,B)*IncProj(A,a,
  C) = IncProj(Q,b,B)* IncProj(A,q,Q)
proof
  consider c such that
A1: c on A & c on C by INCPROJ:def 9;
  assume
A2: ( not a on A)& not b on B & ( not a on C)& not b on C & a<>b & a on
  O & b on O & q on O & ( not q on A)& q<>b & not A,B,C are_concurrent;
A3: now
    assume B,C,O are_concurrent;
    then consider Q such that
A4: c on Q and
A5: ( not b on Q)& not q on Q & IncProj(C,b,B)*IncProj(A,a,C) =
    IncProj(Q,b,B) *IncProj(A,q,Q) by A2,A1,Lm4;
    take Q;
    thus A,C,Q are_concurrent by A1,A4;
    thus not b on Q & not q on Q & IncProj(C,b,B)*IncProj(A,a,C) = IncProj(Q,b
    ,B) * IncProj(A,q,Q) by A5;
  end;
  now
    assume not B,C,O are_concurrent;
    then consider Q such that
A6: c on Q and
A7: ( not b on Q)& not q on Q & IncProj(C,b,B)*IncProj(A,a,C) =
    IncProj(Q,b,B) *IncProj(A,q,Q) by A2,A1,Lm3;
    take Q;
    thus A,C,Q are_concurrent by A1,A6;
    thus not b on Q & not q on Q & IncProj(C,b,B)*IncProj(A,a,C) = IncProj(Q,b
    ,B)* IncProj(A,q,Q) by A7;
  end;
  hence thesis by A3;
end;

theorem
  not a on A & not b on B & not a on C & not b on C & a<>b & a on O & b
on O & q on O & not q on B & q<>a & not A,B,C are_concurrent implies ex Q st B,
C,Q are_concurrent & not a on Q & not q on Q & IncProj(C,b,B)*IncProj(A,a,C) =
  IncProj(Q,q,B)* IncProj(A,a,Q)
proof
  assume that
A1: not a on A and
A2: not b on B and
A3: not a on C and
A4: not b on C and
A5: a<>b & a on O & b on O & q on O and
A6: not q on B and
A7: q<>a and
A8: not A,B,C are_concurrent;
A9: IncProj(C,a,A) is one-to-one & IncProj(B,b,C) is one-to-one by A1,A2,A3,A4
,Th7;
  not B,A,C are_concurrent
  by A8;
  then consider Q such that
A10: B,C,Q are_concurrent and
A11: not a on Q and
A12: not q on Q and
A13: IncProj(C,a,A)*IncProj(B,b,C) = IncProj(Q,a,A)*IncProj (B,q,Q) by A1,A2,A3
,A4,A5,A6,A7,Th23;
A14: IncProj(Q,a,A) is one-to-one & IncProj(B,q,Q) is one-to-one by A1,A6,A11
,A12,Th7;
  take Q;
  thus B,C,Q are_concurrent & not a on Q & not q on Q by A10,A11,A12;
  thus IncProj(C,b,B)*IncProj(A,a,C) = IncProj(B,b,C)"*IncProj (A,a,C) by A2,A4
,Th8
    .= IncProj(B,b,C)"*IncProj(C,a,A)" by A1,A3,Th8
    .= (IncProj(Q,a,A)*IncProj (B,q,Q))" by A13,A9,FUNCT_1:44
    .= IncProj(B,q,Q)"*IncProj(Q,a,A)" by A14,FUNCT_1:44
    .= IncProj(B,q,Q)"*IncProj(A,a,Q) by A1,A11,Th8
    .= IncProj(Q,q,B)*IncProj (A,a,Q) by A6,A12,Th8;
end;