let AS be AffinSpace; :: thesis: for a, b, c, a9, b9 being Element of AS st AS is AffinPlane & not LIN a,b,c 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: ( AS is AffinPlane & not LIN a,b,c implies ex c9 being Element of AS st

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

assume that

A1: AS is AffinPlane and

A2: not LIN a,b,c ; :: thesis: ex c9 being Element of AS st

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

consider C being Subset of AS such that

A3: ( b in C & c in C ) and

A4: C is being_line by Th11;

consider N being Subset of AS such that

A5: b9 in N and

A6: C // N by A4, AFF_1:49;

A7: N is being_line by A6, AFF_1:36;

consider P being Subset of AS such that

A8: a in P and

A9: c in P and

A10: P is being_line by Th11;

consider M being Subset of AS such that

A11: a9 in M and

A12: P // M by A10, AFF_1:49;

A13: not M // N

then consider c9 being Element of AS such that

A14: c9 in M and

A15: c9 in N by A1, A7, A13, AFF_1:58;

A16: b,c // b9,c9 by A3, A5, A6, A15, AFF_1:39;

a,c // a9,c9 by A8, A9, A11, A12, A14, AFF_1:39;

hence ex c9 being Element of AS st

( a,c // a9,c9 & b,c // b9,c9 ) by A16; :: 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: ( AS is AffinPlane & not LIN a,b,c implies ex c9 being Element of AS st

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

assume that

A1: AS is AffinPlane and

A2: not LIN a,b,c ; :: thesis: ex c9 being Element of AS st

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

consider C being Subset of AS such that

A3: ( b in C & c in C ) and

A4: C is being_line by Th11;

consider N being Subset of AS such that

A5: b9 in N and

A6: C // N by A4, AFF_1:49;

A7: N is being_line by A6, AFF_1:36;

consider P being Subset of AS such that

A8: a in P and

A9: c in P and

A10: P is being_line by Th11;

consider M being Subset of AS such that

A11: a9 in M and

A12: P // M by A10, AFF_1:49;

A13: not M // N

proof

M is being_line
by A12, AFF_1:36;
assume
M // N
; :: thesis: contradiction

then N // P by A12, AFF_1:44;

then C // P by A6, AFF_1:44;

then b in P by A3, A9, AFF_1:45;

hence contradiction by A2, A8, A9, A10, AFF_1:21; :: thesis: verum

end;then N // P by A12, AFF_1:44;

then C // P by A6, AFF_1:44;

then b in P by A3, A9, AFF_1:45;

hence contradiction by A2, A8, A9, A10, AFF_1:21; :: thesis: verum

then consider c9 being Element of AS such that

A14: c9 in M and

A15: c9 in N by A1, A7, A13, AFF_1:58;

A16: b,c // b9,c9 by A3, A5, A6, A15, AFF_1:39;

a,c // a9,c9 by A8, A9, A11, A12, A14, AFF_1:39;

hence ex c9 being Element of AS st

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