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

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 )

hence
b,c // b9,c9
by A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, Lm10; :: thesis: verumassume
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;

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

hence
b,c // b9,c9
by A9, A10, A12, AFF_1:51; :: thesis: verumassume A30:
P <> C
; :: thesis: b,c // b9,c9

A31: not Line (q,d),P,C is_coplanar

not A, Line (q,d),P is_coplanar

A34: ( Line (q,d) <> P & Line (q,d) <> C ) by A19, A20, A22, A25;

not A, Line (q,d),C is_coplanar

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;A31: not Line (q,d),P,C is_coplanar

proof

A32:
Line (q,d) <> A
by A18, A22, A25;
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;then P,C, Line (q,d) is_coplanar ;

hence contradiction by A12, A13, A19, A20, A21, A26, A30, Th46; :: thesis: verum

not A, Line (q,d),P is_coplanar

proof

then A33:
d,b // d9,b9
by A2, A3, A5, A6, A8, A9, A11, A12, A14, A16, A25, A27, A28, A24, A29, A32, Lm10;
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 A,P, Line (q,d) is_coplanar ;

hence contradiction by A11, A12, A14, A18, A19, A21, A26, Th46; :: thesis: verum

A34: ( Line (q,d) <> P & Line (q,d) <> C ) by A19, A20, A22, A25;

not A, Line (q,d),C is_coplanar

proof

then
d,c // d9,c9
by A2, A4, A5, A7, A8, A10, A11, A13, A15, A17, A25, A27, A28, A24, A29, A32, Lm10;
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 A,C, Line (q,d) is_coplanar ;

hence contradiction by A11, A13, A15, A18, A20, A21, A26, Th46; :: thesis: verum

hence b,c // b9,c9 by A3, A4, A6, A7, A9, A10, A12, A13, A25, A27, A28, A29, A34, A31, A33, Lm10; :: thesis: verum