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;
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;
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;
A66: now :: thesis: not x <> y
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;
A69: Line (a,c) // Line (a9,c9) by A20, A21, A63, AFF_1:37;
hence contradiction by A66; :: thesis: verum
end;
now :: thesis: ( a = a9 implies b,c // b9,c9 )
assume 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;
hence b,c // b9,c9 by A33; :: thesis: verum
end;
now :: thesis: ( q = a9 implies b,c // b9,c9 )
assume 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;
hence b,c // b9,c9 by A30; :: thesis: verum