let IPP be 2-dimensional Desarguesian IncProjSp; :: thesis:
let c, p, q be POINT of IPP; :: thesis:
let K, L, R be LINE of IPP; :: thesis:
assume that
A1: not p on K and
A2: not p on L and
A3: not q on L and
A4: not q on R and
A5: c on K and
A6: c on L and
A7: c on R and
A8: K <> R ; :: thesis:
defpred S₁[ object ] means ex k being POINT of IPP st
( $1 = k & k on K );
consider X being set such that
A9: for x being object holds
( x in X iff ( x in the Points of IPP & S₁[x] ) ) from XBOOLE_0:sch 1();
A10: ( 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));
dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) by A1, A2, A3, A4, Th22;
hence dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) c= the Points of IPP ; :: thesis:
rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) = rng (IncProj (L,q,R)) by A1, A2, A3, A4, Th22;
hence rng ((IncProj (L,q,R)) * (IncProj (K,p,L))) c= the Points of IPP by RELAT_1:def 19; :: thesis:

end;

A11: now :: thesis:

A12: now :: thesis:

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

proof

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume A14: e in X ; :: thesis:
then reconsider e = e as Element of the Points of IPP by A9;
A15: ex e9 being POINT of IPP st
( e = e9 & e9 on K ) by A9, A14;
dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) by A1, A2, A3, A4, Th22;
hence e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) by A1, A2, A15, Def1; :: thesis:

end;

assume A16: L = R ; :: thesis:
A17: X c= dom (IncProj (K,p,R))

proof

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume A18: e in X ; :: thesis:
then reconsider e = e as POINT of IPP by A9;
ex e9 being POINT of IPP st
( e = e9 & e9 on K ) by A9, A18;
hence e in dom (IncProj (K,p,R)) by A1, A2, A16, Def1; :: thesis:

end;

A19: 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 A20: x in X ; :: thesis:
then A21: ((IncProj (R,q,R)) * (IncProj (K,p,R))) . x = (IncProj (R,q,R)) . ((IncProj (K,p,R)) . x) by A16, A13, FUNCT_1:12;
A22: x on K by A1, A2, A16, A17, A20, Def1;
then reconsider y = (IncProj (K,p,R)) . x as POINT of IPP by A1, A2, A16, Th19;
y on R by A1, A2, A16, A22, Th20;
hence ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,p,R)) . x by A3, A16, A21, Th18; :: thesis:

end;

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

proof

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) ; :: thesis:
then A23: e in dom (IncProj (K,p,L)) by A1, A2, A3, A4, Th22;
then reconsider e = e as POINT of IPP ;
e on K by A1, A2, A23, Def1;
hence e in X by A9; :: thesis:

end;

then A24: X = dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) by A13, XBOOLE_0:def 10;
A25: (IncProj (L,q,R)) * (IncProj (K,p,L)) is PartFunc of the Points of IPP, the Points of IPP by A10, RELSET_1:4;
take p = p; :: thesis:
dom (IncProj (K,p,R)) c= X

proof

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume A26: e in dom (IncProj (K,p,R)) ; :: thesis:
then reconsider e = e as POINT of IPP ;
e on K by A1, A2, A16, A26, Def1;
hence e in X by A9; :: thesis:

end;

then X = dom (IncProj (K,p,R)) by A17, XBOOLE_0:def 10;
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, A2, A16, A24, A19, A25, PARTFUN1:5; :: thesis:

end;

consider A being LINE of IPP such that
A27: p on A and
A28: q on A by INCPROJ:def 5;
consider c1 being POINT of IPP such that
A29: c1 on K and
A30: c1 on A by INCPROJ:def 9;
reconsider c2 = (IncProj (K,p,L)) . c1 as Element of the Points of IPP by A1, A2, A29, Th19;
A31: c2 on L by A1, A2, A29, Th20;
then reconsider c3 = (IncProj (L,q,R)) . c2 as POINT of IPP by A3, A4, Th19;
A32: c3 on R by A3, A4, A31, Th20;
consider a1 being POINT of IPP such that
A33: a1 on K and
A34: c1 <> a1 and
A35: c <> a1 by Th8;
reconsider a2 = (IncProj (K,p,L)) . a1 as POINT of IPP by A1, A2, A33, Th19;
A36: a2 on L by A1, A2, A33, Th20;
then reconsider a3 = (IncProj (L,q,R)) . a2 as POINT of IPP by A3, A4, Th19;
A37: a3 on R by A3, A4, A36, Th20;
A38: not a3 on K

proof

assume a3 on K ; :: thesis:
then A39: c = a3 by A5, A7, A8, A37, INCPROJ:def 4;
ex C being LINE of IPP st
( q on C & c on C ) by INCPROJ:def 5;
then (IncProj (L,q,R)) . c = a3 by A3, A4, A6, A7, A39, Def1;
then A40: c = a2 by A3, A4, A6, A36, Th23;
ex D being LINE of IPP st
( p on D & c on D ) by INCPROJ:def 5;
then (IncProj (K,p,L)) . c = a2 by A1, A2, A5, A6, A40, Def1;
hence contradiction by A1, A2, A5, A33, A35, Th23; :: thesis:

end;

consider B being LINE of IPP such that
A41: ( a1 on B & a3 on B ) by INCPROJ:def 5;
consider o being POINT of IPP such that
A42: o on A and
A43: o on B by INCPROJ:def 9;
A44: not a1 on R by A5, A7, A8, A33, A35, INCPROJ:def 4;
A45: ( not o on K & not o on R )

proof

A46: now :: thesis:

assume A47: o on R ; :: thesis:
then A48: o = a3 by A37, A41, A43, A44, INCPROJ:def 4;
consider A2 being LINE of IPP such that
A49: q on A2 and
A50: c2 on A2 and
A51: c3 on A2 by A3, A4, A31, A32, Def1;
ex A1 being LINE of IPP st
( p on A1 & c1 on A1 & c2 on A1 ) by A1, A2, A29, A31, Def1;
then c2 on A by A1, A27, A29, A30, INCPROJ:def 4;
then A = A2 by A3, A28, A31, A49, A50, INCPROJ:def 4;
then o = c3 by A4, A42, A32, A47, A49, A51, INCPROJ:def 4;
then c2 = a2 by A3, A4, A36, A31, A48, Th23;
hence contradiction by A1, A2, A29, A33, A34, Th23; :: thesis:

end;

A52: now :: thesis:

assume A53: o on K ; :: thesis:
then o = c1 by A1, A27, A29, A30, A42, INCPROJ:def 4;
hence contradiction by A33, A34, A41, A43, A38, A53, INCPROJ:def 4; :: thesis:

end;

assume ( o on K or o on R ) ; :: thesis:
hence contradiction by A52, A46; :: thesis:

end;

assume A54: p <> q ; :: thesis:

A55: now :: thesis:

assume that
A56: L <> R and
K <> L ; :: thesis:
A57: X c= dom ((IncProj (L,q,R)) * (IncProj (K,p,L)))

proof

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume A58: e in X ; :: thesis:
then reconsider e = e as POINT of IPP by A9;
A59: ex e9 being POINT of IPP st
( e = e9 & e9 on K ) by A9, A58;
dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) by A1, A2, A3, A4, Th22;
hence e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) by A1, A2, A59, Def1; :: thesis:

end;

A60: 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 A61: x in X ; :: thesis:

A62: now :: thesis:

assume A63: x = c ; :: thesis:
then ((IncProj (L,q,R)) * (IncProj (K,p,L))) . c = (IncProj (L,q,R)) . ((IncProj (K,p,L)) . c) by A57, A61, FUNCT_1:12;
then ((IncProj (L,q,R)) * (IncProj (K,p,L))) . c = (IncProj (L,q,R)) . c by A1, A2, A5, A6, Th24;
then ((IncProj (L,q,R)) * (IncProj (K,p,L))) . c = c by A3, A4, A6, A7, Th24;
hence ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x by A5, A7, A45, A63, Th24; :: thesis:

end;

A64: now :: thesis:

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

proof

A66: a2 <> a3

proof

assume a2 = a3 ; :: thesis:
then A67: (IncProj (K,p,L)) . a1 = c by A6, A7, A36, A37, A56, INCPROJ:def 4;
(IncProj (K,p,L)) . c = c by A1, A2, A5, A6, Th24;
hence contradiction by A1, A2, A5, A33, A35, A67, Th23; :: thesis:

end;

A68: ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (L,q,R)) . ((IncProj (K,p,L)) . x) by A57, A61, FUNCT_1:12;
A69: a2 <> c

proof

assume A70: a2 = c ; :: thesis:
(IncProj (K,p,L)) . c = c by A1, A2, A5, A6, Th24;
hence contradiction by A1, A2, A5, A33, A35, A70, Th23; :: thesis:

end;

A71: a3 on R by A3, A4, A36, Th20;
A72: dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) by A1, A2, A3, A4, Th22;
then A73: x on K by A1, A2, A57, A61, Def1;
then reconsider y = (IncProj (K,p,L)) . x as POINT of IPP by A1, A2, Th19;
A74: y on L by A1, A2, A73, Th20;
then reconsider z = (IncProj (L,q,R)) . y as POINT of IPP by A3, A4, Th19;
consider B3 being LINE of IPP such that
A75: ( p on B3 & x on B3 & y on B3 ) by A1, A2, A73, A74, Def1;
x on K by A1, A2, A57, A61, A72, Def1;
then A76: c <> y by A1, A5, A65, A75, INCPROJ:def 4;
consider A1 being LINE of IPP such that
A77: q on A1 and
A78: ( a2 on A1 & a3 on A1 ) by A3, A4, A36, A37, Def1;
A79: {a2,a3,q} on A1 by A77, A78, INCSP_1:2;
A80: z on R by A3, A4, A74, Th20;
then consider B1 being LINE of IPP such that
A81: ( q on B1 & y on B1 & z on B1 ) by A3, A4, A74, Def1;
x on K by A1, A2, A57, A61, A72, Def1;
then A82: {x,c,a1} on K by A5, A33, INCSP_1:2;
consider A3 being Element of the Lines of IPP such that
A83: p on A3 and
A84: a1 on A3 and
A85: a2 on A3 by A1, A2, A33, A36, Def1;
A86: {a2,p,a1} on A3 by A83, A84, A85, INCSP_1:2;
A1 <> A3

proof

assume A1 = A3 ; :: thesis:
then A = A3 by A54, A27, A28, A77, A83, INCPROJ:def 4;
hence contradiction by A1, A29, A30, A33, A34, A83, A84, INCPROJ:def 4; :: thesis:

end;

then A87: A1,L,A3 are_mutually_distinct by A2, A3, A77, A83, ZFMISC_1:def 5;
A88: {a2,y,c} on L by A6, A36, A74, INCSP_1:2;
A89: {p,y,x} on B3 by A75, INCSP_1:2;
z on R by A3, A4, A74, Th20;
then A90: {a3,z,c} on R by A7, A71, INCSP_1:2;
A91: ( {p,o,q} on A & {a3,o,a1} on B ) by A27, A28, A41, A42, A43, INCSP_1:2;
A92: a2 <> p by A1, A2, A33, Th20;
{y,z,q} on B1 by A81, INCSP_1:2;
then consider O being LINE of IPP such that
A93: {o,z,x} on O by A69, A66, A76, A88, A79, A86, A89, A91, A82, A90, A87, A92, Th12;
A94: o on O by A93, INCSP_1:2;
( x on O & z on O ) by A93, INCSP_1:2;
hence ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x by A45, A73, A80, A94, A68, Def1; :: thesis:

end;

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

end;

A95: now :: thesis:

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

proof

A97: ((IncProj (L,q,R)) * (IncProj (K,p,L))) . c1 = c3 by A57, A61, A96, FUNCT_1:12;
consider A2 being LINE of IPP such that
A98: ( q on A2 & c2 on A2 ) and
A99: c3 on A2 by A3, A4, A31, A32, Def1;
ex A1 being Element of the Lines of IPP st
( p on A1 & c1 on A1 & c2 on A1 ) by A1, A2, A29, A31, Def1;
then c2 on A by A1, A27, A29, A30, INCPROJ:def 4;
then A = A2 by A3, A28, A31, A98, INCPROJ:def 4;
hence ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x by A29, A30, A42, A32, A45, A96, A97, A99, Def1; :: thesis:

end;

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

end;

now :: thesis:

assume A100: x = a1 ; :: thesis:
then ((IncProj (L,q,R)) * (IncProj (K,p,L))) . a1 = a3 by A57, A61, FUNCT_1:12;
hence ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,o,R)) . x by A33, A37, A41, A43, A45, A100, Def1; :: thesis:

end;

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

end;

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

proof

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

end;

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

proof

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume A103: e in X ; :: thesis:
then reconsider e = e as POINT of IPP by A9;
ex e9 being POINT of IPP st
( e = e9 & e9 on K ) by A9, A103;
hence e in dom (IncProj (K,o,R)) by A45, Def1; :: thesis:

end;

then A104: X = dom (IncProj (K,o,R)) by A101, XBOOLE_0:def 10;
A105: (IncProj (L,q,R)) * (IncProj (K,p,L)) is PartFunc of the Points of IPP, the Points of IPP by A10, RELSET_1:4;
dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) c= X

proof

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) ; :: thesis:
then A106: e in dom (IncProj (K,p,L)) by A1, A2, A3, A4, Th22;
then reconsider e = e as POINT of IPP ;
e on K by A1, A2, A106, Def1;
hence e in X by A9; :: thesis:

end;

then X = dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) by A57, XBOOLE_0:def 10;
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 A45, A60, A104, A105, PARTFUN1:5; :: thesis:

end;

now :: thesis:

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

proof

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume A108: e in X ; :: thesis:
then reconsider e = e as Element of the Points of IPP by A9;
A109: ex e9 being POINT of IPP st
( e = e9 & e9 on K ) by A9, A108;
dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) by A1, A2, A3, A4, Th22;
hence e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) by A1, A2, A109, Def1; :: thesis:

end;

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

proof

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) ; :: thesis:
then A110: e in dom (IncProj (K,p,L)) by A1, A2, A3, A4, Th22;
then reconsider e = e as POINT of IPP ;
e on K by A1, A2, A110, Def1;
hence e in X by A9; :: thesis:

end;

then A111: X = dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) by A107, XBOOLE_0:def 10;
A112: (IncProj (L,q,R)) * (IncProj (K,p,L)) is PartFunc of the Points of IPP, the Points of IPP by A10, RELSET_1:4;
assume A113: K = L ; :: thesis:
A114: X c= dom (IncProj (K,q,R))

proof

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume A115: e in X ; :: thesis:
then reconsider e = e as POINT of IPP by A9;
ex e9 being POINT of IPP st
( e = e9 & e9 on K ) by A9, A115;
hence e in dom (IncProj (K,q,R)) by A3, A4, A113, Def1; :: thesis:

end;

A116: 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 x in X ; :: thesis:
then ( x on K & ((IncProj (K,q,R)) * (IncProj (K,p,K))) . x = (IncProj (K,q,R)) . ((IncProj (K,p,K)) . x) ) by A3, A4, A113, A107, A114, Def1, FUNCT_1:12;
hence ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,q,R)) . x by A1, A113, Th18; :: thesis:

end;

take q = q; :: thesis:
dom (IncProj (K,q,R)) c= X

proof

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume A117: e in dom (IncProj (K,q,R)) ; :: thesis:
then reconsider e = e as POINT of IPP ;
e on K by A3, A4, A113, A117, Def1;
hence e in X by A9; :: thesis:

end;

then X = dom (IncProj (K,q,R)) by A114, XBOOLE_0:def 10;
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 A3, A4, A113, A111, A116, A112, PARTFUN1:5; :: 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 A12, A55; :: thesis:

end;

now :: thesis:

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

proof

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume A119: e in X ; :: thesis:
then reconsider e = e as POINT of IPP by A9;
A120: ex e9 being Element of the Points of IPP st
( e = e9 & e9 on K ) by A9, A119;
dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) = dom (IncProj (K,p,L)) by A1, A2, A3, A4, Th22;
hence e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) by A1, A2, A120, Def1; :: thesis:

end;

assume A121: p = q ; :: thesis:
A122: X c= dom (IncProj (K,p,R))

proof

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume A123: e in X ; :: thesis:
then reconsider e = e as POINT of IPP by A9;
ex e9 being POINT of IPP st
( e = e9 & e9 on K ) by A9, A123;
hence e in dom (IncProj (K,p,R)) by A1, A4, A121, Def1; :: thesis:

end;

A124: 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 A125: x in X ; :: thesis:
then A126: ((IncProj (L,p,R)) * (IncProj (K,p,L))) . x = (IncProj (L,p,R)) . ((IncProj (K,p,L)) . x) by A121, A118, FUNCT_1:12;
A127: x on K by A1, A4, A121, A122, A125, Def1;
then reconsider y = (IncProj (K,p,L)) . x as POINT of IPP by A1, A2, Th19;
A128: y on L by A1, A2, A127, Th20;
then reconsider z = (IncProj (L,p,R)) . y as POINT of IPP by A2, A4, A121, Th19;
consider A being LINE of IPP such that
A129: ( p on A & y on A ) by INCPROJ:def 5;
A130: z on R by A2, A4, A121, A128, Th20;
then consider C being LINE of IPP such that
A131: ( p on C & y on C ) and
A132: z on C by A2, A4, A121, A128, Def1;
A133: A = C by A2, A128, A129, A131, INCPROJ:def 4;
consider B being LINE of IPP such that
A134: p on B and
A135: x on B and
A136: y on B by A1, A2, A127, A128, Def1;
A = B by A2, A128, A129, A134, A136, INCPROJ:def 4;
hence ((IncProj (L,q,R)) * (IncProj (K,p,L))) . x = (IncProj (K,p,R)) . x by A1, A4, A121, A127, A126, A134, A135, A130, A132, A133, Def1; :: thesis:

end;

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

proof

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume e in dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) ; :: thesis:
then A137: e in dom (IncProj (K,p,L)) by A1, A2, A3, A4, Th22;
then reconsider e = e as POINT of IPP ;
e on K by A1, A2, A137, Def1;
hence e in X by A9; :: thesis:

end;

then A138: X = dom ((IncProj (L,q,R)) * (IncProj (K,p,L))) by A118, XBOOLE_0:def 10;
A139: (IncProj (L,q,R)) * (IncProj (K,p,L)) is PartFunc of the Points of IPP, the Points of IPP by A10, RELSET_1:4;
dom (IncProj (K,p,R)) c= X

proof

let e be object ; :: according to TARSKI:def 3 :: thesis:
assume A140: e in dom (IncProj (K,p,R)) ; :: thesis:
then reconsider e = e as POINT of IPP ;
e on K by A1, A4, A121, A140, Def1;
hence e in X by A9; :: thesis:

end;

then X = dom (IncProj (K,p,R)) by A122, XBOOLE_0:def 10;
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, A4, A121, A138, A124, A139, PARTFUN1:5; :: 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 A11; :: thesis: