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;

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;

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 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

A61:
Line (a,c) // Line (a9,c9)
by A14, A15, A55, AFF_1:37;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;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

now :: thesis: not x = y

hence
contradiction
by A58; :: thesis: verumassume
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;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

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

hence
b,c // b9,c9
by A25; :: thesis: verumassume
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;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