let AS be AffinSpace; :: thesis: for q, a, b, c, a', b', c' being Element of
for A, P, C being Subset of st AS is not AffinPlane & q in A & q in P & q in C & q <> a & q <> b & q <> c & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' holds
b,c // b',c'
let q, a, b, c, a', b', c' be Element of ; :: thesis: for A, P, C being Subset of st AS is not AffinPlane & q in A & q in P & q in C & q <> a & q <> b & q <> c & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' holds
b,c // b',c'
let A, P, C be Subset of ; :: thesis: ( AS is not AffinPlane & q in A & q in P & q in C & q <> a & q <> b & q <> c & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' implies b,c // b',c' )
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 & a' in A ) and
A9: ( b in P & b' in P ) and
A10: ( c in C & c' 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 // a',b' and
A17: a,c // a',c' ; :: thesis: b,c // b',c'

now

assume A,P,C is_coplanar ; :: thesis: b,c // b',c'
then consider X being Subset of such that
A18: A c= X and
A19: P c= X and
A20: C c= X and
A21: X is being_plane by Def5;
consider d being Element of such that
A22: not d in X by A1, A21, Th48;
LIN q,a,a' by A2, A8, A11, AFF_1:33;
then consider d' being Element of such that
A23: LIN q,d,d' and
A24: a,d // a',d' by A5, Th1;
set K = Line q,d;
A25: d in Line q,d by AFF_1:26;
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:26, AFF_1:def 3;
then A29: d' in Line q,d by A25, A27, A23, AFF_1:39;

now

assume A30: P <> C ; :: thesis: b,c // b',c'
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 by Th44;
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 by Th44;
hence contradiction by A11, A12, A14, A18, A19, A21, A26, Th46; :: thesis: verum

end;

then A33: d,b // d',b' 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 by Th44;
hence contradiction by A11, A13, A15, A18, A20, A21, A26, Th46; :: thesis: verum

end;

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

end;

hence b,c // b',c' by A9, A10, A12, AFF_1:65; :: thesis: verum

end;

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