let AS be AffinSpace; for a, b, c, a9, b9, c9, q being Element of AS
for A, C, P being Subset of AS st AS is not AffinPlane & q in A & q in P & q in C & 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, b, c, a9, b9, c9, q be Element of AS; for A, C, P being Subset of AS st AS is not AffinPlane & q in A & q in P & q in C & 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, C, P be Subset of AS; ( AS is not AffinPlane & q in A & q in P & q in C & 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:
AS is not AffinPlane
and
A2:
q in A
and
A3:
q in P
and
A4:
q in C
and
A5:
q <> a
and
A6:
q <> b
and
A7:
q <> c
and
A8:
( a in A & a9 in A )
and
A9:
( b in P & b9 in P )
and
A10:
( c in C & c9 in C )
and
A11:
A is being_line
and
A12:
P is being_line
and
A13:
C is being_line
and
A14:
A <> P
and
A15:
A <> C
and
A16:
a,b // a9,b9
and
A17:
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 A18:
A c= X
and A19:
P c= X
and A20:
C c= X
and A21:
X is
being_plane
;
consider d being
Element of
AS such that A22:
not
d in X
by A1, A21, Th48;
LIN q,
a,
a9
by A2, A8, A11, AFF_1:21;
then consider d9 being
Element of
AS such that A23:
LIN q,
d,
d9
and A24:
a,
d // a9,
d9
by A5, Th1;
set K =
Line (
q,
d);
A25:
d in Line (
q,
d)
by AFF_1:15;
then A26:
not
Line (
q,
d)
c= X
by A22;
A27:
q <> d
by A2, A18, A22;
then A28:
(
q in Line (
q,
d) &
Line (
q,
d) is
being_line )
by AFF_1:15, AFF_1:def 3;
then A29:
d9 in Line (
q,
d)
by A25, A27, A23, AFF_1:25;
now ( P <> C implies b,c // b9,c9 )assume A30:
P <> C
;
b,c // b9,c9A31:
not
Line (
q,
d),
P,
C is_coplanar
proof
assume
Line (
q,
d),
P,
C is_coplanar
;
contradiction
then
P,
C,
Line (
q,
d)
is_coplanar
;
hence
contradiction
by A12, A13, A19, A20, A21, A26, A30, Th46;
verum
end; A32:
Line (
q,
d)
<> A
by A18, A22, A25;
not
A,
Line (
q,
d),
P is_coplanar
proof
assume
A,
Line (
q,
d),
P is_coplanar
;
contradiction
then
A,
P,
Line (
q,
d)
is_coplanar
;
hence
contradiction
by A11, A12, A14, A18, A19, A21, A26, Th46;
verum
end; then A33:
d,
b // d9,
b9
by A2, A3, A5, A6, A8, A9, A11, A12, A14, A16, A25, A27, A28, A24, A29, A32, Lm10;
A34:
(
Line (
q,
d)
<> P &
Line (
q,
d)
<> C )
by A19, A20, A22, A25;
not
A,
Line (
q,
d),
C is_coplanar
proof
assume
A,
Line (
q,
d),
C is_coplanar
;
contradiction
then
A,
C,
Line (
q,
d)
is_coplanar
;
hence
contradiction
by A11, A13, A15, A18, A20, A21, A26, Th46;
verum
end; then
d,
c // d9,
c9
by A2, A4, A5, A7, A8, A10, A11, A13, A15, A17, A25, A27, A28, A24, A29, A32, Lm10;
hence
b,
c // b9,
c9
by A3, A4, A6, A7, A9, A10, A12, A13, A25, A27, A28, A29, A34, A31, A33, Lm10;
verum end; hence
b,
c // b9,
c9
by A9, A10, A12, AFF_1:51;
verum end;
hence
b,c // b9,c9
by A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, Lm10; verum