:: Axioms of Incidence
:: by Wojciech A. Trybulec
::
:: Received April 14, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

definition
attrc1 is strict ;
struct IncProjStr  -> ;
aggrIncProjStr(# Points, Lines, Inc #) ->  IncProjStr ;
sel Points c1 ->  non empty set ;
sel Lines c1 ->  non empty set ;
sel Inc c1 ->  Relation of the Points of c1, the Lines of c1;
end;

definition
attrc1 is strict ;
struct IncStruct  ->  IncProjStr ;
aggrIncStruct(# Points, Lines, Planes, Inc, Inc2, Inc3 #) ->  IncStruct ;
sel Planes c1 ->  non empty set ;
sel Inc2 c1 ->  Relation of the Points of c1, the Planes of c1;
sel Inc3 c1 ->  Relation of the Lines of c1, the Planes of c1;
end;

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;

definition
let S be IncStruct ;
mode PLANE of S is Element of the Planes of S;
end;

:: Definitions of predicates: on, is_collinear, is_coplanar
definition
let S be IncProjStr ;
let A be POINT of S;
let L be LINE of S;
predA on L means :Def1: :: INCSP_1:def 1
[A,L] in the Inc of S;
end;

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

definition
let S be IncStruct ;
let A be POINT of S;
let P be PLANE of S;
predA on P means :Def2: :: INCSP_1:def 2
[A,P] in the Inc2 of S;
end;

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

definition
let S be IncStruct ;
let L be LINE of S;
let P be PLANE of S;
predL on P means :Def3: :: INCSP_1:def 3
[L,P] in the Inc3 of S;
end;

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

definition
let S be IncProjStr ;
let F be Subset of the Points of S;
let L be LINE of S;
predF on L means :Def4: :: INCSP_1:def 4
 for A being POINT of S st A in F holds
A on L;
end;

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

definition
let S be IncStruct ;
let F be Subset of the Points of S;
let P be PLANE of S;
predF on P means :Def5: :: INCSP_1:def 5
 for A being POINT of S st A in F holds
A on P;
end;

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

definition
let S be IncProjStr ;
let F be Subset of the Points of S;
attrF is linear  means :Def6: :: INCSP_1:def 6
 ex L being LINE of S st F on L;
end;

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

definition
let S be IncStruct ;
let F be Subset of the Points of S;
attrF is planar  means :Def7: :: INCSP_1:def 7
 ex P being PLANE of S st F on P;
end;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

:: Introduction of mode IncSpace
definition
let S be IncProjStr ;
attrS 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 &amp; {A,B} on L );
attrS 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;
attrS is up-2-rank  means :Def10: :: INCSP_1:def 10
 for A, B being POINT of S
for K, L being LINE of S st A <> B &amp; {A,B} on K &amp; {A,B} on L holds
K = L;
end;

:: 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 &amp; {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 &amp; {A,B} on K &amp; {A,B} on L holds
K = L );

definition
let S be IncStruct ;
attrS 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;
attrS 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;
attrS 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 &amp; {A,B,C} on P &amp; {A,B,C} on Q holds
P = Q;
attrS 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 &amp; {A,B} on L &amp; {A,B} on P ) holds
L on P;
attrS 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 &amp; A on Q holds
ex B being POINT of S st
( A <> B &amp; B on P &amp; B on Q );
attrS 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 ;
attrS 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 &amp; 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 &amp; {A,B,C} on P &amp; {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 &amp; {A,B} on L &amp; {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 &amp; A on Q holds
ex B being POINT of S st
( A <> B &amp; B on P &amp; 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 &amp; L on P holds
A on P );

definition
let IT be IncStruct ;
attrIT is IncSpace-like  means :Def18: :: INCSP_1:def 18
( IT is with_non-trivial_lines &amp; IT is linear &amp; IT is up-2-rank &amp; IT is with_non-empty_planes &amp; IT is planar &amp; IT is with_<=1_plane_per_3_pts &amp; IT is with_lines_inside_planes &amp; IT is with_planes_intersecting_in_2_pts &amp; IT is up-3-dimensional &amp; IT is inc-compatible );
end;

:: 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 &amp; IT is linear &amp; IT is up-2-rank &amp; IT is with_non-empty_planes &amp; IT is planar &amp; IT is with_<=1_plane_per_3_pts &amp; IT is with_lines_inside_planes &amp; IT is with_planes_intersecting_in_2_pts &amp; IT is up-3-dimensional &amp; IT is inc-compatible ) );

registration
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 b1 being IncStruct st b1 is IncSpace-like holds
( b1 is with_non-trivial_lines &amp; b1 is linear &amp; b1 is up-2-rank &amp; b1 is with_non-empty_planes &amp; b1 is planar &amp; b1 is with_<=1_plane_per_3_pts &amp; b1 is with_lines_inside_planes &amp; b1 is with_planes_intersecting_in_2_pts &amp; b1 is up-3-dimensional &amp; b1 is inc-compatible ) by Def18;
end;

registration
cluster strict IncSpace-like for IncStruct ;
existence
 ex b1 being IncStruct st
( b1 is strict &amp; b1 is IncSpace-like )
proofend;
end;

definition
mode IncSpace is IncSpace-like IncStruct ;
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 &amp; L on P holds
F on P
proofend;

:: Collinearity of points &amp; coplanarity of points &amp; lines
theorem Th15: :: INCSP_1:15
for S being IncSpace
for A, B being POINT of S holds {A,A,B} is linear
proofend;

theorem Th16: :: INCSP_1:16
for S being IncSpace
for A, B, C being POINT of S holds {A,A,B,C} is planar
proofend;

theorem Th17: :: INCSP_1:17
for S being IncSpace
for A, B, C, D being POINT of S st {A,B,C} is linear holds
{A,B,C,D} is planar
proofend;

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 &amp; {A,B} on L &amp; not C on L holds
not {A,B,C} is linear
proofend;

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 &amp; {A,B,C} on P &amp; not D on P holds
not {A,B,C,D} is planar
proofend;

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

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 &amp; B on L )
proofend;

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 ) ) &amp; ex A being POINT of S st
( A on L &amp; A on L1 &amp; A on L2 ) holds
L <> L1
proofend;

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 &amp; L2 on P &amp; not L on P &amp; L1 <> L2 holds
for Q being PLANE of S holds
( not L on Q or not L1 on Q or not L2 on Q )
proofend;

:: Lines &amp; 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 &amp; A on L ) holds
ex P being PLANE of S st
( K on P &amp; L on P )
proofend;

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

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

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 &amp; L on Q ) iff P = Q )
proofend;

theorem Th27: :: INCSP_1:27
for S being IncSpace
for K, L being LINE of S st K <> L &amp; ex A being POINT of S st
( A on K &amp; A on L ) holds
ex P being PLANE of S st
for Q being PLANE of S holds
( ( K on Q &amp; L on Q ) iff P = Q )
proofend;

:: Definitions of functions: Line, Plane
definition
let S be IncSpace;
let A, B be POINT of S;
assume A1: A <> B ;
func Line (A,B) ->  LINE of S means :Def19: :: INCSP_1:def 19
{A,B} on it;
correctness
existence
ex b1 being LINE of S st {A,B} on b1;
uniqueness
for b1, b2 being LINE of S st {A,B} on b1 &amp; {A,B} on b2 holds
b1 = b2;
by A1, Def9, Def10;
end;

:: 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: :: INCSP_1:def 20
{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 &amp; {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 );

definition
let S be IncSpace;
let A be POINT of S;
let L be LINE of S;
assume A1: not A on L ;
func Plane (A,L) ->  PLANE of S means :Def21: :: INCSP_1:def 21
( A on it &amp; L on it );
existence
 ex b1 being PLANE of S st
( A on b1 &amp; L on b1 )
proofend;
uniqueness
 for b1, b2 being PLANE of S st A on b1 &amp; L on b1 &amp; A on b2 &amp; L on b2 holds
b1 = b2
proofend;
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 b4 being PLANE of S holds
( b4 = Plane (A,L) iff ( A on b4 &amp; L on b4 ) );

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 &amp; A on L ) ;
func Plane (K,L) ->  PLANE of S means :Def22: :: INCSP_1:def 22
( K on it &amp; L on it );
existence
 ex b1 being PLANE of S st
( K on b1 &amp; L on b1 ) by A2, Th23;
uniqueness
 for b1, b2 being PLANE of S st K on b1 &amp; L on b1 &amp; K on b2 &amp; L on b2 holds
b1 = b2
proofend;
end;

:: deftheorem Def22 defines Plane INCSP_1:def_22_:_
 for S being IncSpace
for K, L being LINE of S st K <> L &amp; ex A being POINT of S st
( A on K &amp; A on L ) holds
for b4 being PLANE of S holds
( b4 = Plane (K,L) iff ( K on b4 &amp; L on b4 ) );

:: Definitional theorems of functions: Line, Plane
theorem :: INCSP_1:28
for S being IncSpace
for A, B being POINT of S st A <> B holds
Line (A,B) = Line (B,A)
proofend;

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

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

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

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

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

theorem :: INCSP_1:34
for S being IncSpace
for K, L being LINE of S st K <> L &amp; ex A being POINT of S st
( A on K &amp; A on L ) holds
Plane (K,L) = Plane (L,K)
proofend;

theorem Th35: :: INCSP_1:35
for S being IncSpace
for A, B, C being POINT of S st A <> B &amp; C on Line (A,B) holds
{A,B,C} is linear
proofend;

theorem :: INCSP_1:36
for S being IncSpace
for A, B, C being POINT of S st A <> B &amp; A <> C &amp; {A,B,C} is linear holds
Line (A,B) = Line (A,C)
proofend;

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

theorem :: INCSP_1:38
for S being IncSpace
for A, B, C, D being POINT of S st not {A,B,C} is linear &amp; D on Plane (A,B,C) holds
{A,B,C,D} is planar
proofend;

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 &amp; {A,B} on L &amp; A <> B holds
Plane (C,L) = Plane (A,B,C)
proofend;

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

Lm2:  for S being IncSpace
for P being PLANE of S ex A, B, C, D being POINT of S st
( A on P &amp; not {A,B,C,D} is planar )
proofend;

:: 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 &amp; not {A,B,C} is linear )
proofend;

:: Fundamental existence theorems
theorem :: INCSP_1:42
for S being IncSpace
for P being PLANE of S ex A, B, C, D being POINT of S st
( A on P &amp; not {A,B,C,D} is planar ) by Lm2;

theorem :: INCSP_1:43
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 &amp; B on L ) by Lm1;

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 &amp; not {A,B,C} is linear )
proofend;

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

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 &amp; not {A,B,C} is linear )
proofend;

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

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

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 &amp; L on P )
proofend;

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 &amp; L1 on P &amp; L2 on P &amp; not L on P &amp; A on L &amp; A on L1 &amp; A on L2 )
proofend;

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 &amp; A on L1 &amp; A on L2 &amp; ( for P being PLANE of S holds
( not L on P or not L1 on P or not L2 on P ) ) )
proofend;

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 &amp; not L on P )
proofend;

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 &amp; not A on L )
proofend;

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

theorem :: INCSP_1:55
for S being IncSpace
for L being LINE of S ex P, Q being PLANE of S st
( P <> Q &amp; L on P &amp; L on Q )
proofend;

:: Intersection of lines and planes
theorem :: INCSP_1:56
for S being IncSpace
for A, B being POINT of S
for L being LINE of S
for P being PLANE of S st not L on P &amp; {A,B} on L &amp; {A,B} on P holds
A = B by Def14;

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 &amp; B on Q ) iff B on L ) )
proofend;