let S be IncSpace; for A being POINT of S ex L, L1, L2 being LINE of S st
( A on L & A on L1 & A on L2 & ( for P being PLANE of S holds
( not L on P or not L1 on P or not L2 on P ) ) )
let A be POINT of S; ex L, L1, L2 being LINE of S st
( A on L & A on L1 & A on L2 & ( for P being PLANE of S holds
( not L on P or not L1 on P or not L2 on P ) ) )
consider P being PLANE of S such that
A1:
{A,A,A} on P
by Def12;
A on P
by A1, Th4;
then consider L, L1, L2 being LINE of S such that
A2:
L1 <> L2
and
A3:
L1 on P
and
A4:
L2 on P
and
A5:
not L on P
and
A6:
A on L
and
A7:
A on L1
and
A8:
A on L2
by Th50;
consider B being POINT of S such that
A9:
A <> B
and
A10:
B on L1
by Lm1;
consider C being POINT of S such that
A11:
A <> C
and
A12:
C on L2
by Lm1;
A13:
C on P
by A4, A12, Def17;
A14:
{A,B} on L1
by A7, A10, Th1;
then
{A,B} on P
by A3, Th14;
then
{A,B} \/ {C} on P
by A13, Th9;
then A15:
{A,B,C} on P
by ENUMSET1:3;
take
L
; ex L1, L2 being LINE of S st
( A on L & A on L1 & A on L2 & ( for P being PLANE of S holds
( not L on P or not L1 on P or not L2 on P ) ) )
take
L1
; ex L2 being LINE of S st
( A on L & A on L1 & A on L2 & ( for P being PLANE of S holds
( not L on P or not L1 on P or not L2 on P ) ) )
take
L2
; ( A on L & A on L1 & A on L2 & ( for P being PLANE of S holds
( not L on P or not L1 on P or not L2 on P ) ) )
thus
( A on L & A on L1 & A on L2 )
by A6, A7, A8; for P being PLANE of S holds
( not L on P or not L1 on P or not L2 on P )
given Q being PLANE of S such that A16:
L on Q
and
A17:
L1 on Q
and
A18:
L2 on Q
; contradiction
A19:
C on Q
by A18, A12, Def17;
A20:
{A,C} on L2
by A8, A12, Th1;
now for K being LINE of S holds not {A,B,C} on Kgiven K being
LINE of
S such that A21:
{A,B,C} on K
;
contradiction
{A,C,B} on K
by A21, ENUMSET1:57;
then
{A,C} \/ {B} on K
by ENUMSET1:3;
then A22:
{A,C} on K
by Th8;
{A,B} \/ {C} on K
by A21, ENUMSET1:3;
then
{A,B} on K
by Th8;
then
K = L1
by A9, A14, Def10;
hence
contradiction
by A2, A11, A20, A22, Def10;
verum end;
then A23:
not {A,B,C} is linear
;
{A,B} on Q
by A17, A14, Th14;
then
{A,B} \/ {C} on Q
by A19, Th9;
then
{A,B,C} on Q
by ENUMSET1:3;
hence
contradiction
by A5, A16, A15, A23, Def13; verum