let AS be AffinSpace; for q, a, b, c, a9, b9, c9 being Element of AS
for A, P, C 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 q, a, b, c, a9, b9, c9 be Element of AS; for A, P, C 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, P, C 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 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
by Def5;
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:33;
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:26;
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:26, AFF_1:def 3;
then A29:
d9 in Line q,
d
by A25, A27, A23, AFF_1:39;
now 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
by Th44;
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
by Th44;
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
by Th44;
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:65;
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