let AS be AffinSpace; :: thesis: for a, b, c, a9, b9 being Element of AS st not LIN a,b,c & a9 <> b9 & a,b // a9,b9 holds
ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 )
let a, b, c, a9, b9 be Element of AS; :: thesis: ( not LIN a,b,c & a9 <> b9 & a,b // a9,b9 implies ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 ) )
assume that
A1: not LIN a,b,c and
A2: a9 <> b9 and
A3: a,b // a9,b9 ; :: thesis: ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 )

now

consider X being Subset of AS such that
A4: a in X and
A5: b in X and
A6: c in X and
A7: X is being_plane by Th37;
assume A8: AS is not AffinPlane ; :: thesis: ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 )

now

set A = Line a,a9;
set P = Line b,b9;
set AB = Line a,b;
set AB9 = Line a9,b9;
A9: a in Line a,b by AFF_1:26;
assume A10: not a9 in X ; :: thesis: ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 )
then A11: Line a,a9 is being_line by A4, AFF_1:def 3;
A12: a <> b by A1, AFF_1:16;
then A13: Line a,b c= X by A4, A5, A7, Th19;
A14: Line a,b // Line a9,b9 by A2, A3, A12, AFF_1:51;
then consider Y being Subset of AS such that
A15: Line a,b c= Y and
A16: Line a9,b9 c= Y and
A17: Y is being_plane by Th39;
A18: b in Line a,b by AFF_1:26;
A19: a9 in Line a9,b9 by AFF_1:26;
then A20: Line a,a9 c= Y by A4, A10, A9, A15, A16, A17, Th19;
A21: b9 in Line a9,b9 by AFF_1:26;
A22: not b9 in X

proof

assume b9 in X ; :: thesis: contradiction
then Line a9,b9 c= X by A7, A21, A14, A13, Th23;
hence contradiction by A10, A19; :: thesis: verum

end;

then A23: Line b,b9 is being_line by A5, AFF_1:def 3;
A24: b9 in Line b,b9 by AFF_1:26;
A25: a in Line a,a9 by AFF_1:26;
A26: a <> c by A1, AFF_1:16;
A27: b in Line b,b9 by AFF_1:26;
A28: a9 in Line a,a9 by AFF_1:26;
A29: Line a,b is being_line by A12, AFF_1:def 3;
A30: Line a,a9 <> Line b,b9

proof

assume Line a,a9 = Line b,b9 ; :: thesis: contradiction
then Line a,a9 = Line a,b by A12, A9, A18, A29, A11, A25, A27, AFF_1:30;
hence contradiction by A10, A13, A28; :: thesis: verum

end;

A31: now

set C = c * (Line a,a9);
assume A32: Line a,a9 // Line b,b9 ; :: thesis: ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 )
A33: c in c * (Line a,a9) by A11, Def3;
A34: Line a,a9 <> c * (Line a,a9)

proof

assume Line a,a9 = c * (Line a,a9) ; :: thesis: contradiction
then Line a,a9 = Line a,c by A26, A11, A25, A33, AFF_1:71;
then Line a,a9 c= X by A4, A6, A7, A26, Th19;
hence contradiction by A10, A28; :: thesis: verum

end;

A35: Line a,a9 // c * (Line a,a9) by A11, Def3;
then consider c9 being Element of AS such that
A36: c9 in c * (Line a,a9) and
A37: a,c // a9,c9 by A25, A28, A33, Lm2;
c * (Line a,a9) is being_line by A11, Th27;
then b,c // b9,c9 by A3, A8, A11, A23, A25, A28, A27, A24, A30, A32, A33, A35, A36, A37, A34, Th51;
hence ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 ) by A37; :: thesis: verum

end;

A38: a9 in Y by A19, A16;

A39: now

given q being Element of AS such that A40: q in Line a,a9 and
A41: q in Line b,b9 ; :: thesis: ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 )
A42: q <> a

proof

assume q = a ; :: thesis: contradiction
then Line a,b = Line b,b9 by A12, A9, A18, A29, A23, A27, A41, AFF_1:30;
hence contradiction by A13, A22, A24; :: thesis: verum

end;

A43: q <> b

proof

assume q = b ; :: thesis: contradiction
then Line a,b = Line a,a9 by A12, A9, A18, A29, A11, A25, A40, AFF_1:30;
hence contradiction by A10, A13, A28; :: thesis: verum

end;

set C = Line q,c;
A44: c in Line q,c by AFF_1:26;
A45: Line a,a9 <> Line q,c

proof

assume Line a,a9 = Line q,c ; :: thesis: contradiction
then Line a,a9 = Line a,c by A26, A11, A25, A44, AFF_1:71;
then Line a,a9 c= X by A4, A6, A7, A26, Th19;
hence contradiction by A10, A28; :: thesis: verum

end;

LIN q,a,a9 by A11, A25, A28, A40, AFF_1:33;
then consider c9 being Element of AS such that
A46: LIN q,c,c9 and
A47: a,c // a9,c9 by A42, Th1;
A48: q <> c by A1, A4, A5, A6, A7, A10, A9, A18, A15, A17, A38, A20, A40, Th25;
then A49: ( q in Line q,c & Line q,c is being_line ) by AFF_1:26, AFF_1:def 3;
then c9 in Line q,c by A48, A44, A46, AFF_1:39;
then b,c // b9,c9 by A3, A8, A11, A23, A25, A28, A27, A24, A30, A40, A41, A42, A43, A48, A44, A49, A47, A45, Th49;
hence ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 ) by A47; :: thesis: verum

end;

Line b,b9 c= Y by A5, A18, A21, A22, A15, A16, A17, Th19;
hence ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 ) by A17, A11, A23, A20, A31, A39, Th22; :: thesis: verum

end;

hence ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 ) by A1, A3, A4, A5, A6, A7, Lm12; :: thesis: verum

end;

hence ex c9 being Element of AS st
( a,c // a9,c9 & b,c // b9,c9 ) by A1, Th53; :: thesis: verum