let AS be AffinSpace; 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; 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; ( 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
; 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 ( 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
;
b,c // b9,c9assume A27:
not
b,
c // b9,
c9
;
contradictionA28:
(
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 not x <> yassume A59:
x <> y
;
contradictionthen
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;
verum end; A61:
Line (
a,
c)
// Line (
a9,
c9)
by A14, A15, A55, AFF_1:37;
now not x = yassume
x = y
;
contradictionthen
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;
verum end; hence
contradiction
by A58;
verum end;
now ( a = a9 implies b,c // b9,c9 )assume
a = a9
;
b,c // b9,c9then
(
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;
verum end;
hence
b,c // b9,c9
by A25; verum