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

proof

let A, P, C be Subset of AS; :: thesis:
let o, a, b, c, a9, b9, c9 be Element of AS; :: thesis:
assume that
A2: o in A and
A3: o in P and
A4: o in C and
A5: o <> a and
A6: o <> b and
A7: o <> c and
A8: a in A and
A9: a9 in A and
A10: b in P and
A11: b9 in P and
A12: c in C and
A13: c9 in C and
A14: A is being_line and
A15: P is being_line and
A16: C is being_line and
A17: A <> P and
A18: A <> C and
A19: a,b // a9,b9 and
A20: a,c // a9,c9 ; :: thesis:

now :: thesis:

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

now :: thesis:

reconsider p = o, a1 = a, b1 = a9, a2 = b, b2 = b9, a3 = c, b3 = c9 as Element of the Points of (IncProjSp_of AS) by Th20;
reconsider C1 = [A,1], C2 = [P,1], C39 = [C,1] as Element of the Lines of (IncProjSp_of AS) by A14, A15, A16, Th23;
assume that
A22: a <> a9 and
A23: o <> a9 ; :: thesis:
A24: o <> c9 by A2, A4, A5, A7, A8, A9, A12, A14, A16, A18, A20, A23, AFF_4:8;
A25: a9 <> c9 by A2, A4, A9, A13, A14, A16, A18, A23, AFF_1:18;
then A26: Line (a9,c9) is being_line by AFF_1:def 3;
A27: o <> b9 by A2, A3, A5, A6, A8, A9, A10, A14, A15, A17, A19, A23, AFF_4:8;
then b9 <> c9 by A3, A4, A11, A13, A15, A16, A21, AFF_1:18;
then A28: Line (b9,c9) is being_line by AFF_1:def 3;
b <> c by A3, A4, A6, A10, A12, A15, A16, A21, AFF_1:18;
then A29: Line (b,c) is being_line by AFF_1:def 3;
A30: a <> c by A2, A4, A5, A8, A12, A14, A16, A18, AFF_1:18;
then A31: Line (a,c) is being_line by AFF_1:def 3;
A32: a <> b by A2, A3, A5, A8, A10, A14, A15, A17, AFF_1:18;
then A33: Line (a,b) is being_line by AFF_1:def 3;
then reconsider s = LDir (Line (a,b)), r = LDir (Line (a,c)) as Element of the Points of (IncProjSp_of AS) by A31, Th20;
A34: p on C2 by A3, A15, Th26;
A35: a9 <> b9 by A2, A3, A9, A11, A14, A15, A17, A23, AFF_1:18;
then A36: Line (a9,b9) is being_line by AFF_1:def 3;
then reconsider A1 = [(Line (b,c)),1], A2 = [(Line (a,c)),1], A3 = [(Line (a,b)),1], B1 = [(Line (b9,c9)),1], B2 = [(Line (a9,c9)),1], B3 = [(Line (a9,b9)),1] as Element of the Lines of (IncProjSp_of AS) by A33, A29, A31, A28, A26, Th23;
A37: r on A2 by A31, Th30;
A38: c in Line (b,c) by AFF_1:15;
then A39: a3 on A1 by A29, Th26;
A40: a3 on A1 by A29, A38, Th26;
A41: c9 in Line (a9,c9) by AFF_1:15;
then A42: b3 on B2 by A26, Th26;
A43: a9 in Line (a9,c9) by AFF_1:15;
then A44: b1 on B2 by A26, Th26;
A45: Line (a,c) // Line (a9,c9) by A20, A30, A25, AFF_1:37;
then Line (a,c) '||' Line (a9,c9) by A31, A26, AFF_4:40;
then r on B2 by A31, A26, Th28;
then A46: {b1,r,b3} on B2 by A44, A42, INCSP_1:2;
A47: c <> c9 by A2, A4, A5, A7, A8, A9, A12, A14, A16, A18, A20, A22, AFF_4:9;
A48: b1 on C1 by A9, A14, Th26;
A49: a3 on C39 by A12, A16, Th26;
A50: b9 in Line (a9,b9) by AFF_1:15;
then A51: b2 on B3 by A36, Th26;
A52: a9 in Line (a9,b9) by AFF_1:15;
then A53: b1 on B3 by A36, Th26;
A54: Line (a,b) // Line (a9,b9) by A19, A32, A35, AFF_1:37;
then Line (a,b) '||' Line (a9,b9) by A33, A36, AFF_4:40;
then s on B3 by A33, A36, Th28;
then A55: {b1,s,b2} on B3 by A53, A51, INCSP_1:2;

A56: now :: thesis:

assume C2 = C39 ; :: thesis:
then P = [C,1] `1
.= C ;
hence contradiction by A21; :: thesis:

end;

A57: now :: thesis:

assume C1 = C39 ; :: thesis:
then A = [C,1] `1
.= C ;
hence contradiction by A18; :: thesis:

end;

now :: thesis:

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

end;

then A58: C1,C2,C39 are_mutually_distinct by A56, A57, ZFMISC_1:def 5;
A59: a1 on C1 by A8, A14, Th26;
A60: b3 on C39 by A13, A16, Th26;
A61: p on C39 by A4, A16, Th26;
then A62: {p,a3,b3} on C39 by A49, A60, INCSP_1:2;
p on C1 by A2, A14, Th26;
then A63: {p,b1,a1} on C1 by A48, A59, INCSP_1:2;
A64: b2 on C2 by A11, A15, Th26;
A65: a in Line (a,c) by AFF_1:15;
then A66: a1 on A2 by A31, Th26;
A67: c in Line (a,c) by AFF_1:15;
then a3 on A2 by A31, Th26;
then A68: {a3,r,a1} on A2 by A37, A66, INCSP_1:2;
A69: b9 in Line (b9,c9) by AFF_1:15;
then A70: b2 on B1 by A28, Th26;
A71: c9 in Line (b9,c9) by AFF_1:15;
then A72: b3 on B1 by A28, Th26;
A73: b3 on B1 by A28, A71, Th26;
A74: a2 on C2 by A10, A15, Th26;
then A75: {p,a2,b2} on C2 by A34, A64, INCSP_1:2;
A76: b in Line (b,c) by AFF_1:15;
then A77: a2 on A1 by A29, Th26;
( 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 A6, A27, A34, A74, A64, A77, A40, A70, A73, INCPROJ:def 4;
hence contradiction by A7, A24, A34, A61, A49, A60, A56, INCPROJ:def 4; :: thesis:

end;

then consider t being Element of the Points of (IncProjSp_of AS) such that
A78: t on A1 and
A79: t on B1 by A34, A61, A74, A64, A49, A60, A77, A40, A70, A73, A56, INCPROJ:def 8;
a2 on A1 by A29, A76, Th26;
then A80: {a3,a2,t} on A1 by A78, A39, INCSP_1:2;
b2 on B1 by A28, A69, Th26;
then A81: {t,b2,b3} on B1 by A79, A72, INCSP_1:2;
A82: a in Line (a,b) by AFF_1:15;
then A83: a1 on A3 by A33, Th26;
A84: s on A3 by A33, Th30;
A85: b in Line (a,b) by AFF_1:15;
then a2 on A3 by A33, Th26;
then A86: {a2,s,a1} on A3 by A84, A83, INCSP_1:2;
b <> b9 by A2, A3, A5, A6, A8, A9, A10, A14, A15, A17, A19, A22, AFF_4:9;
then consider O being Element of the Lines of (IncProjSp_of AS) such that
A87: {r,s,t} on O by A1, A5, A6, A7, A22, A23, A27, A24, A47, A63, A75, A62, A80, A68, A86, A81, A46, A55, A58, INCPROJ:def 13;
A88: t on O by A87, INCSP_1:2;
A89: s on O by A87, INCSP_1:2;
A90: r on O by A87, INCSP_1:2;

A91: now :: thesis:

assume A92: 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 A33, A31, Th14;
A93: [y,O] in the Inc of (IncProjSp_of AS) by A90, INCSP_1:def 1;
[x,O] in the Inc of (IncProjSp_of AS) by A89, INCSP_1:def 1;
then consider Z9 being Element of the Lines of (ProjHorizon AS) such that
A94: O = [Z9,2] by A92, A93, Th41;
consider X being Subset of AS such that
A95: Z9 = PDir X and
A96: X is being_plane by Th15;
take X ; :: thesis:
thus ( O = [(PDir X),2] & X is being_plane ) by A94, A95, A96; :: thesis:

end;

then t is not Element of AS by A88, Th27;
then consider Y being Subset of AS such that
A97: t = LDir Y and
A98: Y is being_line by Th20;
Y '||' Line (b9,c9) by A28, A79, A97, A98, Th28;
then A99: Y // Line (b9,c9) by A28, A98, AFF_4:40;
Y '||' Line (b,c) by A29, A78, A97, A98, Th28;
then Y // Line (b,c) by A29, A98, AFF_4:40;
then Line (b,c) // Line (b9,c9) by A99, AFF_1:44;
hence b,c // b9,c9 by A76, A38, A69, A71, AFF_1:39; :: thesis:

end;

now :: thesis:

assume r = s ; :: thesis:
then A100: Line (a,b) // Line (a,c) by A33, A31, Th11;
then Line (a,b) // Line (a9,c9) by A45, AFF_1:44;
then Line (a9,b9) // Line (a9,c9) by A54, AFF_1:44;
then A101: c9 in Line (a9,b9) by A52, A43, A41, AFF_1:45;
c in Line (a,b) by A82, A65, A67, A100, AFF_1:45;
hence b,c // b9,c9 by A85, A50, A54, A101, AFF_1:39; :: thesis:

end;

hence b,c // b9,c9 by A91; :: thesis:

end;

hence b,c // b9,c9 by A2, A3, A4, A5, A6, A7, A8, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, Th50; :: thesis:

end;

hence b,c // b9,c9 by A10, A11, A12, A13, A15, AFF_1:51; :: thesis:

end;

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