let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis:
let p, q, c be POINT of IPP; :: thesis:
let K, L, R be LINE of IPP; :: thesis:
assume A1: ( not p on K & not p on L & not q on L & not q on R & c on K & c on L & c on R & K <> R ) ; :: thesis:
A2: ( dom ((IncProj L,q,R) * (IncProj K,p,L)) c= the Points of IPP & rng ((IncProj L,q,R) * (IncProj K,p,L)) c= the Points of IPP )

proof

set f = (IncProj L,q,R) * (IncProj K,p,L);
A3: dom ((IncProj L,q,R) * (IncProj K,p,L)) = dom (IncProj K,p,L) by A1, Th25;
A4: rng ((IncProj L,q,R) * (IncProj K,p,L)) = rng (IncProj L,q,R) by A1, Th25;
thus dom ((IncProj L,q,R) * (IncProj K,p,L)) c= the Points of IPP by A3; :: thesis:
thus rng ((IncProj L,q,R) * (IncProj K,p,L)) c= the Points of IPP by A4, RELAT_1:def 19; :: thesis:

end;

defpred S₁[ set ] means ex k being POINT of IPP st
( $1 = k & k on K );
consider X being set such that
A5: for x being set holds
( x in X iff ( x in the Points of IPP & S₁[x] ) ) from XBOOLE_0:sch 1();

A6: now

assume A7: p = q ; :: thesis:
(IncProj L,q,R) * (IncProj K,p,L) = IncProj K,p,R

proof

A8: ( X = dom ((IncProj L,q,R) * (IncProj K,p,L)) & X = dom (IncProj K,p,R) )

proof

thus X = dom ((IncProj L,q,R) * (IncProj K,p,L)) :: thesis:

proof

A9: X c= dom ((IncProj L,q,R) * (IncProj K,p,L))

proof

let e be set ; :: according to TARSKI:def 3 :: thesis:
assume A10: e in X ; :: thesis:
then reconsider e = e as POINT of IPP by A5;
A11: ex e' being Element of the Points of IPP st
( e = e' & e' on K ) by A5, A10;
dom ((IncProj L,q,R) * (IncProj K,p,L)) = dom (IncProj K,p,L) by A1, Th25;
hence e in dom ((IncProj L,q,R) * (IncProj K,p,L)) by A1, A11, Def1; :: thesis:

end;

dom ((IncProj L,q,R) * (IncProj K,p,L)) c= X

proof

let e be set ; :: according to TARSKI:def 3 :: thesis:
assume e in dom ((IncProj L,q,R) * (IncProj K,p,L)) ; :: thesis:
then A12: e in dom (IncProj K,p,L) by A1, Th25;
then reconsider e = e as POINT of IPP ;
e on K by A1, A12, Def1;
hence e in X by A5; :: thesis:

end;

hence X = dom ((IncProj L,q,R) * (IncProj K,p,L)) by A9, XBOOLE_0:def 10; :: thesis:

end;

thus X = dom (IncProj K,p,R) :: thesis:

proof

A13: X c= dom (IncProj K,p,R)

proof

let e be set ; :: according to TARSKI:def 3 :: thesis:
assume A14: e in X ; :: thesis:
then reconsider e = e as POINT of IPP by A5;
ex e' being POINT of IPP st
( e = e' & e' on K ) by A5, A14;
hence e in dom (IncProj K,p,R) by A1, A7, Def1; :: thesis:

end;

dom (IncProj K,p,R) c= X

proof

let e be set ; :: according to TARSKI:def 3 :: thesis:
assume A15: e in dom (IncProj K,p,R) ; :: thesis:
then reconsider e = e as POINT of IPP ;
e on K by A1, A7, A15, Def1;
hence e in X by A5; :: thesis:

end;

hence X = dom (IncProj K,p,R) by A13, XBOOLE_0:def 10; :: thesis:

end;

A16: for x being POINT of IPP st x in X holds
((IncProj L,q,R) * (IncProj K,p,L)) . x = (IncProj K,p,R) . x

proof

let x be POINT of IPP; :: thesis:
assume A17: x in X ; :: thesis:
then A18: x on K by A1, A7, A8, Def1;
A19: ((IncProj L,p,R) * (IncProj K,p,L)) . x = (IncProj L,p,R) . ((IncProj K,p,L) . x) by A7, A8, A17, FUNCT_1:22;
reconsider y = (IncProj K,p,L) . x as POINT of IPP by A1, A18, Th22;
A20: y on L by A1, A18, Th23;
consider A being LINE of IPP such that
A21: ( p on A & y on A ) by INCPROJ:def 10;
consider B being LINE of IPP such that
A22: ( p on B & x on B & y on B ) by A1, A18, A20, Def1;
reconsider z = (IncProj L,p,R) . y as POINT of IPP by A1, A7, A20, Th22;
A23: z on R by A1, A7, A20, Th23;
then consider C being LINE of IPP such that
A24: ( p on C & y on C & z on C ) by A1, A7, A20, Def1;
A25: A = B by A1, A20, A21, A22, INCPROJ:def 9;
A = C by A1, A20, A21, A24, INCPROJ:def 9;
hence ((IncProj L,q,R) * (IncProj K,p,L)) . x = (IncProj K,p,R) . x by A1, A7, A18, A19, A22, A23, A24, A25, Def1; :: thesis:

end;

(IncProj L,q,R) * (IncProj K,p,L) is PartFunc of the Points of IPP,the Points of IPP by A2, RELSET_1:11;
hence (IncProj L,q,R) * (IncProj K,p,L) = IncProj K,p,R by A8, A16, PARTFUN1:34; :: thesis:

end;

hence ex o being POINT of IPP st
( not o on K & not o on R & (IncProj L,q,R) * (IncProj K,p,L) = IncProj K,o,R ) by A1, A7; :: thesis:

end;

now

assume A26: p <> q ; :: thesis:
consider A being LINE of IPP such that
A27: ( p on A & q on A ) by INCPROJ:def 10;
consider c1 being POINT of IPP such that
A28: ( c1 on K & c1 on A ) by INCPROJ:def 14;
consider a1 being POINT of IPP such that
A29: ( a1 on K & c1 <> a1 & c <> a1 ) by Th8;
reconsider a2 = (IncProj K,p,L) . a1 as POINT of IPP by A1, A29, Th22;
A30: a2 on L by A1, A29, Th23;
then reconsider a3 = (IncProj L,q,R) . a2 as POINT of IPP by A1, Th22;
A31: a3 on R by A1, A30, Th23;
consider B being LINE of IPP such that
A32: ( a1 on B & a3 on B ) by INCPROJ:def 10;
consider o being POINT of IPP such that
A33: ( o on A & o on B ) by INCPROJ:def 14;
reconsider c2 = (IncProj K,p,L) . c1 as Element of the Points of IPP by A1, A28, Th22;
A34: c2 on L by A1, A28, Th23;
then reconsider c3 = (IncProj L,q,R) . c2 as POINT of IPP by A1, Th22;
A35: c3 on R by A1, A34, Th23;
A36: not a1 on R by A1, A29, INCPROJ:def 9;
A37: not a3 on K

proof

assume a3 on K ; :: thesis:
then A38: c = a3 by A1, A31, INCPROJ:def 9;
ex C being LINE of IPP st
( q on C & c on C ) by INCPROJ:def 10;
then (IncProj L,q,R) . c = a3 by A1, A38, Def1;
then A39: c = a2 by A1, A30, Th26;
ex D being LINE of IPP st
( p on D & c on D ) by INCPROJ:def 10;
then (IncProj K,p,L) . c = a2 by A1, A39, Def1;
hence contradiction by A1, A29, Th26; :: thesis:

end;

A40: ( not o on K & not o on R )

proof

assume A41: ( o on K or o on R ) ; :: thesis:

A42: now

assume A43: o on K ; :: thesis:
then o = c1 by A1, A27, A28, A33, INCPROJ:def 9;
hence contradiction by A29, A32, A33, A37, A43, INCPROJ:def 9; :: thesis:

end;

now

assume A44: o on R ; :: thesis:
A45: ex A1 being LINE of IPP st
( p on A1 & c1 on A1 & c2 on A1 ) by A1, A28, A34, Def1;
consider A2 being LINE of IPP such that
A46: ( q on A2 & c2 on A2 & c3 on A2 ) by A1, A34, A35, Def1;
c2 on A by A1, A27, A28, A45, INCPROJ:def 9;
then A = A2 by A1, A27, A34, A46, INCPROJ:def 9;
then A47: o = c3 by A1, A33, A35, A44, A46, INCPROJ:def 9;
o = a3 by A31, A32, A33, A36, A44, INCPROJ:def 9;
then c2 = a2 by A1, A30, A34, A47, Th26;
hence contradiction by A1, A28, A29, Th26; :: thesis:

end;

hence contradiction by A41, A42; :: thesis:

end;

A48: now

assume A49: K = L ; :: thesis:
take q = q; :: thesis:
(IncProj L,q,R) * (IncProj K,p,L) = IncProj K,q,R

proof

A50: ( X = dom ((IncProj L,q,R) * (IncProj K,p,L)) & X = dom (IncProj K,q,R) )

proof

thus X = dom ((IncProj L,q,R) * (IncProj K,p,L)) :: thesis:

proof

A51: X c= dom ((IncProj L,q,R) * (IncProj K,p,L))

proof

let e be set ; :: according to TARSKI:def 3 :: thesis:
assume A52: e in X ; :: thesis:
then reconsider e = e as Element of the Points of IPP by A5;
A53: ex e' being POINT of IPP st
( e = e' & e' on K ) by A5, A52;
dom ((IncProj L,q,R) * (IncProj K,p,L)) = dom (IncProj K,p,L) by A1, Th25;
hence e in dom ((IncProj L,q,R) * (IncProj K,p,L)) by A1, A53, Def1; :: thesis:

end;

dom ((IncProj L,q,R) * (IncProj K,p,L)) c= X

proof

let e be set ; :: according to TARSKI:def 3 :: thesis:
assume e in dom ((IncProj L,q,R) * (IncProj K,p,L)) ; :: thesis:
then A54: e in dom (IncProj K,p,L) by A1, Th25;
then reconsider e = e as POINT of IPP ;
e on K by A1, A54, Def1;
hence e in X by A5; :: thesis:

end;

hence X = dom ((IncProj L,q,R) * (IncProj K,p,L)) by A51, XBOOLE_0:def 10; :: thesis:

end;

thus X = dom (IncProj K,q,R) :: thesis:

proof

A55: X c= dom (IncProj K,q,R)

proof

let e be set ; :: according to TARSKI:def 3 :: thesis:
assume A56: e in X ; :: thesis:
then reconsider e = e as POINT of IPP by A5;
ex e' being POINT of IPP st
( e = e' & e' on K ) by A5, A56;
hence e in dom (IncProj K,q,R) by A1, A49, Def1; :: thesis:

end;

dom (IncProj K,q,R) c= X

proof

let e be set ; :: according to TARSKI:def 3 :: thesis:
assume A57: e in dom (IncProj K,q,R) ; :: thesis:
then reconsider e = e as POINT of IPP ;
e on K by A1, A49, A57, Def1;
hence e in X by A5; :: thesis:

end;

hence X = dom (IncProj K,q,R) by A55, XBOOLE_0:def 10; :: thesis:

end;

A58: for x being POINT of IPP st x in X holds
((IncProj L,q,R) * (IncProj K,p,L)) . x = (IncProj K,q,R) . x

proof

let x be Element of the Points of IPP; :: thesis:
assume A59: x in X ; :: thesis:
then A60: x on K by A1, A49, A50, Def1;
((IncProj K,q,R) * (IncProj K,p,K)) . x = (IncProj K,q,R) . ((IncProj K,p,K) . x) by A49, A50, A59, FUNCT_1:22;
hence ((IncProj L,q,R) * (IncProj K,p,L)) . x = (IncProj K,q,R) . x by A1, A49, A60, Th21; :: thesis:

end;

(IncProj L,q,R) * (IncProj K,p,L) is PartFunc of the Points of IPP,the Points of IPP by A2, RELSET_1:11;
hence (IncProj L,q,R) * (IncProj K,p,L) = IncProj K,q,R by A50, A58, PARTFUN1:34; :: thesis:

end;

hence ex o being POINT of IPP st
( not o on K & not o on R & (IncProj L,q,R) * (IncProj K,p,L) = IncProj K,o,R ) by A1, A49; :: thesis:

end;

A61: now

assume A62: L = R ; :: thesis:
take p = p; :: thesis:
(IncProj L,q,R) * (IncProj K,p,L) = IncProj K,p,R

proof

A63: ( X = dom ((IncProj L,q,R) * (IncProj K,p,L)) & X = dom (IncProj K,p,R) )

proof

thus X = dom ((IncProj L,q,R) * (IncProj K,p,L)) :: thesis:

proof

A64: X c= dom ((IncProj L,q,R) * (IncProj K,p,L))

proof

let e be set ; :: according to TARSKI:def 3 :: thesis:
assume A65: e in X ; :: thesis:
then reconsider e = e as Element of the Points of IPP by A5;
A66: ex e' being POINT of IPP st
( e = e' & e' on K ) by A5, A65;
dom ((IncProj L,q,R) * (IncProj K,p,L)) = dom (IncProj K,p,L) by A1, Th25;
hence e in dom ((IncProj L,q,R) * (IncProj K,p,L)) by A1, A66, Def1; :: thesis:

end;

dom ((IncProj L,q,R) * (IncProj K,p,L)) c= X

proof

let e be set ; :: according to TARSKI:def 3 :: thesis:
assume e in dom ((IncProj L,q,R) * (IncProj K,p,L)) ; :: thesis:
then A67: e in dom (IncProj K,p,L) by A1, Th25;
then reconsider e = e as POINT of IPP ;
e on K by A1, A67, Def1;
hence e in X by A5; :: thesis:

end;

hence X = dom ((IncProj L,q,R) * (IncProj K,p,L)) by A64, XBOOLE_0:def 10; :: thesis:

end;

thus X = dom (IncProj K,p,R) :: thesis:

proof

A68: X c= dom (IncProj K,p,R)

proof

let e be set ; :: according to TARSKI:def 3 :: thesis:
assume A69: e in X ; :: thesis:
then reconsider e = e as POINT of IPP by A5;
ex e' being POINT of IPP st
( e = e' & e' on K ) by A5, A69;
hence e in dom (IncProj K,p,R) by A1, A62, Def1; :: thesis:

end;

dom (IncProj K,p,R) c= X

proof

let e be set ; :: according to TARSKI:def 3 :: thesis:
assume A70: e in dom (IncProj K,p,R) ; :: thesis:
then reconsider e = e as POINT of IPP ;
e on K by A1, A62, A70, Def1;
hence e in X by A5; :: thesis:

end;

hence X = dom (IncProj K,p,R) by A68, XBOOLE_0:def 10; :: thesis:

end;

A71: for x being POINT of IPP st x in X holds
((IncProj L,q,R) * (IncProj K,p,L)) . x = (IncProj K,p,R) . x

proof

let x be Element of the Points of IPP; :: thesis:
assume A72: x in X ; :: thesis:
then A73: x on K by A1, A62, A63, Def1;
A74: ((IncProj R,q,R) * (IncProj K,p,R)) . x = (IncProj R,q,R) . ((IncProj K,p,R) . x) by A62, A63, A72, FUNCT_1:22;
reconsider y = (IncProj K,p,R) . x as POINT of IPP by A1, A62, A73, Th22;
y on R by A1, A62, A73, Th23;
hence ((IncProj L,q,R) * (IncProj K,p,L)) . x = (IncProj K,p,R) . x by A1, A62, A74, Th21; :: thesis:

end;

(IncProj L,q,R) * (IncProj K,p,L) is PartFunc of the Points of IPP,the Points of IPP by A2, RELSET_1:11;
hence (IncProj L,q,R) * (IncProj K,p,L) = IncProj K,p,R by A63, A71, PARTFUN1:34; :: thesis:

end;

hence ex o being POINT of IPP st
( not o on K & not o on R & (IncProj L,q,R) * (IncProj K,p,L) = IncProj K,o,R ) by A1, A62; :: thesis:

end;

now

assume A75: ( L <> R & K <> L ) ; :: thesis:
(IncProj L,q,R) * (IncProj K,p,L) = IncProj K,o,R

proof

A76: X = dom ((IncProj L,q,R) * (IncProj K,p,L))

proof

A77: X c= dom ((IncProj L,q,R) * (IncProj K,p,L))

proof

let e be set ; :: according to TARSKI:def 3 :: thesis:
assume A78: e in X ; :: thesis:
then reconsider e = e as POINT of IPP by A5;
A79: ex e' being POINT of IPP st
( e = e' & e' on K ) by A5, A78;
dom ((IncProj L,q,R) * (IncProj K,p,L)) = dom (IncProj K,p,L) by A1, Th25;
hence e in dom ((IncProj L,q,R) * (IncProj K,p,L)) by A1, A79, Def1; :: thesis:

end;

dom ((IncProj L,q,R) * (IncProj K,p,L)) c= X

proof

let e be set ; :: according to TARSKI:def 3 :: thesis:
assume e in dom ((IncProj L,q,R) * (IncProj K,p,L)) ; :: thesis:
then A80: e in dom (IncProj K,p,L) by A1, Th25;
then reconsider e = e as POINT of IPP ;
e on K by A1, A80, Def1;
hence e in X by A5; :: thesis:

end;

hence X = dom ((IncProj L,q,R) * (IncProj K,p,L)) by A77, XBOOLE_0:def 10; :: thesis:

end;

A81: for x being POINT of IPP st x in X holds
((IncProj L,q,R) * (IncProj K,p,L)) . x = (IncProj K,o,R) . x

proof

let x be Element of the Points of IPP; :: thesis:
assume A82: x in X ; :: thesis:

A83: now

assume A84: x = c ; :: thesis:
((IncProj L,q,R) * (IncProj K,p,L)) . x = (IncProj K,o,R) . x

proof

((IncProj L,q,R) * (IncProj K,p,L)) . c = (IncProj L,q,R) . ((IncProj K,p,L) . c) by A76, A82, A84, FUNCT_1:22;
then ((IncProj L,q,R) * (IncProj K,p,L)) . c = (IncProj L,q,R) . c by A1, Th27;
then ((IncProj L,q,R) * (IncProj K,p,L)) . c = c by A1, Th27;
hence ((IncProj L,q,R) * (IncProj K,p,L)) . x = (IncProj K,o,R) . x by A1, A40, A84, Th27; :: thesis:

end;

hence ((IncProj L,q,R) * (IncProj K,p,L)) . x = (IncProj K,o,R) . x ; :: thesis:

end;

A85: now

assume A86: x = c1 ; :: thesis:
((IncProj L,q,R) * (IncProj K,p,L)) . x = (IncProj K,o,R) . x

proof

A87: ((IncProj L,q,R) * (IncProj K,p,L)) . c1 = c3 by A76, A82, A86, FUNCT_1:22;
A88: ex A1 being Element of the Lines of IPP st
( p on A1 & c1 on A1 & c2 on A1 ) by A1, A28, A34, Def1;
consider A2 being LINE of IPP such that
A89: ( q on A2 & c2 on A2 & c3 on A2 ) by A1, A34, A35, Def1;
c2 on A by A1, A27, A28, A88, INCPROJ:def 9;
then A = A2 by A1, A27, A34, A89, INCPROJ:def 9;
hence ((IncProj L,q,R) * (IncProj K,p,L)) . x = (IncProj K,o,R) . x by A28, A33, A35, A40, A86, A87, A89, Def1; :: thesis:

end;

hence ((IncProj L,q,R) * (IncProj K,p,L)) . x = (IncProj K,o,R) . x ; :: thesis:

end;

A90: now

assume A91: x = a1 ; :: thesis:
((IncProj L,q,R) * (IncProj K,p,L)) . x = (IncProj K,o,R) . x

proof

((IncProj L,q,R) * (IncProj K,p,L)) . a1 = a3 by A76, A82, A91, FUNCT_1:22;
hence ((IncProj L,q,R) * (IncProj K,p,L)) . x = (IncProj K,o,R) . x by A29, A31, A32, A33, A40, A91, Def1; :: thesis:

end;

hence ((IncProj L,q,R) * (IncProj K,p,L)) . x = (IncProj K,o,R) . x ; :: thesis:

end;

now

assume A92: ( x <> c1 & x <> c & x <> a1 ) ; :: thesis:
((IncProj L,q,R) * (IncProj K,p,L)) . x = (IncProj K,o,R) . x

proof

A93: dom ((IncProj L,q,R) * (IncProj K,p,L)) = dom (IncProj K,p,L) by A1, Th25;
then A94: x on K by A1, A76, A82, Def1;
then reconsider y = (IncProj K,p,L) . x as POINT of IPP by A1, Th22;
A95: y on L by A1, A94, Th23;
then reconsider z = (IncProj L,q,R) . y as POINT of IPP by A1, Th22;
A96: z on R by A1, A95, Th23;
consider A1 being LINE of IPP such that
A97: ( q on A1 & a2 on A1 & a3 on A1 ) by A1, A30, A31, Def1;
consider A3 being Element of the Lines of IPP such that
A98: ( p on A3 & a1 on A3 & a2 on A3 ) by A1, A29, A30, Def1;
consider B1 being LINE of IPP such that
A99: ( q on B1 & y on B1 & z on B1 ) by A1, A95, A96, Def1;
consider B3 being LINE of IPP such that
A100: ( p on B3 & x on B3 & y on B3 ) by A1, A94, A95, Def1;
A101: ( c on K & x on K & a1 on K ) by A1, A29, A76, A82, A93, Def1;
A102: ( o on B & a3 on B & a1 on B & c on K & x on K & a1 on K & c on R & z on R & a3 on R ) by A1, A29, A30, A32, A33, A76, A82, A93, A95, Def1, Th23;
A103: A1 <> A3

proof

assume A1 = A3 ; :: thesis:
then A = A3 by A26, A27, A97, A98, INCPROJ:def 9;
hence contradiction by A1, A28, A29, A98, INCPROJ:def 9; :: thesis:

end;

A104: a2 <> c

proof

assume A105: a2 = c ; :: thesis:
(IncProj K,p,L) . c = c by A1, Th27;
hence contradiction by A1, A29, A105, Th26; :: thesis:

end;

A106: a2 <> a3

proof

assume a2 = a3 ; :: thesis:
then A107: (IncProj K,p,L) . a1 = c by A1, A30, A31, A75, INCPROJ:def 9;
(IncProj K,p,L) . c = c by A1, Th27;
hence contradiction by A1, A29, A107, Th26; :: thesis:

end;

A108: c <> y by A1, A92, A100, A101, INCPROJ:def 9;
( {a2,y,c} on L & {a2,a3,q} on A1 & {a2,p,a1} on A3 & {p,o,q} on A & {p,y,x} on B3 & {y,z,q} on B1 & {a3,o,a1} on B & {x,c,a1} on K & {a3,z,c} on R & A1,L,A3 are_mutually_different & a2 <> p & a2 <> c & a2 <> a3 ) by A1, A27, A30, A33, A95, A97, A98, A99, A100, A102, A103, A104, A106, INCSP_1:12, ZFMISC_1:def 5;
then consider O being LINE of IPP such that
A109: {o,z,x} on O by A108, Th14;
A110: ( x on O & z on O & o on O ) by A109, INCSP_1:12;
((IncProj L,q,R) * (IncProj K,p,L)) . x = (IncProj L,q,R) . ((IncProj K,p,L) . x) by A76, A82, FUNCT_1:22;
hence ((IncProj L,q,R) * (IncProj K,p,L)) . x = (IncProj K,o,R) . x by A40, A94, A96, A110, Def1; :: thesis:

end;

hence ((IncProj L,q,R) * (IncProj K,p,L)) . x = (IncProj K,o,R) . x ; :: thesis:

end;

hence ((IncProj L,q,R) * (IncProj K,p,L)) . x = (IncProj K,o,R) . x by A83, A85, A90; :: thesis:

end;

A111: X = dom (IncProj K,o,R)

proof

A112: X c= dom (IncProj K,o,R)

proof

let e be set ; :: according to TARSKI:def 3 :: thesis:
assume A113: e in X ; :: thesis:
then reconsider e = e as POINT of IPP by A5;
ex e' being POINT of IPP st
( e = e' & e' on K ) by A5, A113;
hence e in dom (IncProj K,o,R) by A40, Def1; :: thesis:

end;

dom (IncProj K,o,R) c= X

proof

let e be set ; :: according to TARSKI:def 3 :: thesis:
assume A114: e in dom (IncProj K,o,R) ; :: thesis:
then reconsider e = e as POINT of IPP ;
e on K by A40, A114, Def1;
hence e in X by A5; :: thesis:

end;

hence X = dom (IncProj K,o,R) by A112, XBOOLE_0:def 10; :: thesis:

end;

(IncProj L,q,R) * (IncProj K,p,L) is PartFunc of the Points of IPP,the Points of IPP by A2, RELSET_1:11;
hence (IncProj L,q,R) * (IncProj K,p,L) = IncProj K,o,R by A76, A81, A111, PARTFUN1:34; :: thesis:

end;

hence ex o being POINT of IPP st
( not o on K & not o on R & (IncProj L,q,R) * (IncProj K,p,L) = IncProj K,o,R ) by A40; :: thesis:

end;

hence ex o being POINT of IPP st
( not o on K & not o on R & (IncProj L,q,R) * (IncProj K,p,L) = IncProj K,o,R ) by A48, A61; :: thesis:

end;

hence ex o being POINT of IPP st
( not o on K & not o on R & (IncProj L,q,R) * (IncProj K,p,L) = IncProj K,o,R ) by A6; :: thesis: