:: PROJRED2 semantic presentation

begin


definition
let IPS be IncProjSp;
let A, B, C be LINE of IPS;
predA,B,C are_concurrent  means :Def1: :: PROJRED2:def 1
 ex o being Element of the Points of IPS st
( o on A & o on B & o on C );
end;

:: deftheorem Def1 defines are_concurrent PROJRED2:def_1_:_
 for IPS being IncProjSp
for A, B, C being LINE of IPS holds
( A,B,C are_concurrent iff ex o being Element of the Points of IPS st
( o on A & o on B & o on C ) );

definition
let IPS be IncProjSp;
let Z be LINE of IPS;
func CHAIN Z ->  Subset of the Points of IPS equals :: PROJRED2:def 2
 {  z where z is POINT of IPS : z on Z  }  ;
correctness
coherence
{  z where z is POINT of IPS : z on Z  }  is Subset of the Points of IPS;
proof
set X =  {  z where z is POINT of IPS : z on Z  }  ;
now__::_thesis:_for_x_being_set_st_x_in__{__z_where_z_is_POINT_of_IPS_:_z_on_Z__}__holds_
x_in_the_Points_of_IPS
let x be set ; ::_thesis: ( x in  {  z where z is POINT of IPS : z on Z  }  implies x in the Points of IPS )
assume  x in  {  z where z is POINT of IPS : z on Z  }  ; ::_thesis: x in the Points of IPS
then  ex z being POINT of IPS st
( z = x & z on Z ) ;
hence  x in the Points of IPS ; ::_thesis: verum
end;
hence   {  z where z is POINT of IPS : z on Z  }  is Subset of the Points of IPS by TARSKI:def_3; ::_thesis: verum
end;
end;

:: deftheorem  defines CHAIN PROJRED2:def_2_:_
 for IPS being IncProjSp
for Z being LINE of IPS holds CHAIN Z =  {  z where z is POINT of IPS : z on Z  }  ;


definition
let IPP be 2-dimensional Desarguesian IncProjSp;
mode Projection of IPP ->  PartFunc of the Points of IPP, the Points of IPP means :Def3: :: PROJRED2:def 3
 ex a being POINT of IPP ex A, B being LINE of IPP st
( not a on A & not a on B & it = IncProj (A,a,B) );
existence
 ex b1 being PartFunc of the Points of IPP, the Points of IPP ex a being POINT of IPP ex A, B being LINE of IPP st
( not a on A & not a on B & b1 = IncProj (A,a,B) )
proof
set A = the LINE of IPP;
consider a being POINT of IPP such that
A1: ( not a on the LINE of IPP & not a on the LINE of IPP ) by PROJRED1:6;
take  IncProj ( the LINE of IPP,a, the LINE of IPP) ; ::_thesis: ex a being POINT of IPP ex A, B being LINE of IPP st
( not a on A & not a on B & IncProj ( the LINE of IPP,a, the LINE of IPP) = IncProj (A,a,B) )
thus  ex a being POINT of IPP ex A, B being LINE of IPP st
( not a on A & not a on B & IncProj ( the LINE of IPP,a, the LINE of IPP) = IncProj (A,a,B) ) by A1; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines Projection PROJRED2:def_3_:_
 for IPP being 2-dimensional Desarguesian IncProjSp
for b2 being PartFunc of the Points of IPP, the Points of IPP holds
( b2 is Projection of IPP iff ex a being POINT of IPP ex A, B being LINE of IPP st
( not a on A & not a on B & b2 = IncProj (A,a,B) ) );

theorem Th1: :: PROJRED2:1
for IPP being 2-dimensional Desarguesian IncProjSp
for A, B, C being LINE of IPP st ( A = B or B = C or C = A ) holds
A,B,C are_concurrent
proof
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for A, B, C being LINE of IPP st ( A = B or B = C or C = A ) holds
A,B,C are_concurrent
let A, B, C be LINE of IPP; ::_thesis: ( ( A = B or B = C or C = A ) implies A,B,C are_concurrent )
A1: ( ex a being POINT of IPP st
( a on B & a on C ) & ex b being POINT of IPP st
( b on C & b on A ) ) by INCPROJ:def_9;
assume  ( A = B or B = C or C = A ) ; ::_thesis: A,B,C are_concurrent
hence  A,B,C are_concurrent by A1, Def1; ::_thesis: verum
end;

theorem :: PROJRED2:2
for IPP being 2-dimensional Desarguesian IncProjSp
for A, B, C being LINE of IPP st A,B,C are_concurrent holds
( 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 )
proof
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for A, B, C being LINE of IPP st A,B,C are_concurrent holds
( 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 )
let A, B, C be LINE of IPP; ::_thesis: ( 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 ) )
assume  A,B,C are_concurrent ; ::_thesis: ( 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 )
then  ex o being POINT of IPP st
( o on A & o on B & o on C ) by Def1;
hence  ( 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 ) by Def1; ::_thesis: verum
end;

theorem Th3: :: PROJRED2:3
for IPP being 2-dimensional Desarguesian IncProjSp
for o, y being POINT of IPP
for A, B being LINE of IPP st not o on A & not o on B & y on B holds
ex x being POINT of IPP st
( x on A & (IncProj (A,o,B)) . x = y )
proof
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for o, y being POINT of IPP
for A, B being LINE of IPP st not o on A & not o on B & y on B holds
ex x being POINT of IPP st
( x on A & (IncProj (A,o,B)) . x = y )
let o, y be POINT of IPP; ::_thesis: for A, B being LINE of IPP st not o on A & not o on B & y on B holds
ex x being POINT of IPP st
( x on A & (IncProj (A,o,B)) . x = y )
let A, B be LINE of IPP; ::_thesis: ( not o on A & not o on B & y on B implies ex x being POINT of IPP st
( x on A & (IncProj (A,o,B)) . x = y ) )
consider X being LINE of IPP such that
A1: ( o on X & y on X ) by INCPROJ:def_5;
consider x being POINT of IPP 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 ) ; ::_thesis: ex x being POINT of IPP st
( x on A & (IncProj (A,o,B)) . x = y )
then  (IncProj (A,o,B)) . x = y by A1, A2, A3, PROJRED1:def_1;
hence  ex x being POINT of IPP st
( x on A & (IncProj (A,o,B)) . x = y ) by A3; ::_thesis: verum
end;

theorem Th4: :: PROJRED2:4
for IPP being 2-dimensional Desarguesian IncProjSp
for o being POINT of IPP
for A, B being LINE of IPP st not o on A & not o on B holds
dom (IncProj (A,o,B)) = CHAIN A
proof
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for o being POINT of IPP
for A, B being LINE of IPP st not o on A & not o on B holds
dom (IncProj (A,o,B)) = CHAIN A
let o be POINT of IPP; ::_thesis: for A, B being LINE of IPP st not o on A & not o on B holds
dom (IncProj (A,o,B)) = CHAIN A
let A, B be LINE of IPP; ::_thesis: ( not o on A & not o on B implies dom (IncProj (A,o,B)) = CHAIN A )
assume A1: ( not o on A & not o on B ) ; ::_thesis: dom (IncProj (A,o,B)) = CHAIN A
A2: now__::_thesis:_for_x_being_set_st_x_in_dom_(IncProj_(A,o,B))_holds_
x_in_CHAIN_A
let x be set ; ::_thesis: ( x in dom (IncProj (A,o,B)) implies x in CHAIN A )
assume A3: x in dom (IncProj (A,o,B)) ; ::_thesis: x in CHAIN A
then reconsider x9 = x as POINT of IPP ;
 x9 on A by A1, A3, PROJRED1:def_1;
hence  x in CHAIN A ; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_CHAIN_A_holds_
x_in_dom_(IncProj_(A,o,B))
let x be set ; ::_thesis: ( x in CHAIN A implies x in dom (IncProj (A,o,B)) )
assume  x in CHAIN A ; ::_thesis: x in dom (IncProj (A,o,B))
then  ex b being POINT of IPP st
( b = x & b on A ) ;
hence  x in dom (IncProj (A,o,B)) by A1, PROJRED1:def_1; ::_thesis: verum
end;
hence  dom (IncProj (A,o,B)) = CHAIN A by A2, TARSKI:1; ::_thesis: verum
end;

theorem Th5: :: PROJRED2:5
for IPP being 2-dimensional Desarguesian IncProjSp
for o being POINT of IPP
for A, B being LINE of IPP st not o on A & not o on B holds
rng (IncProj (A,o,B)) = CHAIN B
proof
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for o being POINT of IPP
for A, B being LINE of IPP st not o on A & not o on B holds
rng (IncProj (A,o,B)) = CHAIN B
let o be POINT of IPP; ::_thesis: for A, B being LINE of IPP st not o on A & not o on B holds
rng (IncProj (A,o,B)) = CHAIN B
let A, B be LINE of IPP; ::_thesis: ( not o on A & not o on B implies rng (IncProj (A,o,B)) = CHAIN B )
assume A1: ( not o on A & not o on B ) ; ::_thesis: rng (IncProj (A,o,B)) = CHAIN B
A2: now__::_thesis:_for_x_being_set_st_x_in_CHAIN_B_holds_
x_in_rng_(IncProj_(A,o,B))
let x be set ; ::_thesis: ( x in CHAIN B implies x in rng (IncProj (A,o,B)) )
assume A3: x in CHAIN B ; ::_thesis: x in rng (IncProj (A,o,B))
then reconsider x9 = x as Element of the Points of IPP ;
 ex b being POINT of IPP st
( b = x & b on B ) by A3;
then consider y being POINT of IPP 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; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in_rng_(IncProj_(A,o,B))_holds_
x_in_CHAIN_B
let x be set ; ::_thesis: ( x in rng (IncProj (A,o,B)) implies x in CHAIN B )
assume A6: x in rng (IncProj (A,o,B)) ; ::_thesis: x in CHAIN 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 ; ::_thesis: verum
end;
hence  rng (IncProj (A,o,B)) = CHAIN B by A2, TARSKI:1; ::_thesis: verum
end;

theorem :: PROJRED2:6
for IPP being 2-dimensional Desarguesian IncProjSp
for A being LINE of IPP
for x being set holds
( x in CHAIN A iff ex a being POINT of IPP st
( x = a & a on A ) ) ;

theorem Th7: :: PROJRED2:7
for IPP being 2-dimensional Desarguesian IncProjSp
for o being POINT of IPP
for A, B being LINE of IPP st not o on A & not o on B holds
IncProj (A,o,B) is one-to-one
proof
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for o being POINT of IPP
for A, B being LINE of IPP st not o on A & not o on B holds
IncProj (A,o,B) is one-to-one
let o be POINT of IPP; ::_thesis: for A, B being LINE of IPP st not o on A & not o on B holds
IncProj (A,o,B) is one-to-one
let A, B be LINE of IPP; ::_thesis: ( not o on A & not o on B implies IncProj (A,o,B) is one-to-one )
set f = IncProj (A,o,B);
assume A1: ( not o on A & not o on B ) ; ::_thesis: IncProj (A,o,B) is one-to-one
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_dom_(IncProj_(A,o,B))_&_x2_in_dom_(IncProj_(A,o,B))_&_(IncProj_(A,o,B))_._x1_=_(IncProj_(A,o,B))_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in dom (IncProj (A,o,B)) & x2 in dom (IncProj (A,o,B)) & (IncProj (A,o,B)) . x1 = (IncProj (A,o,B)) . x2 implies x1 = x2 )
assume that
A2: x1 in dom (IncProj (A,o,B)) and
A3: x2 in dom (IncProj (A,o,B)) and
A4: (IncProj (A,o,B)) . x1 = (IncProj (A,o,B)) . x2 ; ::_thesis: x1 = x2
 x1 in CHAIN A by A1, A2, Th4;
then consider a being POINT of IPP such that
A5: x1 = a and
A6: a on A ;
 x2 in CHAIN A by A1, A3, Th4;
then consider b being POINT of IPP such that
A7: x2 = b and
A8: b on A ;
reconsider x = (IncProj (A,o,B)) . a, y = (IncProj (A,o,B)) . 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; ::_thesis: verum
end;
hence  IncProj (A,o,B) is one-to-one by FUNCT_1:def_4; ::_thesis: verum
end;

theorem Th8: :: PROJRED2:8
for IPP being 2-dimensional Desarguesian IncProjSp
for o being POINT of IPP
for A, B being LINE of IPP st not o on A & not o on B holds
(IncProj (A,o,B)) " = IncProj (B,o,A)
proof
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for o being POINT of IPP
for A, B being LINE of IPP st not o on A & not o on B holds
(IncProj (A,o,B)) " = IncProj (B,o,A)
let o be POINT of IPP; ::_thesis: for A, B being LINE of IPP st not o on A & not o on B holds
(IncProj (A,o,B)) " = IncProj (B,o,A)
let A, B be LINE of IPP; ::_thesis: ( not o on A & not o on B implies (IncProj (A,o,B)) " = IncProj (B,o,A) )
set f = IncProj (A,o,B);
set g = IncProj (B,o,A);
assume A1: ( not o on A & not o on B ) ; ::_thesis: (IncProj (A,o,B)) " = IncProj (B,o,A)
then A2: rng (IncProj (A,o,B)) = CHAIN B by Th5;
A3: dom (IncProj (A,o,B)) = CHAIN A by A1, Th4;
A4: now__::_thesis:_for_y,_x_being_set_holds_
(_y_in_rng_(IncProj_(A,o,B))_&_x_=_(IncProj_(B,o,A))_._y_iff_(_x_in_dom_(IncProj_(A,o,B))_&_y_=_(IncProj_(A,o,B))_._x_)_)
let y, x be set ; ::_thesis: ( y in rng (IncProj (A,o,B)) & x = (IncProj (B,o,A)) . y iff ( x in dom (IncProj (A,o,B)) & y = (IncProj (A,o,B)) . x ) )
A5: now__::_thesis:_(_x_in_dom_(IncProj_(A,o,B))_&_y_=_(IncProj_(A,o,B))_._x_implies_(_y_in_rng_(IncProj_(A,o,B))_&_x_=_(IncProj_(B,o,A))_._y_)_)
assume that
A6: x in dom (IncProj (A,o,B)) and
A7: y = (IncProj (A,o,B)) . x ; ::_thesis: ( y in rng (IncProj (A,o,B)) & x = (IncProj (B,o,A)) . y )
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 being LINE of IPP st
( o on O & x9 on O & y9 on O ) by A1, A7, A8, A9, PROJRED1:def_1;
hence  ( y in rng (IncProj (A,o,B)) & x = (IncProj (B,o,A)) . y ) by A1, A8, A9, A10, Th5, PROJRED1:def_1; ::_thesis: verum
end;
now__::_thesis:_(_y_in_rng_(IncProj_(A,o,B))_&_x_=_(IncProj_(B,o,A))_._y_implies_(_x_in_dom_(IncProj_(A,o,B))_&_y_=_(IncProj_(A,o,B))_._x_)_)
assume that
A11: y in rng (IncProj (A,o,B)) and
A12: x = (IncProj (B,o,A)) . y ; ::_thesis: ( x in dom (IncProj (A,o,B)) & y = (IncProj (A,o,B)) . x )
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 being LINE of IPP st
( o on O & y9 on O & x9 on O ) by A1, A12, A13, PROJRED1:def_1;
hence  ( x in dom (IncProj (A,o,B)) & y = (IncProj (A,o,B)) . x ) by A1, A13, A14, PROJRED1:def_1; ::_thesis: verum
end;
hence  ( y in rng (IncProj (A,o,B)) & x = (IncProj (B,o,A)) . y iff ( x in dom (IncProj (A,o,B)) & y = (IncProj (A,o,B)) . x ) ) by A5; ::_thesis: verum
end;
A15: IncProj (A,o,B) is one-to-one by A1, Th7;
dom (IncProj (B,o,A)) = CHAIN B by A1, Th4
.= rng (IncProj (A,o,B)) by A1, Th5 ;
hence  (IncProj (A,o,B)) " = IncProj (B,o,A) by A15, A4, FUNCT_1:32; ::_thesis: verum
end;

theorem :: PROJRED2:9
for IPP being 2-dimensional Desarguesian IncProjSp
for f being Projection of IPP holds f " is Projection of IPP
proof
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for f being Projection of IPP holds f " is Projection of IPP
let f be Projection of IPP; ::_thesis: f " is Projection of IPP
consider a being POINT of IPP, A, B being LINE of IPP 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  f " is Projection of IPP by A1, Def3; ::_thesis: verum
end;

theorem Th10: :: PROJRED2:10
for IPP being 2-dimensional Desarguesian IncProjSp
for o being POINT of IPP
for A being LINE of IPP st not o on A holds
IncProj (A,o,A) = id (CHAIN A)
proof
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for o being POINT of IPP
for A being LINE of IPP st not o on A holds
IncProj (A,o,A) = id (CHAIN A)
let o be POINT of IPP; ::_thesis: for A being LINE of IPP st not o on A holds
IncProj (A,o,A) = id (CHAIN A)
let A be LINE of IPP; ::_thesis: ( not o on A implies IncProj (A,o,A) = id (CHAIN A) )
set f = IncProj (A,o,A);
assume A1: not o on A ; ::_thesis: IncProj (A,o,A) = id (CHAIN A)
A2: for x being set st x in CHAIN A holds
(IncProj (A,o,A)) . x = x
proof
let x be set ; ::_thesis: ( x in CHAIN A implies (IncProj (A,o,A)) . x = x )
assume  x in CHAIN A ; ::_thesis: (IncProj (A,o,A)) . x = x
then  ex x9 being Element of the Points of IPP st
( x = x9 & x9 on A ) ;
hence  (IncProj (A,o,A)) . x = x by A1, PROJRED1:24; ::_thesis: verum
end;
 dom (IncProj (A,o,A)) = CHAIN A by A1, Th4;
hence  IncProj (A,o,A) = id (CHAIN A) by A2, FUNCT_1:17; ::_thesis: verum
end;

theorem :: PROJRED2:11
for IPP being 2-dimensional Desarguesian IncProjSp
for A being LINE of IPP holds id (CHAIN A) is Projection of IPP
proof
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for A being LINE of IPP holds id (CHAIN A) is Projection of IPP
let A be LINE of IPP; ::_thesis: id (CHAIN A) is Projection of IPP
consider o being POINT of IPP such that
A1: not o on A by PROJRED1:1;
 id (CHAIN A) = IncProj (A,o,A) by A1, Th10;
hence  id (CHAIN A) is Projection of IPP by A1, Def3; ::_thesis: verum
end;

theorem :: PROJRED2:12
for IPP being 2-dimensional Desarguesian IncProjSp
for o being POINT of IPP
for A, B, C being LINE of IPP st not o on A & not o on B & not o on C holds
(IncProj (C,o,B)) * (IncProj (A,o,C)) = IncProj (A,o,B)
proof
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for o being POINT of IPP
for A, B, C being LINE of IPP st not o on A & not o on B & not o on C holds
(IncProj (C,o,B)) * (IncProj (A,o,C)) = IncProj (A,o,B)
let o be POINT of IPP; ::_thesis: for A, B, C being LINE of IPP st not o on A & not o on B & not o on C holds
(IncProj (C,o,B)) * (IncProj (A,o,C)) = IncProj (A,o,B)
let A, B, C be LINE of IPP; ::_thesis: ( 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) )
assume that
A1: not o on A and
A2: not o on B and
A3: not o on C ; ::_thesis: (IncProj (C,o,B)) * (IncProj (A,o,C)) = IncProj (A,o,B)
set f = IncProj (A,o,B);
set g = IncProj (C,o,B);
set h = IncProj (A,o,C);
A4: dom (IncProj (A,o,B)) = CHAIN A by A1, A2, Th4;
set X = CHAIN A;
A5: dom (IncProj (A,o,C)) = CHAIN A by A1, A3, Th4;
A6: for x being POINT of IPP st x on A holds
(IncProj (A,o,B)) . x = ((IncProj (C,o,B)) * (IncProj (A,o,C))) . x
proof
let x be POINT of IPP; ::_thesis: ( x on A implies (IncProj (A,o,B)) . x = ((IncProj (C,o,B)) * (IncProj (A,o,C))) . x )
assume A7: x on A ; ::_thesis: (IncProj (A,o,B)) . x = ((IncProj (C,o,B)) * (IncProj (A,o,C))) . x
consider Q1 being LINE of IPP 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: (IncProj (A,o,C)) . 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: (IncProj (A,o,B)) . x = y by A1, A2, A7, A8, A9, A12, PROJRED1:def_1;
 x in dom (IncProj (A,o,C)) by A5, A7;
then ((IncProj (C,o,B)) * (IncProj (A,o,C))) . x = (IncProj (C,o,B)) . ((IncProj (A,o,C)) . x) by FUNCT_1:13
.= (IncProj (A,o,B)) . x by A2, A3, A8, A10, A12, A13, A11, PROJRED1:def_1 ;
hence  (IncProj (A,o,B)) . x = ((IncProj (C,o,B)) * (IncProj (A,o,C))) . x ; ::_thesis: verum
end;
A14: now__::_thesis:_for_y_being_set_st_y_in_CHAIN_A_holds_
((IncProj_(C,o,B))_*_(IncProj_(A,o,C)))_._y_=_(IncProj_(A,o,B))_._y
let y be set ; ::_thesis: ( y in CHAIN A implies ((IncProj (C,o,B)) * (IncProj (A,o,C))) . y = (IncProj (A,o,B)) . y )
assume  y in CHAIN A ; ::_thesis: ((IncProj (C,o,B)) * (IncProj (A,o,C))) . y = (IncProj (A,o,B)) . y
then  ex x being POINT of IPP st
( y = x & x on A ) ;
hence  ((IncProj (C,o,B)) * (IncProj (A,o,C))) . y = (IncProj (A,o,B)) . y by A6; ::_thesis: verum
end;
 dom ((IncProj (C,o,B)) * (IncProj (A,o,C))) = CHAIN A by A1, A2, A3, A5, PROJRED1:22;
hence  (IncProj (C,o,B)) * (IncProj (A,o,C)) = IncProj (A,o,B) by A4, A14, FUNCT_1:2; ::_thesis: verum
end;

theorem :: PROJRED2:13
for IPP being 2-dimensional Desarguesian IncProjSp
for o1, o2 being POINT of IPP
for O1, O2, O3 being LINE of IPP st not o1 on O1 & not o1 on O2 & not o2 on O2 & not o2 on O3 & O1,O2,O3 are_concurrent & O1 <> O3 holds
ex o being POINT of IPP st
( not o on O1 & not o on O3 & (IncProj (O2,o2,O3)) * (IncProj (O1,o1,O2)) = IncProj (O1,o,O3) )
proof
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for o1, o2 being POINT of IPP
for O1, O2, O3 being LINE of IPP st not o1 on O1 & not o1 on O2 & not o2 on O2 & not o2 on O3 & O1,O2,O3 are_concurrent & O1 <> O3 holds
ex o being POINT of IPP st
( not o on O1 & not o on O3 & (IncProj (O2,o2,O3)) * (IncProj (O1,o1,O2)) = IncProj (O1,o,O3) )
let o1, o2 be POINT of IPP; ::_thesis: for O1, O2, O3 being LINE of IPP st not o1 on O1 & not o1 on O2 & not o2 on O2 & not o2 on O3 & O1,O2,O3 are_concurrent & O1 <> O3 holds
ex o being POINT of IPP st
( not o on O1 & not o on O3 & (IncProj (O2,o2,O3)) * (IncProj (O1,o1,O2)) = IncProj (O1,o,O3) )
let O1, O2, O3 be LINE of IPP; ::_thesis: ( 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 being POINT of IPP st
( not o on O1 & not o on O3 & (IncProj (O2,o2,O3)) * (IncProj (O1,o1,O2)) = IncProj (O1,o,O3) ) )
assume that
A1: ( not o1 on O1 & not o1 on O2 & not o2 on O2 & not o2 on O3 ) and
A2: O1,O2,O3 are_concurrent and
A3: O1 <> O3 ; ::_thesis: ex o being POINT of IPP st
( not o on O1 & not o on O3 & (IncProj (O2,o2,O3)) * (IncProj (O1,o1,O2)) = IncProj (O1,o,O3) )
 ex p being POINT of IPP st
( p on O1 & p on O2 & p on O3 ) by A2, Def1;
hence  ex o being POINT of IPP st
( not o on O1 & not o on O3 & (IncProj (O2,o2,O3)) * (IncProj (O1,o1,O2)) = IncProj (O1,o,O3) ) by A1, A3, PROJRED1:25; ::_thesis: verum
end;

theorem Th14: :: PROJRED2:14
for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, c, d, p, q, pp9 being POINT of IPP
for A, B, C, Q, O, O1, O2, O3 being LINE of IPP st 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 holds
(IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q))
proof
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for a, b, c, d, p, q, pp9 being POINT of IPP
for A, B, C, Q, O, O1, O2, O3 being LINE of IPP st 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 holds
(IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q))
let a, b, c, d, p, q, pp9 be POINT of IPP; ::_thesis: for A, B, C, Q, O, O1, O2, O3 being LINE of IPP st 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 holds
(IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q))
let A, B, C, Q, O, O1, O2, O3 be LINE of IPP; ::_thesis: ( 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)) )
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 ; ::_thesis: (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q))
set f = IncProj (A,a,C);
set g = IncProj (C,b,B);
set g1 = IncProj (Q,b,B);
set f1 = IncProj (A,q,Q);
A29: dom (IncProj (A,a,C)) = CHAIN A by A1, A3, Th4;
set X = CHAIN A;
A30: dom (IncProj (A,q,Q)) = CHAIN A by A27, A28, Th4;
then A31: dom ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) = CHAIN A by A2, A9, A27, A28, PROJRED1:22;
A32: O1 <> O2
proof
assume  not O1 <> O2 ; ::_thesis: contradiction
then  d on O by A11, A16, A17, A20, A21, A26, INCPROJ:def_4;
hence  contradiction by A13, A14, A15, Def1; ::_thesis: verum
end;
 c <> d by A5, A6, A7, A15, Def1;
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 being POINT of IPP 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 be POINT of IPP; ::_thesis: ( x on A implies ((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . x )
assume A35: x on A ; ::_thesis: ((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . x
consider Q3 being LINE of IPP such that
A36: ( q on Q3 & x on Q3 ) by INCPROJ:def_5;
consider Q1 being LINE of IPP 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__::_thesis:_(_p_<>_x_implies_((IncProj_(C,b,B))_*_(IncProj_(A,a,C)))_._x_=_((IncProj_(Q,b,B))_*_(IncProj_(A,q,Q)))_._x_)
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 ; ::_thesis: ((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . x
 ( {x,x9,a} on Q1 & A,O1,O2 are_mutually_different ) by A1, A16, A21, A27, A32, A37, A40, INCSP_1:2, ZFMISC_1:def_5;
then consider R being LINE of IPP 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: (IncProj (C,b,B)) . x9 = x99 by A2, A4, A41, A50, A49, PROJRED1:def_1;
A52: x in dom (IncProj (A,q,Q)) by A30, A35;
 y on R by A48, INCSP_1:2;
then A53: (IncProj (Q,b,B)) . y = x99 by A2, A9, A39, A50, A49, PROJRED1:def_1;
A54: x in dom (IncProj (A,a,C)) by A29, A35;
 ( (IncProj (A,a,C)) . x = x9 & (IncProj (A,q,Q)) . x = y ) by A1, A3, A27, A28, A35, A37, A40, A41, A36, A38, A39, PROJRED1:def_1;
then ((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = (IncProj (Q,b,B)) . ((IncProj (A,q,Q)) . x) by A51, A53, A54, FUNCT_1:13
.= ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . x by A52, FUNCT_1:13 ;
hence  ((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . x ; ::_thesis: verum
end;
now__::_thesis:_(_p_=_x_implies_((IncProj_(C,b,B))_*_(IncProj_(A,a,C)))_._x_=_((IncProj_(Q,b,B))_*_(IncProj_(A,q,Q)))_._x_)
A55: ( (IncProj (A,q,Q)) . p = pp9 & (IncProj (Q,b,B)) . pp9 = d ) by A2, A9, A15, A18, A21, A22, A23, A24, A25, A27, A28, PROJRED1:def_1;
assume A56: p = x ; ::_thesis: ((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . x
A57: x in dom (IncProj (A,q,Q)) by A30, A35;
A58: x in dom (IncProj (A,a,C)) by A29, A35;
 ( (IncProj (A,a,C)) . p = d & (IncProj (C,b,B)) . d = d ) by A1, A2, A3, A4, A14, A15, A16, A17, A18, A19, A23, PROJRED1:def_1;
then ((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = (IncProj (Q,b,B)) . ((IncProj (A,q,Q)) . x) by A56, A55, A58, FUNCT_1:13
.= ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . x by A57, FUNCT_1:13 ;
hence  ((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . x ; ::_thesis: verum
end;
hence  ((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . x by A42; ::_thesis: verum
end;
A59: now__::_thesis:_for_y_being_set_st_y_in_CHAIN_A_holds_
((IncProj_(C,b,B))_*_(IncProj_(A,a,C)))_._y_=_((IncProj_(Q,b,B))_*_(IncProj_(A,q,Q)))_._y
let y be set ; ::_thesis: ( y in CHAIN A implies ((IncProj (C,b,B)) * (IncProj (A,a,C))) . y = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . y )
assume  y in CHAIN A ; ::_thesis: ((IncProj (C,b,B)) * (IncProj (A,a,C))) . y = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . y
then  ex x being POINT of IPP st
( y = x & x on A ) ;
hence  ((IncProj (C,b,B)) * (IncProj (A,a,C))) . y = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . y by A34; ::_thesis: verum
end;
 dom ((IncProj (C,b,B)) * (IncProj (A,a,C))) = CHAIN A by A1, A2, A3, A4, A29, PROJRED1:22;
hence  (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q)) by A31, A59, FUNCT_1:2; ::_thesis: verum
end;

theorem Th15: :: PROJRED2:15
for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, q, c, o, o99, d, o9, oo9 being POINT of IPP
for A, C, B, Q, O, O1, O2, O3 being LINE of IPP st 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 holds
(IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q))
proof
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for a, b, q, c, o, o99, d, o9, oo9 being POINT of IPP
for A, C, B, Q, O, O1, O2, O3 being LINE of IPP st 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 holds
(IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q))
let a, b, q, c, o, o99, d, o9, oo9 be POINT of IPP; ::_thesis: for A, C, B, Q, O, O1, O2, O3 being LINE of IPP st 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 holds
(IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q))
let A, C, B, Q, O, O1, O2, O3 be LINE of IPP; ::_thesis: ( 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)) )
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 ; ::_thesis: (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q))
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);
set g = IncProj (C,b,B);
set f1 = IncProj (A,q,Q);
set g1 = IncProj (Q,b,B);
A26: o on B by A11, INCSP_1:2;
A27: dom (IncProj (A,a,C)) = 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, Def1;
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, Def1;
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  q on A ; ::_thesis: contradiction
then  oo9 on A by A37, A35, A29, A40, INCPROJ:def_4;
hence  contradiction by A9, A20, A42, A47, INCPROJ:def_4; ::_thesis: verum
end;
A49: a on O by A13, INCSP_1:2;
 o9 <> d
proof
assume  not o9 <> d ; ::_thesis: contradiction
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; ::_thesis: verum
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  q on Q ; ::_thesis: contradiction
then  o on Q by A42, A35, A29, A50, INCPROJ:def_4;
hence  contradiction by A9, A20, A37, A45, INCPROJ:def_4; ::_thesis: verum
end;
then A52: dom (IncProj (A,q,Q)) = CHAIN A by A48, Th4;
then A53: dom ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) = CHAIN A 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 O1 <> O2 ; ::_thesis: contradiction
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; ::_thesis: verum
end;
A56: ( c on Q & oo9 on Q ) by A14, INCSP_1:1;
A57: for x being POINT of IPP 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_different by A2, A4, A38, A30, A55, ZFMISC_1:def_5;
let x be POINT of IPP; ::_thesis: ( x on A implies ((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . x )
assume A61: x on A ; ::_thesis: ((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . x
A62: {c,o,x} on A by A44, A19, A61, INCSP_1:2;
A63: x in dom (IncProj (A,q,Q)) by A52, A61;
A64: x in dom (IncProj (A,a,C)) by A27, A61;
consider Q1 being LINE of IPP 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 being LINE of IPP such that
A70: x9 on Q2 and
A71: b on Q2 by INCPROJ:def_5;
consider y being POINT of IPP 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 being LINE of IPP 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: (IncProj (A,q,Q)) . 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: (IncProj (Q,b,B)) . y = x99 by A3, A5, A71, A78, A72, A73, PROJRED1:def_1;
A80: (IncProj (C,b,B)) . x9 = x99 by A3, A4, A67, A70, A71, A78, PROJRED1:def_1;
 (IncProj (A,a,C)) . x = x9 by A1, A2, A61, A65, A66, A67, PROJRED1:def_1;
then ((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = (IncProj (Q,b,B)) . ((IncProj (A,q,Q)) . x) by A80, A77, A79, A64, FUNCT_1:13
.= ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . x by A63, FUNCT_1:13 ;
hence  ((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . x ; ::_thesis: verum
end;
A81: now__::_thesis:_for_y_being_set_st_y_in_CHAIN_A_holds_
((IncProj_(C,b,B))_*_(IncProj_(A,a,C)))_._y_=_((IncProj_(Q,b,B))_*_(IncProj_(A,q,Q)))_._y
let y be set ; ::_thesis: ( y in CHAIN A implies ((IncProj (C,b,B)) * (IncProj (A,a,C))) . y = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . y )
assume  y in CHAIN A ; ::_thesis: ((IncProj (C,b,B)) * (IncProj (A,a,C))) . y = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . y
then  ex x being POINT of IPP st
( y = x & x on A ) ;
hence  ((IncProj (C,b,B)) * (IncProj (A,a,C))) . y = ((IncProj (Q,b,B)) * (IncProj (A,q,Q))) . y by A57; ::_thesis: verum
end;
 dom ((IncProj (C,b,B)) * (IncProj (A,a,C))) = CHAIN A by A1, A2, A3, A4, A27, PROJRED1:22;
hence  (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q)) by A53, A81, FUNCT_1:2; ::_thesis: verum
end;

theorem Th16: :: PROJRED2:16
for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, c, p, d, q, pp9 being POINT of IPP
for A, C, Q, B, O, O1, O2, O3 being LINE of IPP st 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 holds
( q <> a & q <> b & not q on A & not q on Q )
proof
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for a, b, c, p, d, q, pp9 being POINT of IPP
for A, C, Q, B, O, O1, O2, O3 being LINE of IPP st 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 holds
( q <> a & q <> b & not q on A & not q on Q )
let a, b, c, p, d, q, pp9 be POINT of IPP; ::_thesis: for A, C, Q, B, O, O1, O2, O3 being LINE of IPP st 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 holds
( q <> a & q <> b & not q on A & not q on Q )
let A, C, Q, B, O, O1, O2, O3 be LINE of IPP; ::_thesis: ( 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 ) )
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 ; ::_thesis: ( q <> a & q <> b & not q on A & not q on Q )
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, Def1;
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 q <> pp9 ; ::_thesis: contradiction
then  O3 = O by A4, A30, A29, A27, A24, A23, INCPROJ:def_4;
hence  contradiction by A6, A11, A18, A28, Def1; ::_thesis: verum
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, INCSP_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 O1 <> O2 ; ::_thesis: contradiction
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, Def1; ::_thesis: verum
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  q on Q ; ::_thesis: contradiction
then  p on Q by A33, A32, A31, INCPROJ:def_4;
hence  contradiction by A7, A20, A35, A34, A40, INCPROJ:def_4; ::_thesis: verum
end;
A42: a on O by A13, INCSP_1:2;
A43: q <> p
proof
assume  not q <> p ; ::_thesis: contradiction
then  O = O1 by A1, A42, A26, A34, A39, A29, INCPROJ:def_4;
hence  contradiction by A6, A11, A18, A22, Def1; ::_thesis: verum
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, Def1;
 q <> b
proof
assume  not q <> b ; ::_thesis: contradiction
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; ::_thesis: verum
end;
hence  ( q <> a & q <> b & not q on A & not q on Q ) by A26, A34, A39, A46, A44, A45, A37, A43, A41, INCPROJ:def_4; ::_thesis: verum
end;

theorem Th17: :: PROJRED2:17
for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, c, o, o99, d, o9, oo9, q being POINT of IPP
for A, C, B, Q, O, O1, O2, O3 being LINE of IPP st 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 holds
( not q on A & not q on Q & b <> q )
proof
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for a, b, c, o, o99, d, o9, oo9, q being POINT of IPP
for A, C, B, Q, O, O1, O2, O3 being LINE of IPP st 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 holds
( not q on A & not q on Q & b <> q )
let a, b, c, o, o99, d, o9, oo9, q be POINT of IPP; ::_thesis: for A, C, B, Q, O, O1, O2, O3 being LINE of IPP st 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 holds
( not q on A & not q on Q & b <> q )
let A, C, B, Q, O, O1, O2, O3 be LINE of IPP; ::_thesis: ( 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 ) )
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 ; ::_thesis: ( not q on A & not q on Q & b <> q )
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, Def1;
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 O1 <> O2 ; ::_thesis: contradiction
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; ::_thesis: verum
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, Def1;
A41: b <> q
proof
assume  not b <> q ; ::_thesis: contradiction
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; ::_thesis: verum
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, Def1;
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 o9 <> d ; ::_thesis: contradiction
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; ::_thesis: verum
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  q on Q ; ::_thesis: contradiction
then  o on Q by A23, A38, A33, A49, INCPROJ:def_4;
hence  contradiction by A8, A44, A26, A50, A46, INCPROJ:def_4; ::_thesis: verum
end;
A52: q <> o by A3, A17, A18, A29, A30, A35, A28, INCPROJ:def_4;
 not q on A
proof
assume  q on A ; ::_thesis: contradiction
then  oo9 on A by A20, A38, A33, A52, INCPROJ:def_4;
hence  contradiction by A8, A19, A23, A48, INCPROJ:def_4; ::_thesis: verum
end;
hence  ( not q on A & not q on Q & b <> q ) by A51, A41; ::_thesis: verum
end;

theorem Th18: :: PROJRED2:18
for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, q, c, p, d, pp9 being POINT of IPP
for A, C, B, O, Q, O1, O2, O3 being LINE of IPP st 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 holds
( Q <> A & Q <> C & not q on Q & not b on Q )
proof
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for a, b, q, c, p, d, pp9 being POINT of IPP
for A, C, B, O, Q, O1, O2, O3 being LINE of IPP st 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 holds
( Q <> A & Q <> C & not q on Q & not b on Q )
let a, b, q, c, p, d, pp9 be POINT of IPP; ::_thesis: for A, C, B, O, Q, O1, O2, O3 being LINE of IPP st 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 holds
( Q <> A & Q <> C & not q on Q & not b on Q )
let A, C, B, O, Q, O1, O2, O3 be LINE of IPP; ::_thesis: ( 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 ) )
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 ; ::_thesis: ( Q <> A & Q <> C & not q on Q & not b on Q )
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, Def1;
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, Def1;
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, Def1;
A37: pp9 <> d
proof
assume  not pp9 <> d ; ::_thesis: contradiction
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; ::_thesis: verum
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 p <> pp9 ; ::_thesis: contradiction
then  O1 = O3 by A28, A30, A39, A22, A36, INCPROJ:def_4;
hence  contradiction by A7, A26, A40, A32, A27, A29, INCPROJ:def_4; ::_thesis: verum
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  b on Q ; ::_thesis: contradiction
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; ::_thesis: verum
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, Def1;
 not q on Q
proof
assume  q on Q ; ::_thesis: contradiction
then  q = pp9 by A34, A33, A24, A47, INCPROJ:def_4;
hence  contradiction by A8, A40, A25, A27, A22, A48, INCPROJ:def_4; ::_thesis: verum
end;
hence  ( Q <> A & Q <> C & not q on Q & not b on Q ) by A18, A35, A34, A31, A33, A39, A27, A22, A24, A41, A37, A44, INCPROJ:def_4; ::_thesis: verum
end;

theorem Th19: :: PROJRED2:19
for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, q, c, o, o99, d, o9, oo9 being POINT of IPP
for A, C, B, O, Q, O1, O2, O3 being LINE of IPP st 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 holds
( not b on Q & not q on Q & A <> Q )
proof
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for a, b, q, c, o, o99, d, o9, oo9 being POINT of IPP
for A, C, B, O, Q, O1, O2, O3 being LINE of IPP st 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 holds
( not b on Q & not q on Q & A <> Q )
let a, b, q, c, o, o99, d, o9, oo9 be POINT of IPP; ::_thesis: for A, C, B, O, Q, O1, O2, O3 being LINE of IPP st 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 holds
( not b on Q & not q on Q & A <> Q )
let A, C, B, O, Q, O1, O2, O3 be LINE of IPP; ::_thesis: ( 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 ) )
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 ; ::_thesis: ( not b on Q & not q on Q & A <> Q )
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, Def1;
A24: o on O3 by A16, INCSP_1:2;
A25: b <> oo9
proof
assume  not b <> oo9 ; ::_thesis: contradiction
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; ::_thesis: verum
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, INCSP_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, Def1;
then A38: o9 <> c by A1, A33, A18, A34, A36, A29, INCPROJ:def_4;
A39: not b on Q
proof
assume  b on Q ; ::_thesis: contradiction
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; ::_thesis: verum
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 O1 <> O2 ; ::_thesis: contradiction
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; ::_thesis: verum
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, INCSP_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 o9 <> d ; ::_thesis: contradiction
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; ::_thesis: verum
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  q on Q ; ::_thesis: contradiction
then  Q = O3 by A31, A50, A53, INCPROJ:def_4;
hence  contradiction by A5, A33, A18, A42, A47, A37, INCPROJ:def_4; ::_thesis: verum
end;
 o <> o9 by A6, A18, A21, A43, Def1;
then  o <> oo9 by A36, A29, A49, A27, A46, INCPROJ:def_4;
hence  ( not b on Q & not q on Q & A <> Q ) by A18, A48, A47, A39, A54, INCPROJ:def_4; ::_thesis: verum
end;

Lm1:  for IPP being 2-dimensional Desarguesian IncProjSp
for a, b being POINT of IPP
for A, B, C, Q, O being LINE of IPP st 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 holds
ex q being POINT of IPP 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
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for a, b being POINT of IPP
for A, B, C, Q, O being LINE of IPP st 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 holds
ex q being POINT of IPP 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)) )
let a, b be POINT of IPP; ::_thesis: for A, B, C, Q, O being LINE of IPP st 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 holds
ex q being POINT of IPP 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)) )
let A, B, C, Q, O be LINE of IPP; ::_thesis: ( 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 being POINT of IPP 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)) ) )
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 ; ::_thesis: ex q being POINT of IPP 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)) )
consider c being POINT of IPP such that
A11: ( c on A & c on C ) and
A12: c on Q by A5, Def1;
consider d being POINT of IPP such that
A13: d on C and
A14: d on B by INCPROJ:def_9;
consider O1 being LINE of IPP such that
A15: ( a on O1 & d on O1 ) by INCPROJ:def_5;
consider O3 being LINE of IPP 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 being POINT of IPP such that
A19: p on A and
A20: p on O1 by INCPROJ:def_9;
consider O2 being LINE of IPP such that
A21: ( p on O2 & pp9 on O2 ) by INCPROJ:def_5;
consider q being POINT of IPP such that
A22: q on O and
A23: q on O2 by INCPROJ:def_9;
now__::_thesis:_(_Q_<>_C_implies_ex_q,_q_being_POINT_of_IPP_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))_)_)
assume A24: Q <> C ; ::_thesis: ex q, q being POINT of IPP 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)) )
take q = q; ::_thesis: ex q being POINT of IPP 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)) )
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, INCSP_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  ex q being POINT of IPP 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)) ) by A22, A29; ::_thesis: verum
end;
hence  ex q being POINT of IPP 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)) ) by A1, A3, A8; ::_thesis: verum
end;

Lm2:  for IPP being 2-dimensional Desarguesian IncProjSp
for a, b being POINT of IPP
for A, B, C, Q, O being LINE of IPP st 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 holds
ex q being POINT of IPP 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
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for a, b being POINT of IPP
for A, B, C, Q, O being LINE of IPP st 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 holds
ex q being POINT of IPP 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)) )
let a, b be POINT of IPP; ::_thesis: for A, B, C, Q, O being LINE of IPP st 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 holds
ex q being POINT of IPP 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)) )
let A, B, C, Q, O be LINE of IPP; ::_thesis: ( 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 being POINT of IPP 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)) ) )
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 ; ::_thesis: ex q being POINT of IPP 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)) )
consider d being POINT of IPP such that
A6: d on B and
A7: d on C and
A8: d on O by A5, Def1;
A9: {a,b,d} on O by A4, A8, INCSP_1:2;
consider o being POINT of IPP such that
A10: o on A and
A11: o on B by INCPROJ:def_9;
consider O1 being LINE of IPP 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 being POINT of IPP such that
A16: c on A and
A17: c on C and
A18: c on Q by A2, Def1;
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 being LINE of IPP 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 being LINE of IPP 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 being POINT of IPP 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  ex q being POINT of IPP 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)) ) by A34, A38; ::_thesis: verum
end;

theorem Th20: :: PROJRED2:20
for IPP being 2-dimensional Desarguesian IncProjSp
for a, b being POINT of IPP
for A, B, C, Q, O being LINE of IPP st 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 holds
ex q being POINT of IPP 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
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for a, b being POINT of IPP
for A, B, C, Q, O being LINE of IPP st 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 holds
ex q being POINT of IPP 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)) )
let a, b be POINT of IPP; ::_thesis: for A, B, C, Q, O being LINE of IPP st 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 holds
ex q being POINT of IPP 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)) )
let A, B, C, Q, O be LINE of IPP; ::_thesis: ( 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 being POINT of IPP 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)) ) )
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 ) ; ::_thesis: ex q being POINT of IPP 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)) )
then  ( not B,C,O are_concurrent implies ex q being POINT of IPP 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)) ) ) by Lm1;
hence  ex q being POINT of IPP 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)) ) by A1, Lm2; ::_thesis: verum
end;

theorem :: PROJRED2:21
for IPP being 2-dimensional Desarguesian IncProjSp
for a, b being POINT of IPP
for A, B, C, Q, O being LINE of IPP st 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 holds
ex q being POINT of IPP 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
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for a, b being POINT of IPP
for A, B, C, Q, O being LINE of IPP st 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 holds
ex q being POINT of IPP 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)) )
let a, b be POINT of IPP; ::_thesis: for A, B, C, Q, O being LINE of IPP st 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 holds
ex q being POINT of IPP 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)) )
let A, B, C, Q, O be LINE of IPP; ::_thesis: ( 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 being POINT of IPP 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)) ) )
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 ) ; ::_thesis: ex q being POINT of IPP 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)) )
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
proof
assume  B,A,C are_concurrent ; ::_thesis: contradiction
then  ex o being POINT of IPP st
( o on B & o on A & o on C ) by Def1;
hence  contradiction by A5, Def1; ::_thesis: verum
end;
then consider q being POINT of IPP 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 ; ::_thesis: ( 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)) )
thus  ( q on O & not q on B & not q on Q ) by A10, A11; ::_thesis: (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,q,B)) * (IncProj (A,a,Q))
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 ; ::_thesis: verum
end;

theorem :: PROJRED2:22
for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, c, d, s, r being POINT of IPP
for A, B, C, S, R, Q being LINE of IPP st 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 holds
(IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,a,B)) * (IncProj (A,b,Q))
proof
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for a, b, c, d, s, r being POINT of IPP
for A, B, C, S, R, Q being LINE of IPP st 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 holds
(IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,a,B)) * (IncProj (A,b,Q))
let a, b, c, d, s, r be POINT of IPP; ::_thesis: for A, B, C, S, R, Q being LINE of IPP st 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 holds
(IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,a,B)) * (IncProj (A,b,Q))
let A, B, C, S, R, Q be LINE of IPP; ::_thesis: ( 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)) )
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 ; ::_thesis: (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,a,B)) * (IncProj (A,b,Q))
A22: c <> d by A7, A8, A9, A21, Def1;
then A23: c <> s by A3, A8, A10, A11, A12, A16, INCPROJ:def_4;
A24: now__::_thesis:_not_b_on_Q
assume  b on Q ; ::_thesis: contradiction
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; ::_thesis: verum
end;
A25: d <> r by A4, A8, A10, A13, A14, A18, A22, INCPROJ:def_4;
A26: now__::_thesis:_not_a_on_Q
assume  a on Q ; ::_thesis: contradiction
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; ::_thesis: verum
end;
set X = CHAIN A;
set f = IncProj (A,a,C);
set g = IncProj (C,b,B);
set g1 = IncProj (Q,a,B);
set f1 = IncProj (A,b,Q);
A27: dom (IncProj (A,a,C)) = CHAIN A by A1, A3, Th4;
A28: dom (IncProj (A,b,Q)) = CHAIN A by A6, A24, Th4;
then A29: dom ((IncProj (Q,a,B)) * (IncProj (A,b,Q))) = CHAIN A by A5, A6, A26, A24, PROJRED1:22;
 A <> C by A21, Th1;
then A30: C,A,R are_mutually_different by A4, A6, A14, ZFMISC_1:def_5;
A31: c <> d by A7, A8, A9, A21, Def1;
A32: for x being POINT of IPP 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 be POINT of IPP; ::_thesis: ( x on A implies ((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = ((IncProj (Q,a,B)) * (IncProj (A,b,Q))) . x )
assume A33: x on A ; ::_thesis: ((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = ((IncProj (Q,a,B)) * (IncProj (A,b,Q))) . x
then reconsider x9 = (IncProj (A,a,C)) . x, y = (IncProj (A,b,Q)) . x as POINT of IPP by A1, A3, A6, A24, PROJRED1:19;
A34: x in dom (IncProj (A,b,Q)) by A28, A33;
A35: x9 on C by A1, A3, A33, PROJRED1:20;
then reconsider x99 = (IncProj (C,b,B)) . x9 as POINT of IPP by A2, A4, PROJRED1:19;
consider O1 being LINE of IPP 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 being LINE of IPP 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 being LINE of IPP such that
A40: ( b on O2 & x9 on O2 & x99 on O2 ) by A2, A4, A35, PROJRED1:def_1;
A41: now__::_thesis:_(_s_<>_x_implies_(IncProj_(C,b,B))_._((IncProj_(A,a,C))_._x)_=_(IncProj_(Q,a,B))_._((IncProj_(A,b,Q))_._x)_)
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 ; ::_thesis: (IncProj (C,b,B)) . ((IncProj (A,a,C)) . x) = (IncProj (Q,a,B)) . ((IncProj (A,b,Q)) . 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 being LINE of IPP 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  (IncProj (C,b,B)) . ((IncProj (A,a,C)) . x) = (IncProj (Q,a,B)) . ((IncProj (A,b,Q)) . x) by A5, A26, A37, A39, A48, PROJRED1:def_1; ::_thesis: verum
end;
A49: now__::_thesis:_(_s_=_x_implies_(IncProj_(C,b,B))_._((IncProj_(A,a,C))_._x)_=_(IncProj_(Q,a,B))_._((IncProj_(A,b,Q))_._x)_)
assume A50: s = x ; ::_thesis: (IncProj (C,b,B)) . ((IncProj (A,a,C)) . x) = (IncProj (Q,a,B)) . ((IncProj (A,b,Q)) . 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  (IncProj (C,b,B)) . ((IncProj (A,a,C)) . x) = (IncProj (Q,a,B)) . ((IncProj (A,b,Q)) . x) by A5, A9, A11, A12, A16, A19, A26, A51, PROJRED1:def_1; ::_thesis: verum
end;
 x in dom (IncProj (A,a,C)) by A27, A33;
then ((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = (IncProj (Q,a,B)) . ((IncProj (A,b,Q)) . x) by A49, A41, FUNCT_1:13
.= ((IncProj (Q,a,B)) * (IncProj (A,b,Q))) . x by A34, FUNCT_1:13 ;
hence  ((IncProj (C,b,B)) * (IncProj (A,a,C))) . x = ((IncProj (Q,a,B)) * (IncProj (A,b,Q))) . x ; ::_thesis: verum
end;
A52: now__::_thesis:_for_y_being_set_st_y_in_CHAIN_A_holds_
((IncProj_(C,b,B))_*_(IncProj_(A,a,C)))_._y_=_((IncProj_(Q,a,B))_*_(IncProj_(A,b,Q)))_._y
let y be set ; ::_thesis: ( y in CHAIN A implies ((IncProj (C,b,B)) * (IncProj (A,a,C))) . y = ((IncProj (Q,a,B)) * (IncProj (A,b,Q))) . y )
assume  y in CHAIN A ; ::_thesis: ((IncProj (C,b,B)) * (IncProj (A,a,C))) . y = ((IncProj (Q,a,B)) * (IncProj (A,b,Q))) . y
then  ex x being POINT of IPP st
( y = x & x on A ) ;
hence  ((IncProj (C,b,B)) * (IncProj (A,a,C))) . y = ((IncProj (Q,a,B)) * (IncProj (A,b,Q))) . y by A32; ::_thesis: verum
end;
 dom ((IncProj (C,b,B)) * (IncProj (A,a,C))) = CHAIN A by A1, A2, A3, A4, A27, PROJRED1:22;
hence  (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,a,B)) * (IncProj (A,b,Q)) by A29, A52, FUNCT_1:2; ::_thesis: verum
end;

Lm3:  for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, c, q being POINT of IPP
for A, B, C, O being LINE of IPP st 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 holds
ex Q being LINE of IPP 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
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for a, b, c, q being POINT of IPP
for A, B, C, O being LINE of IPP st 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 holds
ex Q being LINE of IPP 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)) )
let a, b, c, q be POINT of IPP; ::_thesis: for A, B, C, O being LINE of IPP st 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 holds
ex Q being LINE of IPP 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)) )
let A, B, C, O be LINE of IPP; ::_thesis: ( 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 being LINE of IPP 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)) ) )
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 ) ; ::_thesis: ex Q being LINE of IPP 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)) )
consider d being POINT of IPP such that
A11: d on C and
A12: d on B by INCPROJ:def_9;
consider O1 being LINE of IPP such that
A13: ( a on O1 & d on O1 ) by INCPROJ:def_5;
consider O3 being LINE of IPP such that
A14: ( b on O3 & d on O3 ) by INCPROJ:def_5;
consider p being POINT of IPP such that
A15: p on A and
A16: p on O1 by INCPROJ:def_9;
consider O2 being LINE of IPP 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 being LINE of IPP such that
A20: c on Q and
A21: pp9 on Q by INCPROJ:def_5;
now__::_thesis:_(_q_<>_a_implies_ex_Q_being_LINE_of_IPP_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))_)_)
A22: ( {a,b,q} on O & {c,pp9} on Q ) by A7, A20, A21, INCSP_1:1, INCSP_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 ; ::_thesis: ex Q being LINE of IPP 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)) )
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  ex Q being LINE of IPP 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)) ) by A20, A27; ::_thesis: verum
end;
hence  ex Q being LINE of IPP 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)) ) by A3, A5; ::_thesis: verum
end;

Lm4:  for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, c, q being POINT of IPP
for A, B, C, O being LINE of IPP st 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 holds
ex Q being LINE of IPP 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
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for a, b, c, q being POINT of IPP
for A, B, C, O being LINE of IPP st 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 holds
ex Q being LINE of IPP 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)) )
let a, b, c, q be POINT of IPP; ::_thesis: for A, B, C, O being LINE of IPP st 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 holds
ex Q being LINE of IPP 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)) )
let A, B, C, O be LINE of IPP; ::_thesis: ( 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 being LINE of IPP 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)) ) )
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 ; ::_thesis: ex Q being LINE of IPP 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)) )
consider d being POINT of IPP such that
A10: d on B and
A11: d on C and
A12: d on O by A9, Def1;
A13: {a,b,d} on O by A5, A12, INCSP_1:2;
consider o being POINT of IPP such that
A14: o on A and
A15: o on B by INCPROJ:def_9;
consider O1 being LINE of IPP 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 being LINE of IPP 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 being LINE of IPP 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 being LINE of IPP 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  ex Q being LINE of IPP 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)) ) by A36, A41; ::_thesis: verum
end;

theorem Th23: :: PROJRED2:23
for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, q being POINT of IPP
for A, B, C, O being LINE of IPP st 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 holds
ex Q being LINE of IPP 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
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for a, b, q being POINT of IPP
for A, B, C, O being LINE of IPP st 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 holds
ex Q being LINE of IPP 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)) )
let a, b, q be POINT of IPP; ::_thesis: for A, B, C, O being LINE of IPP st 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 holds
ex Q being LINE of IPP 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)) )
let A, B, C, O be LINE of IPP; ::_thesis: ( 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 being LINE of IPP 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)) ) )
consider c being POINT of IPP 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 ) ; ::_thesis: ex Q being LINE of IPP 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)) )
A3: now__::_thesis:_(_B,C,O_are_concurrent_implies_ex_Q_being_LINE_of_IPP_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))_)_)
assume  B,C,O are_concurrent ; ::_thesis: ex Q being LINE of IPP 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)) )
then consider Q being LINE of IPP 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 = Q; ::_thesis: ( 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)) )
thus  A,C,Q are_concurrent by A1, A4, Def1; ::_thesis: ( not b on Q & not q on Q & (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q)) )
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; ::_thesis: verum
end;
now__::_thesis:_(_not_B,C,O_are_concurrent_implies_ex_Q_being_LINE_of_IPP_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))_)_)
assume  not B,C,O are_concurrent ; ::_thesis: ex Q being LINE of IPP 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)) )
then consider Q being LINE of IPP 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 = Q; ::_thesis: ( 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)) )
thus  A,C,Q are_concurrent by A1, A6, Def1; ::_thesis: ( not b on Q & not q on Q & (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,b,B)) * (IncProj (A,q,Q)) )
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; ::_thesis: verum
end;
hence  ex Q being LINE of IPP 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)) ) by A3; ::_thesis: verum
end;

theorem :: PROJRED2:24
for IPP being 2-dimensional Desarguesian IncProjSp
for a, b, q being POINT of IPP
for A, B, C, O being LINE of IPP st 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 holds
ex Q being LINE of IPP 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
let IPP be 2-dimensional Desarguesian IncProjSp; ::_thesis: for a, b, q being POINT of IPP
for A, B, C, O being LINE of IPP st 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 holds
ex Q being LINE of IPP 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)) )
let a, b, q be POINT of IPP; ::_thesis: for A, B, C, O being LINE of IPP st 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 holds
ex Q being LINE of IPP 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)) )
let A, B, C, O be LINE of IPP; ::_thesis: ( 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 being LINE of IPP 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)) ) )
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 ; ::_thesis: ex Q being LINE of IPP 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)) )
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
proof
assume  B,A,C are_concurrent ; ::_thesis: contradiction
then  ex o being POINT of IPP st
( o on B & o on A & o on C ) by Def1;
hence  contradiction by A8, Def1; ::_thesis: verum
end;
then consider Q being LINE of IPP 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 ; ::_thesis: ( 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)) )
thus  ( B,C,Q are_concurrent & not a on Q & not q on Q ) by A10, A11, A12; ::_thesis: (IncProj (C,b,B)) * (IncProj (A,a,C)) = (IncProj (Q,q,B)) * (IncProj (A,a,Q))
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 ; ::_thesis: verum
end;