let AS be AffinSpace; for q, a, b, c, a9, b9, c9 being Element of AS
for A, P, C 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 q, a, b, c, a9, b9, c9 be Element of AS; for A, P, C 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, P, C be Subset of AS; ( 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
; b,c // b9,c9
A21:
c <> a
by A1, A3, A5, A8, A12, A14, A16, A18, AFF_1:30;
A22:
P <> C
by A1, A2, A4, A14, A15, Th47;
then A23:
b <> c
by A2, A3, A6, A10, A12, A15, A16, AFF_1:30;
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:30;
A30:
now assume A31:
q <> a9
;
b,c // b9,c9then A32:
q <> c9
by A1, A3, A5, A7, A8, A9, A12, A14, A16, A18, A20, Th8;
A33:
now 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
;
b,c // b9,c9assume A35:
not
b,
c // b9,
c9
;
contradictionA36:
(
b9 in Line b9,
c9 &
c9 in Line b9,
c9 )
by AFF_1:26;
A37:
Line b,
c c= X
by A10, A12, A24, A25, A23, Th19;
A38:
c in Line b,
c
by AFF_1:26;
A39:
(
Line b,
c is
being_line &
b in Line b,
c )
by A23, AFF_1:26, AFF_1:def 3;
A40:
c9 <> b9
by A2, A3, A11, A13, A15, A16, A22, A32, AFF_1:30;
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:53;
A44:
a9 in Line a9,
c9
by AFF_1:26;
LIN c9,
b9,
p
by A41, A36, A43, AFF_1:33;
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:26;
LIN c,
b,
p
by A39, A38, A42, AFF_1:33;
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:26;
A51:
(
Line a,
c is
being_line &
a in Line a,
c )
by A21, AFF_1:26, AFF_1:def 3;
then A52:
x in Line a,
c
by A21, A47, A48, AFF_1:39;
set K =
p * (Line a,b);
A53:
b in Line a,
b
by AFF_1:26;
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:13;
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:30;
p,
y // a9,
b9
by A46, AFF_1:13;
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:51;
then
Line a9,
b9 // p * (Line a,b)
by A55, AFF_1:58;
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:26;
A63:
a9 <> c9
by A1, A3, A9, A13, A14, A16, A18, A31, AFF_1:30;
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:39;
A65:
Line a9,
c9 c= Y
by A9, A13, A26, A27, A28, A63, Th19;
A66:
now assume A67:
x <> y
;
contradictionthen
p * (Line a,b) = Line x,
y
by A54, A57, A60, Th27, AFF_1:71;
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:71;
then
P c= Y
by A1, A6, A26, A28, A53, A68, Th19;
hence
contradiction
by A4, A26, A27, A28, Def5;
verum end; A69:
Line a,
c // Line a9,
c9
by A20, A21, A63, AFF_1:51;
now assume
x = y
;
contradictionthen
a9 in Line a,
c
by A44, A69, A52, A64, AFF_1:59;
then
c in A
by A8, A9, A14, A34, A51, A47, AFF_1:30;
hence
contradiction
by A1, A3, A7, A12, A14, A16, A18, AFF_1:30;
verum end; hence
contradiction
by A66;
verum end; now assume
a = a9
;
b,c // b9,c9then
(
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:11;
verum end; hence
b,
c // b9,
c9
by A33;
verum end;
now assume
q = a9
;
b,c // b9,c9then
(
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:12;
verum end;
hence
b,c // b9,c9
by A30; verum