:: by Wojciech A. Trybulec

::

:: Received April 14, 1989

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

definition

attr c_{1} is strict ;

struct IncProjStr -> ;

aggr IncProjStr(# Points, Lines, Inc #) -> IncProjStr ;

sel Points c_{1} -> non empty set ;

sel Lines c_{1} -> non empty set ;

sel Inc c_{1} -> Relation of the Points of c_{1}, the Lines of c_{1};

end;
struct IncProjStr -> ;

aggr IncProjStr(# Points, Lines, Inc #) -> IncProjStr ;

sel Points c

sel Lines c

sel Inc c

definition

attr c_{1} is strict ;

struct IncStruct -> IncProjStr ;

aggr IncStruct(# Points, Lines, Planes, Inc, Inc2, Inc3 #) -> IncStruct ;

sel Planes c_{1} -> non empty set ;

sel Inc2 c_{1} -> Relation of the Points of c_{1}, the Planes of c_{1};

sel Inc3 c_{1} -> Relation of the Lines of c_{1}, the Planes of c_{1};

end;
struct IncStruct -> IncProjStr ;

aggr IncStruct(# Points, Lines, Planes, Inc, Inc2, Inc3 #) -> IncStruct ;

sel Planes c

sel Inc2 c

sel Inc3 c

definition

let S be IncProjStr ;

mode POINT of S is Element of the Points of S;

mode LINE of S is Element of the Lines of S;

end;
mode POINT of S is Element of the Points of S;

mode LINE of S is Element of the Lines of S;

:: Definitions of predicates: on, is_collinear, is_coplanar

:: 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 );

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 );

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 );

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 );

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 );

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 );

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 );

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 );

:: Definitional theorems of predicates: on, is_collinear, is_coplanar

theorem Th1: :: INCSP_1:1

for S being IncProjStr

for L being LINE of S

for A, B being POINT of S holds

( {A,B} on L iff ( A on L & B on L ) )

for L being LINE of S

for A, B being POINT of S holds

( {A,B} on L iff ( A on L & B on L ) )

proof end;

theorem Th2: :: INCSP_1:2

for S being IncProjStr

for L being LINE of S

for A, B, C being POINT of S holds

( {A,B,C} on L iff ( A on L & B on L & C on L ) )

for L being LINE of S

for A, B, C being POINT of S holds

( {A,B,C} on L iff ( A on L & B on L & C on L ) )

proof end;

theorem Th3: :: INCSP_1:3

for S being IncStruct

for A, B being POINT of S

for P being PLANE of S holds

( {A,B} on P iff ( A on P & B on P ) )

for A, B being POINT of S

for P being PLANE of S holds

( {A,B} on P iff ( A on P & B on P ) )

proof end;

theorem Th4: :: INCSP_1:4

for S being IncStruct

for A, B, C being POINT of S

for P being PLANE of S holds

( {A,B,C} on P iff ( A on P & B on P & C on P ) )

for A, B, C being POINT of S

for P being PLANE of S holds

( {A,B,C} on P iff ( A on P & B on P & C on P ) )

proof end;

theorem Th5: :: INCSP_1:5

for S being IncStruct

for A, B, C, D being POINT of S

for P being PLANE of S holds

( {A,B,C,D} on P iff ( A on P & B on P & C on P & D on P ) )

for A, B, C, D being POINT of S

for P being PLANE of S holds

( {A,B,C,D} on P iff ( A on P & B on P & C on P & D on P ) )

proof end;

theorem Th6: :: INCSP_1:6

for S being IncStruct

for L being LINE of S

for G, F being Subset of the Points of S st G c= F & F on L holds

G on L

for L being LINE of S

for G, F being Subset of the Points of S st G c= F & F on L holds

G on L

proof end;

theorem Th7: :: INCSP_1:7

for S being IncStruct

for P being PLANE of S

for G, F being Subset of the Points of S st G c= F & F on P holds

G on P

for P being PLANE of S

for G, F being Subset of the Points of S st G c= F & F on P holds

G on P

proof end;

theorem Th8: :: INCSP_1:8

for S being IncStruct

for A being POINT of S

for L being LINE of S

for F being Subset of the Points of S holds

( ( F on L & A on L ) iff F \/ {A} on L )

for A being POINT of S

for L being LINE of S

for F being Subset of the Points of S holds

( ( F on L & A on L ) iff F \/ {A} on L )

proof end;

theorem Th9: :: INCSP_1:9

for S being IncStruct

for A being POINT of S

for P being PLANE of S

for F being Subset of the Points of S holds

( ( F on P & A on P ) iff F \/ {A} on P )

for A being POINT of S

for P being PLANE of S

for F being Subset of the Points of S holds

( ( F on P & A on P ) iff F \/ {A} on P )

proof end;

theorem Th10: :: INCSP_1:10

for S being IncStruct

for L being LINE of S

for F, G being Subset of the Points of S holds

( F \/ G on L iff ( F on L & G on L ) )

for L being LINE of S

for F, G being Subset of the Points of S holds

( F \/ G on L iff ( F on L & G on L ) )

proof end;

theorem Th11: :: INCSP_1:11

for S being IncStruct

for P being PLANE of S

for F, G being Subset of the Points of S holds

( F \/ G on P iff ( F on P & G on P ) )

for P being PLANE of S

for F, G being Subset of the Points of S holds

( F \/ G on P iff ( F on P & G on P ) )

proof end;

theorem :: INCSP_1:12

for S being IncStruct

for G, F being Subset of the Points of S st G c= F & F is linear holds

G is linear

for G, F being Subset of the Points of S st G c= F & F is linear holds

G is linear

proof end;

theorem :: INCSP_1:13

for S being IncStruct

for G, F being Subset of the Points of S st G c= F & F is planar holds

G is planar

for G, F being Subset of the Points of S st G c= F & F is planar holds

G is planar

proof end;

:: Introduction of mode IncSpace

definition

let S be IncProjStr ;

end;
attr S is with_non-trivial_lines means :Def8: :: INCSP_1:def 8

for L being LINE of S ex A, B being POINT of S st

( A <> B & {A,B} on L );

for L being LINE of S ex A, B being POINT of S st

( A <> B & {A,B} on L );

attr S is linear means :Def9: :: INCSP_1:def 9

for A, B being POINT of S ex L being LINE of S st {A,B} on L;

for A, B being POINT of S ex L being LINE of S st {A,B} on L;

:: 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 ) );

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 );

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 );

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 ;

end;
attr S is with_non-empty_planes means :Def11: :: INCSP_1:def 11

for P being PLANE of S ex A being POINT of S st A on P;

for P being PLANE of S ex A being POINT of S st A on P;

attr S is planar means :Def12: :: INCSP_1:def 12

for A, B, C being POINT of S ex P being PLANE of S st {A,B,C} on P;

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: :: INCSP_1:def 13

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;

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: :: INCSP_1:def 14

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;

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: :: INCSP_1:def 15

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 );

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: :: INCSP_1:def 16

not for A, B, C, D being POINT of S holds {A,B,C,D} is planar ;

not for A, B, C, D being POINT of S holds {A,B,C,D} is planar ;

attr S is inc-compatible means :Def17: :: INCSP_1:def 17

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;

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 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 );

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 );

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 );

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 );

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 ) );

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 );

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 );

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 );

definition

let IT be IncStruct ;

end;
attr IT is IncSpace-like means :Def18: :: INCSP_1:def 18

( 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 );

( 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 );

:: 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 ) );

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 ) );

registration

for b_{1} being IncStruct st b_{1} is IncSpace-like holds

( b_{1} is with_non-trivial_lines & b_{1} is linear & b_{1} is up-2-rank & b_{1} is with_non-empty_planes & b_{1} is planar & b_{1} is with_<=1_plane_per_3_pts & b_{1} is with_lines_inside_planes & b_{1} is with_planes_intersecting_in_2_pts & b_{1} is up-3-dimensional & b_{1} is inc-compatible )
by Def18;

end;

cluster IncSpace-like -> with_non-trivial_lines linear up-2-rank with_non-empty_planes planar with_<=1_plane_per_3_pts with_lines_inside_planes with_planes_intersecting_in_2_pts up-3-dimensional inc-compatible for IncStruct ;

coherence for b

( b

registration
end;

:: Axioms of Incidence

theorem Th14: :: INCSP_1:14

for S being IncSpace

for L being LINE of S

for P being PLANE of S

for F being Subset of the Points of S st F on L & L on P holds

F on P

for L being LINE of S

for P being PLANE of S

for F being Subset of the Points of S st F on L & L on P holds

F on P

proof end;

:: Collinearity of points & coplanarity of points & lines

theorem Th18: :: INCSP_1:18

for S being IncSpace

for A, B, C being POINT of S

for L being LINE of S st A <> B & {A,B} on L & not C on L holds

not {A,B,C} is linear

for A, B, C being POINT of S

for L being LINE of S st A <> B & {A,B} on L & not C on L holds

not {A,B,C} is linear

proof end;

theorem Th19: :: INCSP_1:19

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

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

proof end;

theorem :: INCSP_1:20

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

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

proof end;

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 )

proof end;

theorem :: INCSP_1:21

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

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

proof end;

theorem :: INCSP_1:22

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 )

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 )

proof end;

:: Lines & planes

theorem Th23: :: INCSP_1:23

for S being IncSpace

for K, L being LINE of S st ex A being POINT of S st

( A on K & A on L ) holds

ex P being PLANE of S st

( K on P & L on P )

for K, L being LINE of S st ex A being POINT of S st

( A on K & A on L ) holds

ex P being PLANE of S st

( K on P & L on P )

proof end;

theorem :: INCSP_1:24

for S being IncSpace

for A, B being POINT of S st A <> B holds

ex L being LINE of S st

for K being LINE of S holds

( {A,B} on K iff K = L )

for A, B being POINT of S st A <> B holds

ex L being LINE of S st

for K being LINE of S holds

( {A,B} on K iff K = L )

proof end;

theorem :: INCSP_1:25

for S being IncSpace

for A, B, C being POINT of S st not {A,B,C} is linear holds

ex P being PLANE of S st

for Q being PLANE of S holds

( {A,B,C} on Q iff P = Q )

for A, B, C being POINT of S st not {A,B,C} is linear holds

ex P being PLANE of S st

for Q being PLANE of S holds

( {A,B,C} on Q iff P = Q )

proof end;

theorem Th26: :: INCSP_1:26

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 )

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 )

proof end;

theorem Th27: :: INCSP_1:27

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 )

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 )

proof end;

:: Definitions of functions: Line, Plane

definition

let S be IncSpace;

let A, B be POINT of S;

assume A1: A <> B ;

correctness

existence

ex b_{1} being LINE of S st {A,B} on b_{1};

uniqueness

for b_{1}, b_{2} being LINE of S st {A,B} on b_{1} & {A,B} on b_{2} holds

b_{1} = b_{2};

by A1, Def9, Def10;

end;
let A, B be POINT of S;

assume A1: A <> B ;

correctness

existence

ex b

uniqueness

for b

b

by A1, Def9, Def10;

:: deftheorem Def19 defines Line INCSP_1:def 19 :

for S being IncSpace

for A, B being POINT of S st A <> B holds

for b_{4} being LINE of S holds

( b_{4} = Line (A,B) iff {A,B} on b_{4} );

for S being IncSpace

for A, B being POINT of S st A <> B holds

for b

( b

definition

let S be IncSpace;

let A, B, C be POINT of S;

assume A1: not {A,B,C} is linear ;

correctness

existence

ex b_{1} being PLANE of S st {A,B,C} on b_{1};

uniqueness

for b_{1}, b_{2} being PLANE of S st {A,B,C} on b_{1} & {A,B,C} on b_{2} holds

b_{1} = b_{2};

by A1, Def12, Def13;

end;
let A, B, C be POINT of S;

assume A1: not {A,B,C} is linear ;

correctness

existence

ex b

uniqueness

for b

b

by A1, Def12, Def13;

:: 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 b_{5} being PLANE of S holds

( b_{5} = Plane (A,B,C) iff {A,B,C} on b_{5} );

for S being IncSpace

for A, B, C being POINT of S st not {A,B,C} is linear holds

for b

( b

definition

let S be IncSpace;

let A be POINT of S;

let L be LINE of S;

assume A1: not A on L ;

existence

ex b_{1} being PLANE of S st

( A on b_{1} & L on b_{1} )

for b_{1}, b_{2} being PLANE of S st A on b_{1} & L on b_{1} & A on b_{2} & L on b_{2} holds

b_{1} = b_{2}

end;
let A be POINT of S;

let L be LINE of S;

assume A1: not A on L ;

existence

ex b

( A on b

proof end;

uniqueness for b

b

proof end;

:: 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 b_{4} being PLANE of S holds

( b_{4} = Plane (A,L) iff ( A on b_{4} & L on b_{4} ) );

for S being IncSpace

for A being POINT of S

for L being LINE of S st not A on L holds

for b

( b

definition

let S be IncSpace;

let K, L be LINE of S;

assume that

A1: K <> L and

A2: ex A being POINT of S st

( A on K & A on L ) ;

existence

ex b_{1} being PLANE of S st

( K on b_{1} & L on b_{1} )
by A2, Th23;

uniqueness

for b_{1}, b_{2} being PLANE of S st K on b_{1} & L on b_{1} & K on b_{2} & L on b_{2} holds

b_{1} = b_{2}

end;
let K, L be LINE of S;

assume that

A1: K <> L and

A2: ex A being POINT of S st

( A on K & A on L ) ;

existence

ex b

( K on b

uniqueness

for b

b

proof end;

:: 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 b_{4} being PLANE of S holds

( b_{4} = Plane (K,L) iff ( K on b_{4} & L on b_{4} ) );

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 b

( b

:: Definitional theorems of functions: Line, Plane

theorem Th29: :: INCSP_1:29

for S being IncSpace

for A, B, C being POINT of S st not {A,B,C} is linear holds

Plane (A,B,C) = Plane (A,C,B)

for A, B, C being POINT of S st not {A,B,C} is linear holds

Plane (A,B,C) = Plane (A,C,B)

proof end;

theorem Th30: :: INCSP_1:30

for S being IncSpace

for A, B, C being POINT of S st not {A,B,C} is linear holds

Plane (A,B,C) = Plane (B,A,C)

for A, B, C being POINT of S st not {A,B,C} is linear holds

Plane (A,B,C) = Plane (B,A,C)

proof end;

theorem :: INCSP_1:31

for S being IncSpace

for A, B, C being POINT of S st not {A,B,C} is linear holds

Plane (A,B,C) = Plane (B,C,A)

for A, B, C being POINT of S st not {A,B,C} is linear holds

Plane (A,B,C) = Plane (B,C,A)

proof end;

theorem Th32: :: INCSP_1:32

for S being IncSpace

for A, B, C being POINT of S st not {A,B,C} is linear holds

Plane (A,B,C) = Plane (C,A,B)

for A, B, C being POINT of S st not {A,B,C} is linear holds

Plane (A,B,C) = Plane (C,A,B)

proof end;

theorem :: INCSP_1:33

for S being IncSpace

for A, B, C being POINT of S st not {A,B,C} is linear holds

Plane (A,B,C) = Plane (C,B,A)

for A, B, C being POINT of S st not {A,B,C} is linear holds

Plane (A,B,C) = Plane (C,B,A)

proof end;

theorem :: INCSP_1:34

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

Plane (K,L) = Plane (L,K)

for K, L being LINE of S st K <> L & ex A being POINT of S st

( A on K & A on L ) holds

Plane (K,L) = Plane (L,K)

proof end;

theorem Th35: :: INCSP_1:35

for S being IncSpace

for A, B, C being POINT of S st A <> B & C on Line (A,B) holds

{A,B,C} is linear

for A, B, C being POINT of S st A <> B & C on Line (A,B) holds

{A,B,C} is linear

proof end;

theorem :: INCSP_1:36

for S being IncSpace

for A, B, C being POINT of S st A <> B & A <> C & {A,B,C} is linear holds

Line (A,B) = Line (A,C)

for A, B, C being POINT of S st A <> B & A <> C & {A,B,C} is linear holds

Line (A,B) = Line (A,C)

proof end;

theorem :: INCSP_1:37

for S being IncSpace

for A, B, C being POINT of S st not {A,B,C} is linear holds

Plane (A,B,C) = Plane (C,(Line (A,B)))

for A, B, C being POINT of S st not {A,B,C} is linear holds

Plane (A,B,C) = Plane (C,(Line (A,B)))

proof end;

theorem :: INCSP_1:38

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

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

proof end;

theorem :: INCSP_1:39

for S being IncSpace

for C, A, B being POINT of S

for L being LINE of S st not C on L & {A,B} on L & A <> B holds

Plane (C,L) = Plane (A,B,C)

for C, A, B being POINT of S

for L being LINE of S st not C on L & {A,B} on L & A <> B holds

Plane (C,L) = Plane (A,B,C)

proof end;

theorem :: INCSP_1:40

for S being IncSpace

for A, B, C being POINT of S st not {A,B,C} is linear holds

Plane (A,B,C) = Plane ((Line (A,B)),(Line (A,C)))

for A, B, C being POINT of S st not {A,B,C} is linear holds

Plane (A,B,C) = Plane ((Line (A,B)),(Line (A,C)))

proof end;

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 )

proof end;

:: The fourth axiom of incidence

theorem Th41: :: INCSP_1:41

for S being IncSpace

for P being PLANE of S ex A, B, C being POINT of S st

( {A,B,C} on P & not {A,B,C} is linear )

for P being PLANE of S ex A, B, C being POINT of S st

( {A,B,C} on P & not {A,B,C} is linear )

proof end;

:: Fundamental existence theorems

theorem :: INCSP_1:42

theorem :: INCSP_1:43

theorem Th44: :: INCSP_1:44

for S being IncSpace

for A, B being POINT of S

for P being PLANE of S st A <> B holds

ex C being POINT of S st

( C on P & not {A,B,C} is linear )

for A, B being POINT of S

for P being PLANE of S st A <> B holds

ex C being POINT of S st

( C on P & not {A,B,C} is linear )

proof end;

theorem Th45: :: INCSP_1:45

for S being IncSpace

for A, B, C being POINT of S st not {A,B,C} is linear holds

ex D being POINT of S st not {A,B,C,D} is planar

for A, B, C being POINT of S st not {A,B,C} is linear holds

ex D being POINT of S st not {A,B,C,D} is planar

proof end;

theorem Th46: :: INCSP_1:46

for S being IncSpace

for A being POINT of S

for P being PLANE of S ex B, C being POINT of S st

( {B,C} on P & not {A,B,C} is linear )

for A being POINT of S

for P being PLANE of S ex B, C being POINT of S st

( {B,C} on P & not {A,B,C} is linear )

proof end;

theorem Th47: :: INCSP_1:47

for S being IncSpace

for A, B being POINT of S st A <> B holds

ex C, D being POINT of S st not {A,B,C,D} is planar

for A, B being POINT of S st A <> B holds

ex C, D being POINT of S st not {A,B,C,D} is planar

proof end;

theorem :: INCSP_1:48

for S being IncSpace

for A being POINT of S holds

not for B, C, D being POINT of S holds {A,B,C,D} is planar

for A being POINT of S holds

not for B, C, D being POINT of S holds {A,B,C,D} is planar

proof end;

theorem :: INCSP_1:49

for S being IncSpace

for A being POINT of S

for P being PLANE of S ex L being LINE of S st

( not A on L & L on P )

for A being POINT of S

for P being PLANE of S ex L being LINE of S st

( not A on L & L on P )

proof end;

theorem Th50: :: INCSP_1:50

for S being IncSpace

for A being POINT of S

for P being PLANE of S st A on P holds

ex L, L1, L2 being LINE of S st

( L1 <> L2 & L1 on P & L2 on P & not L on P & A on L & A on L1 & A on L2 )

for A being POINT of S

for P being PLANE of S st A on P holds

ex L, L1, L2 being LINE of S st

( L1 <> L2 & L1 on P & L2 on P & not L on P & A on L & A on L1 & A on L2 )

proof end;

theorem :: INCSP_1:51

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 ) ) )

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 ) ) )

proof end;

theorem :: INCSP_1:52

for S being IncSpace

for A being POINT of S

for L being LINE of S ex P being PLANE of S st

( A on P & not L on P )

for A being POINT of S

for L being LINE of S ex P being PLANE of S st

( A on P & not L on P )

proof end;

theorem :: INCSP_1:53

for S being IncSpace

for L being LINE of S

for P being PLANE of S ex A being POINT of S st

( A on P & not A on L )

for L being LINE of S

for P being PLANE of S ex A being POINT of S st

( A on P & not A on L )

proof end;

theorem :: INCSP_1:54

for S being IncSpace

for L being LINE of S ex K being LINE of S st

for P being PLANE of S holds

( not L on P or not K on P )

for L being LINE of S ex K being LINE of S st

for P being PLANE of S holds

( not L on P or not K on P )

proof end;

:: Intersection of lines and planes

theorem :: INCSP_1:56

theorem :: INCSP_1:57

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 ) )

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 ) )

proof end;