let AS be AffinSpace; :: thesis:
assume A1: IncProjSp_of AS is Desarguesian ; :: thesis:
set XX = IncProjSp_of AS;
for A, P, C being Subset of AS
for o, a, b, c, a', b', c' being Element of the carrier of AS st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' holds
b,c // b',c'

proof

let A, P, C be Subset of AS; :: thesis:
let o, a, b, c, a', b', c' be Element of the carrier of AS; :: thesis:
assume that
A2: ( o in A & o in P & o in C ) and
A3: ( o <> a & o <> b & o <> c ) and
A4: ( a in A & a' in A & b in P & b' in P & c in C & c' in C ) and
A5: ( A is being_line & P is being_line & C is being_line ) and
A6: ( A <> P & A <> C ) and
A7: ( a,b // a',b' & a,c // a',c' ) ; :: thesis:

now

assume A8: P <> C ; :: thesis:

now

assume A9: ( a <> a' & o <> a' ) ; :: thesis:
then A10: ( o <> b' & o <> c' & b <> b' & c <> c' ) by A2, A3, A4, A5, A6, A7, AFF_4:8, AFF_4:9;
then A11: ( a <> b & b <> c & a <> c & a' <> b' & b' <> c' & a' <> c' ) by A2, A3, A4, A5, A6, A8, AFF_1:30;
then A12: ( Line a,b is being_line & Line b,c is being_line & Line a,c is being_line & Line a',b' is being_line & Line b',c' is being_line & Line a',c' is being_line ) by AFF_1:def 3;
A13: ( a in Line a,b & b in Line a,b & b in Line b,c & c in Line b,c & a in Line a,c & c in Line a,c & a' in Line a',b' & b' in Line a',b' & b' in Line b',c' & c' in Line b',c' & a' in Line a',c' & c' in Line a',c' ) by AFF_1:26;
A14: ( Line a,b // Line a',b' & Line a,c // Line a',c' ) by A7, A11, AFF_1:51;
then A15: ( Line a,b '||' Line a',b' & Line a,c '||' Line a',c' ) by A12, AFF_4:40;
reconsider p = o, a1 = a, b1 = a', a2 = b, b2 = b', a3 = c, b3 = c' as Element of the Points of (IncProjSp_of AS) by Th20;
reconsider C1 = [A,1], C2 = [P,1], C3' = [C,1] as Element of the Lines of (IncProjSp_of AS) by A5, Th23;
reconsider A1 = [(Line b,c),1], A2 = [(Line a,c),1], A3 = [(Line a,b),1], B1 = [(Line b',c'),1], B2 = [(Line a',c'),1], B3 = [(Line a',b'),1] as Element of the Lines of (IncProjSp_of AS) by A12, Th23;
reconsider s = LDir (Line a,b), r = LDir (Line a,c) as Element of the Points of (IncProjSp_of AS) by A12, Th20;
A16: ( p on C2 & p on C3' & a2 on C2 & b2 on C2 & a3 on C3' & b3 on C3' ) by A2, A4, A5, Th26;
A17: ( a2 on A1 & a3 on A1 & b2 on B1 & b3 on B1 ) by A12, A13, Th26;

A18: now

assume C2 = C3' ; :: thesis:
then P = [C,1] `1 by MCART_1:7
.= C by MCART_1:7 ;
hence contradiction by A8; :: thesis:

end;

( not p on A1 & not p on B1 )

proof

assume ( p on A1 or p on B1 ) ; :: thesis:
then ( a3 on C2 or b3 on C2 ) by A3, A10, A16, A17, INCPROJ:def 9;
hence contradiction by A3, A10, A16, A18, INCPROJ:def 9; :: thesis:

end;

then consider t being Element of the Points of (IncProjSp_of AS) such that
A19: ( t on A1 & t on B1 ) by A16, A17, A18, INCPROJ:def 13;
( p on C1 & b1 on C1 & a1 on C1 ) by A2, A4, A5, Th26;
then A20: ( {p,b1,a1} on C1 & {p,a2,b2} on C2 & {p,a3,b3} on C3' ) by A16, INCSP_1:12;
A21: ( a2 on A1 & a3 on A1 & a3 on A2 & r on A2 & a1 on A2 & a2 on A3 & s on A3 & a1 on A3 ) by A12, A13, Th26, Th30;
( b2 on B1 & b3 on B1 & b1 on B2 & r on B2 & b3 on B2 & b1 on B3 & s on B3 & b2 on B3 ) by A12, A13, A15, Th26, Th28;
then A22: ( {a3,a2,t} on A1 & {a3,r,a1} on A2 & {a2,s,a1} on A3 & {t,b2,b3} on B1 & {b1,r,b3} on B2 & {b1,s,b2} on B3 ) by A19, A21, INCSP_1:12;

A23: now

assume C1 = C2 ; :: thesis:
then A = [P,1] `1 by MCART_1:7
.= P by MCART_1:7 ;
hence contradiction by A6; :: thesis:

end;

now

assume C1 = C3' ; :: thesis:
then A = [C,1] `1 by MCART_1:7
.= C by MCART_1:7 ;
hence contradiction by A6; :: thesis:

end;

then C1,C2,C3' are_mutually_different by A18, A23, ZFMISC_1:def 5;
then consider O being Element of the Lines of (IncProjSp_of AS) such that
A24: {r,s,t} on O by A1, A3, A9, A10, A20, A22, INCPROJ:def 19;
A25: ( r on O & s on O & t on O ) by A24, INCSP_1:12;

A26: now

assume r = s ; :: thesis:
then A27: Line a,b // Line a,c by A12, Th11;
then Line a,b // Line a',c' by A14, AFF_1:58;
then Line a',b' // Line a',c' by A14, AFF_1:58;
then ( c in Line a,b & c' in Line a',b' ) by A13, A27, AFF_1:59;
hence b,c // b',c' by A13, A14, AFF_1:53; :: thesis:

end;

now

assume A28: r <> s ; :: thesis:
ex X being Subset of AS st
( O = [(PDir X),2] & X is being_plane )

proof

reconsider x = LDir (Line a,b), y = LDir (Line a,c) as Element of the Points of (ProjHorizon AS) by A12, Th14;
( [x,O] in the Inc of (IncProjSp_of AS) & [y,O] in the Inc of (IncProjSp_of AS) ) by A25, INCSP_1:def 1;
then consider Z' being Element of the Lines of (ProjHorizon AS) such that
A29: O = [Z',2] by A28, Th41;
consider X being Subset of AS such that
A30: ( Z' = PDir X & X is being_plane ) by Th15;
take X ; :: thesis:
thus ( O = [(PDir X),2] & X is being_plane ) by A29, A30; :: thesis:

end;

then t is not Element of AS by A25, Th27;
then consider Y being Subset of AS such that
A31: ( t = LDir Y & Y is being_line ) by Th20;
( Y '||' Line b,c & Y '||' Line b',c' ) by A12, A19, A31, Th28;
then ( Y // Line b,c & Y // Line b',c' ) by A12, A31, AFF_4:40;
then Line b,c // Line b',c' by AFF_1:58;
hence b,c // b',c' by A13, AFF_1:53; :: thesis:

end;

hence b,c // b',c' by A26; :: thesis:

end;

hence b,c // b',c' by A2, A3, A4, A5, A6, A7, Th50; :: thesis:

end;

hence b,c // b',c' by A4, A5, AFF_1:65; :: thesis:

end;

hence AS is Desarguesian by AFF_2:def 4; :: thesis: