let AS be AffinSpace; for a, a', b, b', c, c' being Element of
for A, P, C being Subset of st A // P & A // C & not A,P,C is_coplanar & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' holds
b,c // b',c'
let a, a', b, b', c, c' be Element of ; for A, P, C being Subset of st A // P & A // C & not A,P,C is_coplanar & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' holds
b,c // b',c'
let A, P, C be Subset of ; ( A // P & A // C & not A,P,C is_coplanar & a in A & a' in A & b in P & b' in P & c in C & c' in C & A is being_line & A <> P & A <> C & a,b // a',b' & a,c // a',c' implies b,c // b',c' )
assume that
A1:
A // P
and
A2:
A // C
and
A3:
not A,P,C is_coplanar
and
A4:
a in A
and
A5:
a' in A
and
A6:
b in P
and
A7:
b' in P
and
A8:
c in C
and
A9:
c' in C
and
A10:
A is being_line
and
A11:
A <> P
and
A12:
A <> C
and
A13:
a,b // a',b'
and
A14:
a,c // a',c'
; b,c // b',c'
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 such that
A17:
( P c= X & C c= X )
and
A18:
X is being_plane
by Th39;
consider Y being Subset of 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 BC' =
Line b',
c';
set AB =
Line a,
b;
set AB' =
Line a',
b';
set AC =
Line a,
c;
set AC' =
Line a',
c';
assume A26:
a <> a'
;
b,c // b',c'assume A27:
not
b,
c // b',
c'
;
contradictionA28:
(
b' in Line b',
c' &
c' in Line b',
c' )
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:
c' <> b'
by A7, A9, A16, A22, AFF_1:59;
then A33:
Line b',
c' is
being_line
by AFF_1:def 3;
Line b',
c' c= X
by A7, A9, A17, A18, A32, Th19;
then consider p being
Element of
such that A34:
p in Line b,
c
and A35:
p in Line b',
c'
by A18, A27, A33, A31, A30, A28, A29, Th22, AFF_1:53;
A36:
a' in Line a',
c'
by AFF_1:26;
LIN c',
b',
p
by A33, A28, A35, AFF_1:33;
then consider y being
Element of
such that A37:
LIN c',
a',
y
and A38:
b',
a' // 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
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:
a' <> b'
by A1, A5, A7, A11, AFF_1:59;
p,
y // a',
b'
by A38, AFF_1:13;
then A51:
p,
y // Line a',
b'
by A50, AFF_1:def 4;
Line a,
b // Line a',
b'
by A13, A24, A50, AFF_1:51;
then
Line a',
b' // 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:
c' in Line a',
c'
by AFF_1:26;
A55:
a' <> c'
by A2, A5, A9, A12, AFF_1:59;
then
Line a',
c' is
being_line
by AFF_1:def 3;
then A56:
y in Line a',
c'
by A55, A36, A54, A37, AFF_1:39;
A57:
Line a',
c' 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 a',
c'
by A14, A15, A55, AFF_1:51;
now assume
x = y
;
contradictionthen
a' 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 = a'
;
b,c // b',c'then
(
b = b' &
c = c' )
by A1, A2, A4, A6, A7, A8, A9, A11, A12, A13, A14, Th10;
hence
b,
c // b',
c'
by AFF_1:11;
verum end;
hence
b,c // b',c'
by A25; verum