let AS be AffinSpace; :: thesis: for a, b, c, a9, b9, c9, q being Element of AS
for A, C, P being Subset of AS st AS is not AffinPlane & q in A & q in P & q in C & q <> a & q <> b & q <> 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
let a, b, c, a9, b9, c9, q be Element of AS; :: thesis: for A, C, P being Subset of AS st AS is not AffinPlane & q in A & q in P & q in C & q <> a & q <> b & q <> 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
let A, C, P be Subset of AS; :: thesis: ( AS is not AffinPlane & q in A & q in P & q in C & q <> a & q <> b & q <> 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 implies b,c // b9,c9 )
assume that
A1: AS is not AffinPlane and
A2: q in A and
A3: q in P and
A4: q in C and
A5: q <> a and
A6: q <> b and
A7: q <> c and
A8: ( a in A & a9 in A ) and
A9: ( b in P & b9 in P ) and
A10: ( c in C & c9 in C ) and
A11: A is being_line and
A12: P is being_line and
A13: C is being_line and
A14: A <> P and
A15: A <> C and
A16: a,b // a9,b9 and
A17: a,c // a9,c9 ; :: thesis: b,c // b9,c9

now :: thesis: ( A,P,C is_coplanar implies b,c // b9,c9 )

assume A,P,C is_coplanar ; :: thesis: b,c // b9,c9
then consider X being Subset of AS such that
A18: A c= X and
A19: P c= X and
A20: C c= X and
A21: X is being_plane ;
consider d being Element of AS such that
A22: not d in X by A1, A21, Th48;
LIN q,a,a9 by A2, A8, A11, AFF_1:21;
then consider d9 being Element of AS such that
A23: LIN q,d,d9 and
A24: a,d // a9,d9 by A5, Th1;
set K = Line (q,d);
A25: d in Line (q,d) by AFF_1:15;
then A26: not Line (q,d) c= X by A22;
A27: q <> d by A2, A18, A22;
then A28: ( q in Line (q,d) & Line (q,d) is being_line ) by AFF_1:15, AFF_1:def 3;
then A29: d9 in Line (q,d) by A25, A27, A23, AFF_1:25;

now :: thesis: ( P <> C implies b,c // b9,c9 )

assume A30: P <> C ; :: thesis: b,c // b9,c9
A31: not Line (q,d),P,C is_coplanar

proof

assume Line (q,d),P,C is_coplanar ; :: thesis: contradiction
then P,C, Line (q,d) is_coplanar ;
hence contradiction by A12, A13, A19, A20, A21, A26, A30, Th46; :: thesis: verum

end;

A32: Line (q,d) <> A by A18, A22, A25;
not A, Line (q,d),P is_coplanar

proof

assume A, Line (q,d),P is_coplanar ; :: thesis: contradiction
then A,P, Line (q,d) is_coplanar ;
hence contradiction by A11, A12, A14, A18, A19, A21, A26, Th46; :: thesis: verum

end;

then A33: d,b // d9,b9 by A2, A3, A5, A6, A8, A9, A11, A12, A14, A16, A25, A27, A28, A24, A29, A32, Lm10;
A34: ( Line (q,d) <> P & Line (q,d) <> C ) by A19, A20, A22, A25;
not A, Line (q,d),C is_coplanar

proof

assume A, Line (q,d),C is_coplanar ; :: thesis: contradiction
then A,C, Line (q,d) is_coplanar ;
hence contradiction by A11, A13, A15, A18, A20, A21, A26, Th46; :: thesis: verum

end;

then d,c // d9,c9 by A2, A4, A5, A7, A8, A10, A11, A13, A15, A17, A25, A27, A28, A24, A29, A32, Lm10;
hence b,c // b9,c9 by A3, A4, A6, A7, A9, A10, A12, A13, A25, A27, A28, A29, A34, A31, A33, Lm10; :: thesis: verum

end;

hence b,c // b9,c9 by A9, A10, A12, AFF_1:51; :: thesis: verum

end;

hence b,c // b9,c9 by A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, Lm10; :: thesis: verum