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 )

( a,c // a9,c9 & b,c // b9,c9 ) by A1, Th53; :: thesis: verum

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 :: thesis: ( AS is not AffinPlane implies ex c9 being Element of AS st

( a,c // a9,c9 & b,c // b9,c9 ) )

hence
ex c9 being Element of AS st ( a,c // a9,c9 & b,c // b9,c9 ) )

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 )

( a,c // a9,c9 & b,c // b9,c9 ) by A1, A3, A4, A5, A6, A7, Lm12; :: thesis: verum

end;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 :: thesis: ( not a9 in X implies ex c9 being Element of AS st

( a,c // a9,c9 & b,c // b9,c9 ) )

hence
ex c9 being Element of AS st ( a,c // a9,c9 & b,c // b9,c9 ) )

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:15;

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:7;

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:37;

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:15;

A19: a9 in Line (a9,b9) by AFF_1:15;

then A20: Line (a,a9) c= Y by A4, A10, A9, A15, A16, A17, Th19;

A21: b9 in Line (a9,b9) by AFF_1:15;

A22: not b9 in X

A24: b9 in Line (b,b9) by AFF_1:15;

A25: a in Line (a,a9) by AFF_1:15;

A26: a <> c by A1, AFF_1:7;

A27: b in Line (b,b9) by AFF_1:15;

A28: a9 in Line (a,a9) by AFF_1:15;

A29: Line (a,b) is being_line by A12, AFF_1:def 3;

A30: Line (a,a9) <> Line (b,b9)

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;set P = Line (b,b9);

set AB = Line (a,b);

set AB9 = Line (a9,b9);

A9: a in Line (a,b) by AFF_1:15;

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:7;

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:37;

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:15;

A19: a9 in Line (a9,b9) by AFF_1:15;

then A20: Line (a,a9) c= Y by A4, A10, A9, A15, A16, A17, Th19;

A21: b9 in Line (a9,b9) by AFF_1:15;

A22: not b9 in X

proof

then A23:
Line (b,b9) is being_line
by A5, AFF_1:def 3;
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 Line (a9,b9) c= X by A7, A21, A14, A13, Th23;

hence contradiction by A10, A19; :: thesis: verum

A24: b9 in Line (b,b9) by AFF_1:15;

A25: a in Line (a,a9) by AFF_1:15;

A26: a <> c by A1, AFF_1:7;

A27: b in Line (b,b9) by AFF_1:15;

A28: a9 in Line (a,a9) by AFF_1:15;

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:18;

hence contradiction by A10, A13, A28; :: thesis: verum

end;then Line (a,a9) = Line (a,b) by A12, A9, A18, A29, A11, A25, A27, AFF_1:18;

hence contradiction by A10, A13, A28; :: thesis: verum

A31: now :: thesis: ( Line (a,a9) // Line (b,b9) implies ex c9 being Element of AS st

( a,c // a9,c9 & b,c // b9,c9 ) )

A38:
a9 in Y
by A19, A16;( a,c // a9,c9 & b,c // b9,c9 ) )

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))

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;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

A35:
Line (a,a9) // c * (Line (a,a9))
by A11, Def3;
assume
Line (a,a9) = c * (Line (a,a9))
; :: thesis: contradiction

then Line (a,a9) = Line (a,c) by A26, A11, A25, A33, AFF_1:57;

then Line (a,a9) c= X by A4, A6, A7, A26, Th19;

hence contradiction by A10, A28; :: thesis: verum

end;then Line (a,a9) = Line (a,c) by A26, A11, A25, A33, AFF_1:57;

then Line (a,a9) c= X by A4, A6, A7, A26, Th19;

hence contradiction by A10, A28; :: thesis: verum

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

A39: now :: thesis: ( ex q being Element of AS st

( q in Line (a,a9) & q in Line (b,b9) ) implies ex c9 being Element of AS st

( a,c // a9,c9 & b,c // b9,c9 ) )

Line (b,b9) c= Y
by A5, A18, A21, A22, A15, A16, A17, Th19;( q in Line (a,a9) & q in Line (b,b9) ) implies ex c9 being Element of AS st

( a,c // a9,c9 & b,c // b9,c9 ) )

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

A44: c in Line (q,c) by AFF_1:15;

A45: Line (a,a9) <> Line (q,c)

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:15, AFF_1:def 3;

then c9 in Line (q,c) by A48, A44, A46, AFF_1:25;

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;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

A43:
q <> b
assume
q = a
; :: thesis: contradiction

then Line (a,b) = Line (b,b9) by A12, A9, A18, A29, A23, A27, A41, AFF_1:18;

hence contradiction by A13, A22, A24; :: thesis: verum

end;then Line (a,b) = Line (b,b9) by A12, A9, A18, A29, A23, A27, A41, AFF_1:18;

hence contradiction by A13, A22, A24; :: thesis: verum

proof

set C = Line (q,c);
assume
q = b
; :: thesis: contradiction

then Line (a,b) = Line (a,a9) by A12, A9, A18, A29, A11, A25, A40, AFF_1:18;

hence contradiction by A10, A13, A28; :: thesis: verum

end;then Line (a,b) = Line (a,a9) by A12, A9, A18, A29, A11, A25, A40, AFF_1:18;

hence contradiction by A10, A13, A28; :: thesis: verum

A44: c in Line (q,c) by AFF_1:15;

A45: Line (a,a9) <> Line (q,c)

proof

LIN q,a,a9
by A11, A25, A28, A40, AFF_1:21;
assume
Line (a,a9) = Line (q,c)
; :: thesis: contradiction

then Line (a,a9) = Line (a,c) by A26, A11, A25, A44, AFF_1:57;

then Line (a,a9) c= X by A4, A6, A7, A26, Th19;

hence contradiction by A10, A28; :: thesis: verum

end;then Line (a,a9) = Line (a,c) by A26, A11, A25, A44, AFF_1:57;

then Line (a,a9) c= X by A4, A6, A7, A26, Th19;

hence contradiction by A10, A28; :: thesis: verum

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:15, AFF_1:def 3;

then c9 in Line (q,c) by A48, A44, A46, AFF_1:25;

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

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

( a,c // a9,c9 & b,c // b9,c9 ) by A1, A3, A4, A5, A6, A7, Lm12; :: thesis: verum

( a,c // a9,c9 & b,c // b9,c9 ) by A1, Th53; :: thesis: verum