let AS be AffinSpace; for a, a9, b, b9, c, c9 being Element of AS
for A, P, C 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, a9, b, b9, c, c9 be Element of AS; for A, P, C 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, P, C 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:59;
A16:
P // C
by A1, A2, AFF_1:58;
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, Def5;
then A23:
b <> c
by A6, A8, A16, AFF_1:59;
A24:
a <> b
by A1, A4, A6, A11, AFF_1:59;
A25:
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 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:26;
A29:
Line b,
c c= X
by A6, A8, A17, A18, A23, Th19;
A30:
c in Line b,
c
by AFF_1:26;
A31:
(
Line b,
c is
being_line &
b in Line b,
c )
by A23, AFF_1:26, AFF_1:def 3;
A32:
c9 <> b9
by A7, A9, A16, A22, AFF_1:59;
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:53;
A36:
a9 in Line a9,
c9
by AFF_1:26;
LIN c9,
b9,
p
by A33, A28, A35, AFF_1:33;
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:26;
LIN c,
b,
p
by A31, A30, A34, AFF_1:33;
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:26;
A43:
(
Line a,
c is
being_line &
a in Line a,
c )
by A15, AFF_1:26, AFF_1:def 3;
then A44:
x in Line a,
c
by A15, A39, A40, AFF_1:39;
set K =
p * (Line a,b);
A45:
b in Line a,
b
by AFF_1:26;
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:13;
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:59;
p,
y // a9,
b9
by A38, AFF_1:13;
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:51;
then
Line a9,
b9 // p * (Line a,b)
by A47, AFF_1:58;
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:26;
A55:
a9 <> c9
by A2, A5, A9, A12, AFF_1:59;
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:39;
A57:
Line a9,
c9 c= Y
by A5, A9, A19, A20, A21, A55, Th19;
A58:
now assume A59:
x <> y
;
contradictionthen
p * (Line a,b) = Line x,
y
by A46, A49, A52, Th27, AFF_1:71;
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, Def5;
verum end; A61:
Line a,
c // Line a9,
c9
by A14, A15, A55, AFF_1:51;
now assume
x = y
;
contradictionthen
a9 in Line a,
c
by A36, A61, A44, A56, AFF_1:59;
then
c in A
by A4, A5, A10, A26, A43, A39, AFF_1:30;
hence
contradiction
by A2, A8, A12, AFF_1:59;
verum end; hence
contradiction
by A58;
verum end;
now 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:11;
verum end;
hence
b,c // b9,c9
by A25; verum