begin
:: deftheorem Def1 defines on INCSP_1:def 1 :
for S being IncProjStr
for A being POINT of S
for L being LINE of S holds
( A on L iff [A,L] in the Inc of S );
:: deftheorem Def2 defines on INCSP_1:def 2 :
for S being IncStruct
for A being POINT of S
for P being PLANE of S holds
( A on P iff [A,P] in the Inc2 of S );
:: deftheorem Def3 defines on INCSP_1:def 3 :
for S being IncStruct
for L being LINE of S
for P being PLANE of S holds
( L on P iff [L,P] in the Inc3 of S );
:: deftheorem Def4 defines on INCSP_1:def 4 :
for S being IncProjStr
for F being Subset of the Points of S
for L being LINE of S holds
( F on L iff for A being POINT of S st A in F holds
A on L );
:: deftheorem Def5 defines on INCSP_1:def 5 :
for S being IncStruct
for F being Subset of the Points of S
for P being PLANE of S holds
( F on P iff for A being POINT of S st A in F holds
A on P );
:: deftheorem Def6 defines linear INCSP_1:def 6 :
for S being IncProjStr
for F being Subset of the Points of S holds
( F is linear iff ex L being LINE of S st F on L );
:: deftheorem Def7 defines planar INCSP_1:def 7 :
for S being IncStruct
for F being Subset of the Points of S holds
( F is planar iff ex P being PLANE of S st F on P );
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem
theorem
:: deftheorem Def8 defines with_non-trivial_lines INCSP_1:def 8 :
for S being IncProjStr holds
( S is with_non-trivial_lines iff for L being LINE of S ex A, B being POINT of S st
( A <> B & {A,B} on L ) );
:: deftheorem Def9 defines linear INCSP_1:def 9 :
for S being IncProjStr holds
( S is linear iff for A, B being POINT of S ex L being LINE of S st {A,B} on L );
:: deftheorem Def10 defines up-2-rank INCSP_1:def 10 :
for S being IncProjStr holds
( S is up-2-rank iff for A, B being POINT of S
for K, L being LINE of S st A <> B & {A,B} on K & {A,B} on L holds
K = L );
definition
let S be
IncStruct ;
attr S is
with_non-empty_planes means :
Def11:
for
P being
PLANE of
S ex
A being
POINT of
S st
A on P;
attr S is
planar means :
Def12:
for
A,
B,
C being
POINT of
S ex
P being
PLANE of
S st
{A,B,C} on P;
attr S is
with_<=1_plane_per_3_pts means :
Def13:
for
A,
B,
C being
POINT of
S for
P,
Q being
PLANE of
S st not
{A,B,C} is
linear &
{A,B,C} on P &
{A,B,C} on Q holds
P = Q;
attr S is
with_lines_inside_planes means :
Def14:
for
L being
LINE of
S for
P being
PLANE of
S st ex
A,
B being
POINT of
S st
(
A <> B &
{A,B} on L &
{A,B} on P ) holds
L on P;
attr S is
with_planes_intersecting_in_2_pts means :
Def15:
for
A being
POINT of
S for
P,
Q being
PLANE of
S st
A on P &
A on Q holds
ex
B being
POINT of
S st
(
A <> B &
B on P &
B on Q );
attr S is
up-3-dimensional means :
Def16:
not for
A,
B,
C,
D being
POINT of
S holds
{A,B,C,D} is
planar ;
attr S is
inc-compatible means :
Def17:
for
A being
POINT of
S for
L being
LINE of
S for
P being
PLANE of
S st
A on L &
L on P holds
A on P;
end;
:: deftheorem Def11 defines with_non-empty_planes INCSP_1:def 11 :
for S being IncStruct holds
( S is with_non-empty_planes iff for P being PLANE of S ex A being POINT of S st A on P );
:: deftheorem Def12 defines planar INCSP_1:def 12 :
for S being IncStruct holds
( S is planar iff for A, B, C being POINT of S ex P being PLANE of S st {A,B,C} on P );
:: deftheorem Def13 defines with_<=1_plane_per_3_pts INCSP_1:def 13 :
for S being IncStruct holds
( S is with_<=1_plane_per_3_pts iff for A, B, C being POINT of S
for P, Q being PLANE of S st not {A,B,C} is linear & {A,B,C} on P & {A,B,C} on Q holds
P = Q );
:: deftheorem Def14 defines with_lines_inside_planes INCSP_1:def 14 :
for S being IncStruct holds
( S is with_lines_inside_planes iff for L being LINE of S
for P being PLANE of S st ex A, B being POINT of S st
( A <> B & {A,B} on L & {A,B} on P ) holds
L on P );
:: deftheorem Def15 defines with_planes_intersecting_in_2_pts INCSP_1:def 15 :
for S being IncStruct holds
( S is with_planes_intersecting_in_2_pts iff for A being POINT of S
for P, Q being PLANE of S st A on P & A on Q holds
ex B being POINT of S st
( A <> B & B on P & B on Q ) );
:: deftheorem Def16 defines up-3-dimensional INCSP_1:def 16 :
for S being IncStruct holds
( S is up-3-dimensional iff not for A, B, C, D being POINT of S holds {A,B,C,D} is planar );
:: deftheorem Def17 defines inc-compatible INCSP_1:def 17 :
for S being IncStruct holds
( S is inc-compatible iff for A being POINT of S
for L being LINE of S
for P being PLANE of S st A on L & L on P holds
A on P );
:: deftheorem Def18 defines IncSpace-like INCSP_1:def 18 :
for IT being IncStruct holds
( IT is IncSpace-like iff ( IT is with_non-trivial_lines & IT is linear & IT is up-2-rank & IT is with_non-empty_planes & IT is planar & IT is with_<=1_plane_per_3_pts & IT is with_lines_inside_planes & IT is with_planes_intersecting_in_2_pts & IT is up-3-dimensional & IT is inc-compatible ) );
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th35:
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
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 Th44:
theorem Th45:
theorem
theorem
theorem Th48:
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 Th49:
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 )
:: deftheorem Def19 defines Line INCSP_1:def 19 :
for S being IncSpace
for A, B being POINT of S st A <> B holds
for b4 being LINE of S holds
( b4 = Line (A,B) iff {A,B} on b4 );
definition
let S be
IncSpace;
let A,
B,
C be
POINT of
S;
assume A1:
not
{A,B,C} is
linear
;
func Plane (
A,
B,
C)
-> PLANE of
S means :
Def20:
{A,B,C} on it;
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;
:: deftheorem Def20 defines Plane INCSP_1:def 20 :
for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is linear holds
for b5 being PLANE of S holds
( b5 = Plane (A,B,C) iff {A,B,C} on b5 );
:: deftheorem Def21 defines Plane INCSP_1:def 21 :
for S being IncSpace
for A being POINT of S
for L being LINE of S st not A on L holds
for b4 being PLANE of S holds
( b4 = Plane (A,L) iff ( A on b4 & L on b4 ) );
:: deftheorem Def22 defines Plane INCSP_1:def 22 :
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
for b4 being PLANE of S holds
( b4 = Plane (K,L) iff ( K on b4 & L on b4 ) );
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th58:
theorem Th59:
theorem
theorem Th61:
theorem
theorem
canceled;
theorem
theorem Th65:
theorem
theorem
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
theorem
theorem
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 Th71:
theorem
theorem
theorem Th74:
theorem Th75:
theorem Th76:
theorem Th77:
theorem
theorem
theorem Th80:
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
theorem
theorem
theorem
theorem
canceled;
theorem
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 ) )