begin
theorem Th19:
for
S being
IncSpace for
A,
B,
C,
D being
POINT of
S for
P being
PLANE of
S st not
{A,B,C} is
linear &
{A,B,C} on P & not
D on P holds
not
{A,B,C,D} is
planar
theorem
for
S being
IncSpace for
K,
L being
LINE of
S st ( for
P being
PLANE of
S holds
( not
K on P or not
L on P ) ) holds
K <> L
Lm1:
for S being IncSpace
for A being POINT of S
for L being LINE of S ex B being POINT of S st
( A <> B & B on L )
theorem
for
S being
IncSpace for
L,
L1,
L2 being
LINE of
S st ( for
P being
PLANE of
S holds
( not
L on P or not
L1 on P or not
L2 on P ) ) & ex
A being
POINT of
S st
(
A on L &
A on L1 &
A on L2 ) holds
L <> L1
theorem
for
S being
IncSpace for
L1,
L2,
L being
LINE of
S for
P being
PLANE of
S st
L1 on P &
L2 on P & not
L on P &
L1 <> L2 holds
for
Q being
PLANE of
S holds
( not
L on Q or not
L1 on Q or not
L2 on Q )
theorem Th26:
for
S being
IncSpace for
A being
POINT of
S for
L being
LINE of
S st not
A on L holds
ex
P being
PLANE of
S st
for
Q being
PLANE of
S holds
( (
A on Q &
L on Q ) iff
P = Q )
theorem Th27:
for
S being
IncSpace for
K,
L being
LINE of
S st
K <> L & ex
A being
POINT of
S st
(
A on K &
A on L ) holds
ex
P being
PLANE of
S st
for
Q being
PLANE of
S holds
( (
K on Q &
L on Q ) iff
P = Q )
definition
let S be
IncSpace;
let A,
B,
C be
POINT of
S;
assume A1:
not
{A,B,C} is
linear
;
correctness
existence
ex b1 being PLANE of S st {A,B,C} on b1;
uniqueness
for b1, b2 being PLANE of S st {A,B,C} on b1 & {A,B,C} on b2 holds
b1 = b2;
by A1, Def12, Def13;
end;
theorem
for
S being
IncSpace for
A,
B,
C,
D being
POINT of
S st not
{A,B,C} is
linear &
D on Plane (
A,
B,
C) holds
{A,B,C,D} is
planar
Lm2:
for S being IncSpace
for P being PLANE of S ex A, B, C, D being POINT of S st
( A on P & not {A,B,C,D} is planar )
theorem
for
S being
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 ) ) )
theorem
for
S being
IncSpace for
P,
Q being
PLANE of
S holds
( not
P <> Q or for
A being
POINT of
S holds
( not
A on P or not
A on Q ) or ex
L being
LINE of
S st
for
B being
POINT of
S holds
( (
B on P &
B on Q ) iff
B on L ) )