let AS be AffinSpace; for a, b, c, a9, b9, c9 being Element of AS
for A, C, P being Subset of AS st AS is not AffinPlane & A // P & A // 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, b, c, a9, b9, c9 be Element of AS; for A, C, P being Subset of AS st AS is not AffinPlane & A // P & A // 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, C, P be Subset of AS; ( AS is not AffinPlane & A // P & A // 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:
AS is not AffinPlane
and
A2:
A // P
and
A3:
A // C
and
A4:
( a in A & a9 in A )
and
A5:
( b in P & b9 in P )
and
A6:
( c in C & c9 in C )
and
A7:
A is being_line
and
A8:
P is being_line
and
A9:
C is being_line
and
A10:
A <> P
and
A11:
A <> C
and
A12:
a,b // a9,b9
and
A13:
a,c // a9,c9
; b,c // b9,c9
now ( A,P,C is_coplanar implies b,c // b9,c9 )assume
A,
P,
C is_coplanar
;
b,c // b9,c9then consider X being
Subset of
AS such that A14:
A c= X
and A15:
P c= X
and A16:
C c= X
and A17:
X is
being_plane
;
consider d being
Element of
AS such that A18:
not
d in X
by A1, A17, Th48;
set K =
d * A;
A19:
d in d * A
by A7, Def3;
then A20:
not
d * A c= X
by A18;
A21:
A // d * A
by A7, Def3;
ex
d9 being
Element of
AS st
(
d9 in d * A &
a,
d // a9,
d9 )
proof
A22:
now ( a <> a9 implies ex d9 being Element of AS st
( d9 in d * A & a,d // a9,d9 ) )assume A23:
a <> a9
;
ex d9 being Element of AS st
( d9 in d * A & a,d // a9,d9 )consider d9 being
Element of
AS such that A24:
a,
a9 // d,
d9
and A25:
a,
d // a9,
d9
by DIRAF:40;
d,
d9 // a,
a9
by A24, AFF_1:4;
then
d,
d9 // A
by A4, A7, A23, AFF_1:27;
then
d,
d9 // d * A
by A21, Th3;
then
d9 in d * A
by A19, Th2;
hence
ex
d9 being
Element of
AS st
(
d9 in d * A &
a,
d // a9,
d9 )
by A25;
verum end;
now ( a = a9 implies ex d9 being Element of AS st
( d9 in d * A & a,d // a9,d9 ) )assume A26:
a = a9
;
ex d9 being Element of AS st
( d9 in d * A & a,d // a9,d9 )take d9 =
d;
( d9 in d * A & a,d // a9,d9 )thus
d9 in d * A
by A7, Def3;
a,d // a9,d9thus
a,
d // a9,
d9
by A26, AFF_1:2;
verum end;
hence
ex
d9 being
Element of
AS st
(
d9 in d * A &
a,
d // a9,
d9 )
by A22;
verum
end; then consider d9 being
Element of
AS such that A27:
d9 in d * A
and A28:
a,
d // a9,
d9
;
A29:
(
d * A // P &
d * A // C )
by A2, A3, A21, AFF_1:44;
now ( P <> C implies b,c // b9,c9 )assume A30:
P <> C
;
b,c // b9,c9A31:
not
d * A,
P,
C is_coplanar
proof
assume
d * A,
P,
C is_coplanar
;
contradiction
then
P,
C,
d * A is_coplanar
;
hence
contradiction
by A8, A9, A15, A16, A17, A20, A30, Th46;
verum
end; A32:
d * A <> A
by A14, A18, A19;
not
A,
d * A,
P is_coplanar
proof
assume
A,
d * A,
P is_coplanar
;
contradiction
then
A,
P,
d * A is_coplanar
;
hence
contradiction
by A7, A8, A10, A14, A15, A17, A20, Th46;
verum
end; then A33:
d,
b // d9,
b9
by A2, A4, A5, A7, A10, A12, A19, A21, A27, A28, A32, Lm11;
A34:
(
d * A <> P &
d * A <> C )
by A15, A16, A18, A19;
not
A,
d * A,
C is_coplanar
proof
assume
A,
d * A,
C is_coplanar
;
contradiction
then
A,
C,
d * A is_coplanar
;
hence
contradiction
by A7, A9, A11, A14, A16, A17, A20, Th46;
verum
end; then
d,
c // d9,
c9
by A3, A4, A6, A7, A11, A13, A19, A21, A27, A28, A32, Lm11;
hence
b,
c // b9,
c9
by A5, A6, A7, A19, A29, A27, A34, A31, A33, Lm11, Th27;
verum end; hence
b,
c // b9,
c9
by A5, A6, A8, AFF_1:51;
verum end;
hence
b,c // b9,c9
by A2, A3, A4, A5, A6, A7, A10, A11, A12, A13, Lm11; verum