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 q in A & q in P & q in C & not A,P,C is_coplanar & 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 q in A & q in P & q in C & not A,P,C is_coplanar & 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: ( q in A & q in P & q in C & not A,P,C is_coplanar & 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: q in A and

A2: q in P and

A3: q in C and

A4: not A,P,C is_coplanar and

A5: q <> a and

A6: q <> b and

A7: q <> c and

A8: a in A and

A9: a9 in A and

A10: b in P and

A11: b9 in P and

A12: c in C and

A13: c9 in C and

A14: A is being_line and

A15: P is being_line and

A16: C is being_line and

A17: A <> P and

A18: A <> C and

A19: a,b // a9,b9 and

A20: a,c // a9,c9 ; :: thesis: b,c // b9,c9

A21: c <> a by A1, A3, A5, A8, A12, A14, A16, A18, AFF_1:18;

A22: P <> C by A1, A2, A4, A14, A15, Th47;

then A23: b <> c by A2, A3, A6, A10, A12, A15, A16, AFF_1:18;

consider X being Subset of AS such that

A24: ( P c= X & C c= X ) and

A25: X is being_plane by A2, A3, A15, A16, Th38;

consider Y being Subset of AS such that

A26: A c= Y and

A27: C c= Y and

A28: Y is being_plane by A1, A3, A14, A16, Th38;

A29: a <> b by A1, A2, A5, A8, A10, A14, A15, A17, AFF_1:18;

for A, C, P being Subset of AS st q in A & q in P & q in C & not A,P,C is_coplanar & 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 q in A & q in P & q in C & not A,P,C is_coplanar & 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: ( q in A & q in P & q in C & not A,P,C is_coplanar & 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: q in A and

A2: q in P and

A3: q in C and

A4: not A,P,C is_coplanar and

A5: q <> a and

A6: q <> b and

A7: q <> c and

A8: a in A and

A9: a9 in A and

A10: b in P and

A11: b9 in P and

A12: c in C and

A13: c9 in C and

A14: A is being_line and

A15: P is being_line and

A16: C is being_line and

A17: A <> P and

A18: A <> C and

A19: a,b // a9,b9 and

A20: a,c // a9,c9 ; :: thesis: b,c // b9,c9

A21: c <> a by A1, A3, A5, A8, A12, A14, A16, A18, AFF_1:18;

A22: P <> C by A1, A2, A4, A14, A15, Th47;

then A23: b <> c by A2, A3, A6, A10, A12, A15, A16, AFF_1:18;

consider X being Subset of AS such that

A24: ( P c= X & C c= X ) and

A25: X is being_plane by A2, A3, A15, A16, Th38;

consider Y being Subset of AS such that

A26: A c= Y and

A27: C c= Y and

A28: Y is being_plane by A1, A3, A14, A16, Th38;

A29: a <> b by A1, A2, A5, A8, A10, A14, A15, A17, AFF_1:18;

A30: now :: thesis: ( q <> a9 implies b,c // b9,c9 )

assume A31:
q <> a9
; :: thesis: b,c // b9,c9

then A32: q <> c9 by A1, A3, A5, A7, A8, A9, A12, A14, A16, A18, A20, Th8;

end;then A32: q <> c9 by A1, A3, A5, A7, A8, A9, A12, A14, A16, A18, A20, Th8;

A33: now :: thesis: ( a <> a9 implies b,c // b9,c9 )

set BC = Line (b,c);

set BC9 = Line (b9,c9);

set AB = Line (a,b);

set AB9 = Line (a9,b9);

set AC = Line (a,c);

set AC9 = Line (a9,c9);

assume A34: a <> a9 ; :: thesis: b,c // b9,c9

assume A35: not b,c // b9,c9 ; :: thesis: contradiction

A36: ( b9 in Line (b9,c9) & c9 in Line (b9,c9) ) by AFF_1:15;

A37: Line (b,c) c= X by A10, A12, A24, A25, A23, Th19;

A38: c in Line (b,c) by AFF_1:15;

A39: ( Line (b,c) is being_line & b in Line (b,c) ) by A23, AFF_1:15, AFF_1:def 3;

A40: c9 <> b9 by A2, A3, A11, A13, A15, A16, A22, A32, AFF_1:18;

then A41: Line (b9,c9) is being_line by AFF_1:def 3;

Line (b9,c9) c= X by A11, A13, A24, A25, A40, Th19;

then consider p being Element of AS such that

A42: p in Line (b,c) and

A43: p in Line (b9,c9) by A25, A35, A41, A39, A38, A36, A37, Th22, AFF_1:39;

A44: a9 in Line (a9,c9) by AFF_1:15;

LIN c9,b9,p by A41, A36, A43, AFF_1:21;

then consider y being Element of AS such that

A45: LIN c9,a9,y and

A46: b9,a9 // p,y by A40, Th1;

A47: c in Line (a,c) by AFF_1:15;

LIN c,b,p by A39, A38, A42, AFF_1:21;

then consider x being Element of AS such that

A48: LIN c,a,x and

A49: b,a // p,x by A23, Th1;

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

A51: ( Line (a,c) is being_line & a in Line (a,c) ) by A21, AFF_1:15, AFF_1:def 3;

then A52: x in Line (a,c) by A21, A47, A48, AFF_1:25;

set K = p * (Line (a,b));

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

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

then A55: Line (a,b) // p * (Line (a,b)) by Def3;

A56: p in p * (Line (a,b)) by A54, Def3;

p,x // a,b by A49, AFF_1:4;

then p,x // Line (a,b) by A29, AFF_1:def 4;

then p,x // p * (Line (a,b)) by A55, Th3;

then A57: x in p * (Line (a,b)) by A56, Th2;

A58: a9 <> b9 by A1, A2, A9, A11, A14, A15, A17, A31, AFF_1:18;

p,y // a9,b9 by A46, AFF_1:4;

then A59: p,y // Line (a9,b9) by A58, AFF_1:def 4;

Line (a,b) // Line (a9,b9) by A19, A29, A58, AFF_1:37;

then Line (a9,b9) // p * (Line (a,b)) by A55, AFF_1:44;

then p,y // p * (Line (a,b)) by A59, Th3;

then A60: y in p * (Line (a,b)) by A56, Th2;

A61: Line (a,c) c= Y by A8, A12, A26, A27, A28, A21, Th19;

A62: c9 in Line (a9,c9) by AFF_1:15;

A63: a9 <> c9 by A1, A3, A9, A13, A14, A16, A18, A31, AFF_1:18;

then Line (a9,c9) is being_line by AFF_1:def 3;

then A64: y in Line (a9,c9) by A63, A44, A62, A45, AFF_1:25;

A65: Line (a9,c9) c= Y by A9, A13, A26, A27, A28, A63, Th19;

end;set BC9 = Line (b9,c9);

set AB = Line (a,b);

set AB9 = Line (a9,b9);

set AC = Line (a,c);

set AC9 = Line (a9,c9);

assume A34: a <> a9 ; :: thesis: b,c // b9,c9

assume A35: not b,c // b9,c9 ; :: thesis: contradiction

A36: ( b9 in Line (b9,c9) & c9 in Line (b9,c9) ) by AFF_1:15;

A37: Line (b,c) c= X by A10, A12, A24, A25, A23, Th19;

A38: c in Line (b,c) by AFF_1:15;

A39: ( Line (b,c) is being_line & b in Line (b,c) ) by A23, AFF_1:15, AFF_1:def 3;

A40: c9 <> b9 by A2, A3, A11, A13, A15, A16, A22, A32, AFF_1:18;

then A41: Line (b9,c9) is being_line by AFF_1:def 3;

Line (b9,c9) c= X by A11, A13, A24, A25, A40, Th19;

then consider p being Element of AS such that

A42: p in Line (b,c) and

A43: p in Line (b9,c9) by A25, A35, A41, A39, A38, A36, A37, Th22, AFF_1:39;

A44: a9 in Line (a9,c9) by AFF_1:15;

LIN c9,b9,p by A41, A36, A43, AFF_1:21;

then consider y being Element of AS such that

A45: LIN c9,a9,y and

A46: b9,a9 // p,y by A40, Th1;

A47: c in Line (a,c) by AFF_1:15;

LIN c,b,p by A39, A38, A42, AFF_1:21;

then consider x being Element of AS such that

A48: LIN c,a,x and

A49: b,a // p,x by A23, Th1;

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

A51: ( Line (a,c) is being_line & a in Line (a,c) ) by A21, AFF_1:15, AFF_1:def 3;

then A52: x in Line (a,c) by A21, A47, A48, AFF_1:25;

set K = p * (Line (a,b));

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

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

then A55: Line (a,b) // p * (Line (a,b)) by Def3;

A56: p in p * (Line (a,b)) by A54, Def3;

p,x // a,b by A49, AFF_1:4;

then p,x // Line (a,b) by A29, AFF_1:def 4;

then p,x // p * (Line (a,b)) by A55, Th3;

then A57: x in p * (Line (a,b)) by A56, Th2;

A58: a9 <> b9 by A1, A2, A9, A11, A14, A15, A17, A31, AFF_1:18;

p,y // a9,b9 by A46, AFF_1:4;

then A59: p,y // Line (a9,b9) by A58, AFF_1:def 4;

Line (a,b) // Line (a9,b9) by A19, A29, A58, AFF_1:37;

then Line (a9,b9) // p * (Line (a,b)) by A55, AFF_1:44;

then p,y // p * (Line (a,b)) by A59, Th3;

then A60: y in p * (Line (a,b)) by A56, Th2;

A61: Line (a,c) c= Y by A8, A12, A26, A27, A28, A21, Th19;

A62: c9 in Line (a9,c9) by AFF_1:15;

A63: a9 <> c9 by A1, A3, A9, A13, A14, A16, A18, A31, AFF_1:18;

then Line (a9,c9) is being_line by AFF_1:def 3;

then A64: y in Line (a9,c9) by A63, A44, A62, A45, AFF_1:25;

A65: Line (a9,c9) c= Y by A9, A13, A26, A27, A28, A63, Th19;

A66: now :: thesis: not x <> y

A69:
Line (a,c) // Line (a9,c9)
by A20, A21, A63, AFF_1:37;assume A67:
x <> y
; :: thesis: contradiction

then p * (Line (a,b)) = Line (x,y) by A54, A57, A60, Th27, AFF_1:57;

then p * (Line (a,b)) c= Y by A28, A61, A65, A52, A64, A67, Th19;

then A68: Line (a,b) c= Y by A8, A26, A28, A50, A55, Th23;

P = Line (q,b) by A2, A6, A10, A15, AFF_1:57;

then P c= Y by A1, A6, A26, A28, A53, A68, Th19;

hence contradiction by A4, A26, A27, A28; :: thesis: verum

end;then p * (Line (a,b)) = Line (x,y) by A54, A57, A60, Th27, AFF_1:57;

then p * (Line (a,b)) c= Y by A28, A61, A65, A52, A64, A67, Th19;

then A68: Line (a,b) c= Y by A8, A26, A28, A50, A55, Th23;

P = Line (q,b) by A2, A6, A10, A15, AFF_1:57;

then P c= Y by A1, A6, A26, A28, A53, A68, Th19;

hence contradiction by A4, A26, A27, A28; :: thesis: verum

now :: thesis: not x = y

hence
contradiction
by A66; :: thesis: verumassume
x = y
; :: thesis: contradiction

then a9 in Line (a,c) by A44, A69, A52, A64, AFF_1:45;

then c in A by A8, A9, A14, A34, A51, A47, AFF_1:18;

hence contradiction by A1, A3, A7, A12, A14, A16, A18, AFF_1:18; :: thesis: verum

end;then a9 in Line (a,c) by A44, A69, A52, A64, AFF_1:45;

then c in A by A8, A9, A14, A34, A51, A47, AFF_1:18;

hence contradiction by A1, A3, A7, A12, A14, A16, A18, AFF_1:18; :: thesis: verum

now :: thesis: ( a = a9 implies b,c // b9,c9 )

hence
b,c // b9,c9
by A33; :: thesis: verumassume
a = a9
; :: thesis: b,c // b9,c9

then ( b = b9 & c = c9 ) by A1, A2, A3, A5, A6, A7, A8, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, Th9;

hence b,c // b9,c9 by AFF_1:2; :: thesis: verum

end;then ( b = b9 & c = c9 ) by A1, A2, A3, A5, A6, A7, A8, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, Th9;

hence b,c // b9,c9 by AFF_1:2; :: thesis: verum

now :: thesis: ( q = a9 implies b,c // b9,c9 )

hence
b,c // b9,c9
by A30; :: thesis: verumassume
q = a9
; :: thesis: b,c // b9,c9

then ( q = b9 & q = c9 ) by A1, A2, A3, A5, A6, A7, A8, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, Th8;

hence b,c // b9,c9 by AFF_1:3; :: thesis: verum

end;then ( q = b9 & q = c9 ) by A1, A2, A3, A5, A6, A7, A8, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, Th8;

hence b,c // b9,c9 by AFF_1:3; :: thesis: verum