let AS be AffinSpace; :: thesis: for a, b, c, a9, b9, c9 being Element of AS
for A, C, P being Subset of AS st A // P & A // C & not A,P,C is_coplanar & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A 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 be Element of AS; :: thesis: for A, C, P being Subset of AS st A // P & A // C & not A,P,C is_coplanar & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A 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: ( A // P & A // C & not A,P,C is_coplanar & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & A <> P & A <> C & a,b // a9,b9 & a,c // a9,c9 implies b,c // b9,c9 )
assume that
A1: A // P and
A2: A // C and
A3: not A,P,C is_coplanar and
A4: a in A and
A5: a9 in A and
A6: b in P and
A7: b9 in P and
A8: c in C and
A9: c9 in C and
A10: A is being_line and
A11: A <> P and
A12: A <> C and
A13: a,b // a9,b9 and
A14: a,c // a9,c9 ; :: thesis: b,c // b9,c9
A15: c <> a by A2, A4, A8, A12, AFF_1:45;
A16: P // C by A1, A2, AFF_1:44;
then consider X being Subset of AS such that
A17: ( P c= X & C c= X ) and
A18: X is being_plane by Th39;
consider Y being Subset of AS such that
A19: A c= Y and
A20: C c= Y and
A21: Y is being_plane by A2, Th39;
A22: P <> C by A3, A19, A20, A21;
then A23: b <> c by A6, A8, A16, AFF_1:45;
A24: a <> b by A1, A4, A6, A11, AFF_1:45;
A25: 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 A26: a <> a9 ; :: thesis: b,c // b9,c9
assume A27: not b,c // b9,c9 ; :: thesis: contradiction
A28: ( b9 in Line (b9,c9) & c9 in Line (b9,c9) ) by AFF_1:15;
A29: Line (b,c) c= X by A6, A8, A17, A18, A23, Th19;
A30: c in Line (b,c) by AFF_1:15;
A31: ( Line (b,c) is being_line & b in Line (b,c) ) by A23, AFF_1:15, AFF_1:def 3;
A32: c9 <> b9 by A7, A9, A16, A22, AFF_1:45;
then A33: Line (b9,c9) is being_line by AFF_1:def 3;
Line (b9,c9) c= X by A7, A9, A17, A18, A32, Th19;
then consider p being Element of AS such that
A34: p in Line (b,c) and
A35: p in Line (b9,c9) by A18, A27, A33, A31, A30, A28, A29, Th22, AFF_1:39;
A36: a9 in Line (a9,c9) by AFF_1:15;
LIN c9,b9,p by A33, A28, A35, AFF_1:21;
then consider y being Element of AS such that
A37: LIN c9,a9,y and
A38: b9,a9 // p,y by A32, Th1;
A39: c in Line (a,c) by AFF_1:15;
LIN c,b,p by A31, A30, A34, AFF_1:21;
then consider x being Element of AS such that
A40: LIN c,a,x and
A41: b,a // p,x by A23, Th1;
A42: a in Line (a,b) by AFF_1:15;
A43: ( Line (a,c) is being_line & a in Line (a,c) ) by A15, AFF_1:15, AFF_1:def 3;
then A44: x in Line (a,c) by A15, A39, A40, AFF_1:25;
set K = p * (Line (a,b));
A45: b in Line (a,b) by AFF_1:15;
A46: Line (a,b) is being_line by A24, AFF_1:def 3;
then A47: Line (a,b) // p * (Line (a,b)) by Def3;
A48: p in p * (Line (a,b)) by A46, Def3;
p,x // a,b by A41, AFF_1:4;
then p,x // Line (a,b) by A24, AFF_1:def 4;
then p,x // p * (Line (a,b)) by A47, Th3;
then A49: x in p * (Line (a,b)) by A48, Th2;
A50: a9 <> b9 by A1, A5, A7, A11, AFF_1:45;
p,y // a9,b9 by A38, AFF_1:4;
then A51: p,y // Line (a9,b9) by A50, AFF_1:def 4;
Line (a,b) // Line (a9,b9) by A13, A24, A50, AFF_1:37;
then Line (a9,b9) // p * (Line (a,b)) by A47, AFF_1:44;
then p,y // p * (Line (a,b)) by A51, Th3;
then A52: y in p * (Line (a,b)) by A48, Th2;
A53: Line (a,c) c= Y by A4, A8, A19, A20, A21, A15, Th19;
A54: c9 in Line (a9,c9) by AFF_1:15;
A55: a9 <> c9 by A2, A5, A9, A12, AFF_1:45;
then Line (a9,c9) is being_line by AFF_1:def 3;
then A56: y in Line (a9,c9) by A55, A36, A54, A37, AFF_1:25;
A57: Line (a9,c9) c= Y by A5, A9, A19, A20, A21, A55, Th19;
A58: now :: thesis: not x <> y
assume A59: x <> y ; :: thesis: contradiction
then p * (Line (a,b)) = Line (x,y) by A46, A49, A52, Th27, AFF_1:57;
then p * (Line (a,b)) c= Y by A21, A53, A57, A44, A56, A59, Th19;
then A60: Line (a,b) c= Y by A4, A19, A21, A42, A47, Th23;
P = b * A by A1, A6, A10, Def3;
then P c= Y by A10, A19, A21, A45, A60, Th28;
hence contradiction by A3, A19, A20, A21; :: thesis: verum
end;
A61: Line (a,c) // Line (a9,c9) by A14, A15, A55, AFF_1:37;
now :: thesis: not x = y
assume x = y ; :: thesis: contradiction
then a9 in Line (a,c) by A36, A61, A44, A56, AFF_1:45;
then c in A by A4, A5, A10, A26, A43, A39, AFF_1:18;
hence contradiction by A2, A8, A12, AFF_1:45; :: thesis: verum
end;
hence contradiction by A58; :: 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, A4, A6, A7, A8, A9, A11, A12, A13, A14, Th10;
hence b,c // b9,c9 by AFF_1:2; :: thesis: verum
end;
hence b,c // b9,c9 by A25; :: thesis: verum