:: INCSP_1 semantic presentation

definition

attr a₁ is strict;
struct IncProjStr -> ;
aggr IncProjStr(# Points, Lines, Inc #) -> IncProjStr ;
sel Points c₁ -> non empty set ;
sel Lines c₁ -> non empty set ;
sel Inc c₁ -> Relation of the Points of a₁,the Lines of a₁;

end;

definition

attr a₁ is strict;
struct IncStruct -> IncProjStr ;
aggr IncStruct(# Points, Lines, Planes, Inc, Inc2, Inc3 #) -> IncStruct ;
sel Planes c₁ -> non empty set ;
sel Inc2 c₁ -> Relation of the Points of a₁,the Planes of a₁;
sel Inc3 c₁ -> Relation of the Lines of a₁,the Planes of a₁;

end;

definition

let c₁ be IncProjStr ;
mode POINT of a₁ is Element of the Points of a₁;
mode LINE of a₁ is Element of the Lines of a₁;

end;

definition

let c₁ be IncStruct ;
mode PLANE of a₁ is Element of the Planes of a₁;

end;

definition

let c₁ be IncProjStr ;
let c₂ be POINT of c₁;
let c₃ be LINE of c₁;
pred c₂ on c₃ means :Def1: :: INCSP_1:def 1
[a₂,a₃] in the Inc of a₁;

end;

:: deftheorem Def1 defines on INCSP_1:def 1 :

definition

let c₁ be IncStruct ;
let c₂ be POINT of c₁;
let c₃ be PLANE of c₁;
pred c₂ on c₃ means :Def2: :: INCSP_1:def 2
[a₂,a₃] in the Inc2 of a₁;

end;

:: deftheorem Def2 defines on INCSP_1:def 2 :

definition

let c₁ be IncStruct ;
let c₂ be LINE of c₁;
let c₃ be PLANE of c₁;
pred c₂ on c₃ means :Def3: :: INCSP_1:def 3
[a₂,a₃] in the Inc3 of a₁;

end;

:: deftheorem Def3 defines on INCSP_1:def 3 :

definition

let c₁ be IncProjStr ;
let c₂ be Subset of the Points of c₁;
let c₃ be LINE of c₁;
pred c₂ on c₃ means :Def4: :: INCSP_1:def 4
for b₁ being POINT of a₁ st b₁ in a₂ holds
b₁ on a₃;

end;

:: deftheorem Def4 defines on INCSP_1:def 4 :

definition

let c₁ be IncStruct ;
let c₂ be Subset of the Points of c₁;
let c₃ be PLANE of c₁;
pred c₂ on c₃ means :Def5: :: INCSP_1:def 5
for b₁ being POINT of a₁ st b₁ in a₂ holds
b₁ on a₃;

end;

:: deftheorem Def5 defines on INCSP_1:def 5 :

definition

let c₁ be IncProjStr ;
let c₂ be Subset of the Points of c₁;
attr a₂ is linear means :Def6: :: INCSP_1:def 6
ex b₁ being LINE of a₁ st a₂ on b₁;

end;

:: deftheorem Def6 defines linear INCSP_1:def 6 :

notation

let c₁ be IncProjStr ;
let c₂ be Subset of the Points of c₁;
synonym c₂ is_collinear for linear c₂;

end;

definition

let c₁ be IncStruct ;
let c₂ be Subset of the Points of c₁;
attr a₂ is planar means :Def7: :: INCSP_1:def 7
ex b₁ being PLANE of a₁ st a₂ on b₁;

end;

:: deftheorem Def7 defines planar INCSP_1:def 7 :

notation

let c₁ be IncStruct ;
let c₂ be Subset of the Points of c₁;
synonym c₂ is_coplanar for planar c₂;

end;

theorem Th1: :: INCSP_1:1

canceled;

theorem Th2: :: INCSP_1:2

canceled;

theorem Th3: :: INCSP_1:3

canceled;

theorem Th4: :: INCSP_1:4

canceled;

theorem Th5: :: INCSP_1:5

canceled;

theorem Th6: :: INCSP_1:6

canceled;

theorem Th7: :: INCSP_1:7

canceled;

theorem Th8: :: INCSP_1:8

canceled;

theorem Th9: :: INCSP_1:9

canceled;

theorem Th10: :: INCSP_1:10

canceled;

theorem Th11: :: INCSP_1:11

for b₁ being IncStruct
for b₂, b₃ being POINT of b₁
for b₄ being LINE of b₁ holds
( {b₂,b₃} on b₄ iff ( b₂ on b₄ & b₃ on b₄ ) )

proof end;

theorem Th12: :: INCSP_1:12

for b₁ being IncStruct
for b₂, b₃, b₄ being POINT of b₁
for b₅ being LINE of b₁ holds
( {b₂,b₃,b₄} on b₅ iff ( b₂ on b₅ & b₃ on b₅ & b₄ on b₅ ) )

proof end;

theorem Th13: :: INCSP_1:13

for b₁ being IncStruct
for b₂, b₃ being POINT of b₁
for b₄ being PLANE of b₁ holds
( {b₂,b₃} on b₄ iff ( b₂ on b₄ & b₃ on b₄ ) )

proof end;

theorem Th14: :: INCSP_1:14

for b₁ being IncStruct
for b₂, b₃, b₄ being POINT of b₁
for b₅ being PLANE of b₁ holds
( {b₂,b₃,b₄} on b₅ iff ( b₂ on b₅ & b₃ on b₅ & b₄ on b₅ ) )

proof end;

theorem Th15: :: INCSP_1:15

for b₁ being IncStruct
for b₂, b₃, b₄, b₅ being POINT of b₁
for b₆ being PLANE of b₁ holds
( {b₂,b₃,b₄,b₅} on b₆ iff ( b₂ on b₆ & b₃ on b₆ & b₄ on b₆ & b₅ on b₆ ) )

proof end;

theorem Th16: :: INCSP_1:16

for b₁ being IncStruct
for b₂ being LINE of b₁
for b₃, b₄ being Subset of the Points of b₁ st b₃ c= b₄ & b₄ on b₂ holds
b₃ on b₂

proof end;

theorem Th17: :: INCSP_1:17

for b₁ being IncStruct
for b₂ being PLANE of b₁
for b₃, b₄ being Subset of the Points of b₁ st b₃ c= b₄ & b₄ on b₂ holds
b₃ on b₂

proof end;

theorem Th18: :: INCSP_1:18

for b₁ being IncStruct
for b₂ being POINT of b₁
for b₃ being LINE of b₁
for b₄ being Subset of the Points of b₁ holds
( ( b₄ on b₃ & b₂ on b₃ ) iff b₄ \/ {b₂} on b₃ )

proof end;

theorem Th19: :: INCSP_1:19

for b₁ being IncStruct
for b₂ being POINT of b₁
for b₃ being PLANE of b₁
for b₄ being Subset of the Points of b₁ holds
( ( b₄ on b₃ & b₂ on b₃ ) iff b₄ \/ {b₂} on b₃ )

proof end;

theorem Th20: :: INCSP_1:20

for b₁ being IncStruct
for b₂ being LINE of b₁
for b₃, b₄ being Subset of the Points of b₁ holds
( b₃ \/ b₄ on b₂ iff ( b₃ on b₂ & b₄ on b₂ ) )

proof end;

theorem Th21: :: INCSP_1:21

for b₁ being IncStruct
for b₂ being PLANE of b₁
for b₃, b₄ being Subset of the Points of b₁ holds
( b₃ \/ b₄ on b₂ iff ( b₃ on b₂ & b₄ on b₂ ) )

proof end;

theorem Th22: :: INCSP_1:22

for b₁ being IncStruct
for b₂, b₃ being Subset of the Points of b₁ st b₂ c= b₃ & b₃ is_collinear holds
b₂ is_collinear

proof end;

theorem Th23: :: INCSP_1:23

for b₁ being IncStruct
for b₂, b₃ being Subset of the Points of b₁ st b₂ c= b₃ & b₃ is_coplanar holds
b₂ is_coplanar

proof end;

registration

let c₁, c₂, c₃, c₄ be set ;
cluster {a₁,a₂,a₃,a₄} -> non empty ;
coherence by ENUMSET1:def 2;

end;

definition

let c₁ be IncStruct ;
attr a₁ is IncSpace-like means :Def8: :: INCSP_1:def 8
( ( for b₁ being LINE of a₁ ex b₂, b₃ being POINT of a₁ st
( b₂ <> b₃ & {b₂,b₃} on b₁ ) ) & ( for b₁, b₂ being POINT of a₁ ex b₃ being LINE of a₁ st {b₁,b₂} on b₃ ) & ( for b₁, b₂ being POINT of a₁
for b₃, b₄ being LINE of a₁ st b₁ <> b₂ & {b₁,b₂} on b₃ & {b₁,b₂} on b₄ holds
b₃ = b₄ ) & ( for b₁ being PLANE of a₁ ex b₂ being POINT of a₁ st b₂ on b₁ ) & ( for b₁, b₂, b₃ being POINT of a₁ ex b₄ being PLANE of a₁ st {b₁,b₂,b₃} on b₄ ) & ( for b₁, b₂, b₃ being POINT of a₁
for b₄, b₅ being PLANE of a₁ st not {b₁,b₂,b₃} is_collinear & {b₁,b₂,b₃} on b₄ & {b₁,b₂,b₃} on b₅ holds
b₄ = b₅ ) & ( for b₁ being LINE of a₁
for b₂ being PLANE of a₁ st ex b₃, b₄ being POINT of a₁ st
( b₃ <> b₄ & {b₃,b₄} on b₁ & {b₃,b₄} on b₂ ) holds
b₁ on b₂ ) & ( for b₁ being POINT of a₁
for b₂, b₃ being PLANE of a₁ st b₁ on b₂ & b₁ on b₃ holds
ex b₄ being POINT of a₁ st
( b₁ <> b₄ & b₄ on b₂ & b₄ on b₃ ) ) & not for b₁, b₂, b₃, b₄ being POINT of a₁ holds {b₁,b₂,b₃,b₄} is_coplanar & ( for b₁ being POINT of a₁
for b₂ being LINE of a₁
for b₃ being PLANE of a₁ st b₁ on b₂ & b₂ on b₃ holds
b₁ on b₃ ) );

end;

:: deftheorem Def8 defines IncSpace-like INCSP_1:def 8 :

registration

cluster strict IncSpace-like IncStruct ;
existence

proof end;

end;

definition

mode IncSpace is IncSpace-like IncStruct ;

end;

theorem Th24: :: INCSP_1:24

canceled;

theorem Th25: :: INCSP_1:25

canceled;

theorem Th26: :: INCSP_1:26

canceled;

theorem Th27: :: INCSP_1:27

canceled;

theorem Th28: :: INCSP_1:28

canceled;

theorem Th29: :: INCSP_1:29

canceled;

theorem Th30: :: INCSP_1:30

canceled;

theorem Th31: :: INCSP_1:31

canceled;

theorem Th32: :: INCSP_1:32

canceled;

theorem Th33: :: INCSP_1:33

canceled;

theorem Th34: :: INCSP_1:34

canceled;

theorem Th35: :: INCSP_1:35

for b₁ being IncSpace
for b₂ being LINE of b₁
for b₃ being PLANE of b₁
for b₄ being Subset of the Points of b₁ st b₄ on b₂ & b₂ on b₃ holds
b₄ on b₃

proof end;

theorem Th36: :: INCSP_1:36

for b₁ being IncSpace
for b₂, b₃ being POINT of b₁ holds {b₂,b₂,b₃} is_collinear

proof end;

theorem Th37: :: INCSP_1:37

for b₁ being IncSpace
for b₂, b₃, b₄ being POINT of b₁ holds {b₂,b₂,b₃,b₄} is_coplanar

proof end;

theorem Th38: :: INCSP_1:38

for b₁ being IncSpace
for b₂, b₃, b₄, b₅ being POINT of b₁ st {b₂,b₃,b₄} is_collinear holds
{b₂,b₃,b₄,b₅} is_coplanar

proof end;

theorem Th39: :: INCSP_1:39

for b₁ being IncSpace
for b₂, b₃, b₄ being POINT of b₁
for b₅ being LINE of b₁ st b₂ <> b₃ & {b₂,b₃} on b₅ & not b₄ on b₅ holds
not {b₂,b₃,b₄} is_collinear

proof end;

theorem Th40: :: INCSP_1:40

for b₁ being IncSpace
for b₂, b₃, b₄, b₅ being POINT of b₁
for b₆ being PLANE of b₁ st not {b₂,b₃,b₄} is_collinear & {b₂,b₃,b₄} on b₆ & not b₅ on b₆ holds
not {b₂,b₃,b₄,b₅} is_coplanar

proof end;

theorem Th41: :: INCSP_1:41

for b₁ being IncSpace
for b₂, b₃ being LINE of b₁ st ( for b₄ being PLANE of b₁ holds
( not b₂ on b₄ or not b₃ on b₄ ) ) holds
b₂ <> b₃

proof end;

Lemma26: for b₁ being IncSpace
for b₂ being POINT of b₁
for b₃ being LINE of b₁ ex b₄ being POINT of b₁ st
( b₂ <> b₄ & b₄ on b₃ )

proof end;

theorem Th42: :: INCSP_1:42

for b₁ being IncSpace
for b₂, b₃, b₄ being LINE of b₁ st ( for b₅ being PLANE of b₁ holds
( not b₂ on b₅ or not b₃ on b₅ or not b₄ on b₅ ) ) & ex b₅ being POINT of b₁ st
( b₅ on b₂ & b₅ on b₃ & b₅ on b₄ ) holds
b₂ <> b₃

proof end;

theorem Th43: :: INCSP_1:43

for b₁ being IncSpace
for b₂, b₃, b₄ being LINE of b₁
for b₅ being PLANE of b₁ st b₂ on b₅ & b₃ on b₅ & not b₄ on b₅ & b₂ <> b₃ holds
for b₆ being PLANE of b₁ holds
( not b₄ on b₆ or not b₂ on b₆ or not b₃ on b₆ )

proof end;

theorem Th44: :: INCSP_1:44

for b₁ being IncSpace
for b₂ being POINT of b₁
for b₃ being LINE of b₁ ex b₄ being PLANE of b₁ st
( b₂ on b₄ & b₃ on b₄ )

proof end;

theorem Th45: :: INCSP_1:45

for b₁ being IncSpace
for b₂, b₃ being LINE of b₁ st ex b₄ being POINT of b₁ st
( b₄ on b₂ & b₄ on b₃ ) holds
ex b₄ being PLANE of b₁ st
( b₂ on b₄ & b₃ on b₄ )

proof end;

theorem Th46: :: INCSP_1:46

for b₁ being IncSpace
for b₂, b₃ being POINT of b₁ st b₂ <> b₃ holds
ex b₄ being LINE of b₁ st
for b₅ being LINE of b₁ holds
( {b₂,b₃} on b₅ iff b₅ = b₄ )

proof end;

theorem Th47: :: INCSP_1:47

for b₁ being IncSpace
for b₂, b₃, b₄ being POINT of b₁ st not {b₂,b₃,b₄} is_collinear holds
ex b₅ being PLANE of b₁ st
for b₆ being PLANE of b₁ holds
( {b₂,b₃,b₄} on b₆ iff b₅ = b₆ )

proof end;

theorem Th48: :: INCSP_1:48

for b₁ being IncSpace
for b₂ being POINT of b₁
for b₃ being LINE of b₁ st not b₂ on b₃ holds
ex b₄ being PLANE of b₁ st
for b₅ being PLANE of b₁ holds
( ( b₂ on b₅ & b₃ on b₅ ) iff b₄ = b₅ )

proof end;

theorem Th49: :: INCSP_1:49

for b₁ being IncSpace
for b₂, b₃ being LINE of b₁ st b₂ <> b₃ & ex b₄ being POINT of b₁ st
( b₄ on b₂ & b₄ on b₃ ) holds
ex b₄ being PLANE of b₁ st
for b₅ being PLANE of b₁ holds
( ( b₂ on b₅ & b₃ on b₅ ) iff b₄ = b₅ )

proof end;

definition

let c₁ be IncSpace;
let c₂, c₃ be POINT of c₁;
assume E31: c₂ <> c₃ ;
func Line c₂,c₃ -> LINE of a₁ means :Def9: :: INCSP_1:def 9
{a₂,a₃} on a₄;
correctness by E31, Def8;

end;

:: deftheorem Def9 defines Line INCSP_1:def 9 :

definition

let c₁ be IncSpace;
let c₂, c₃, c₄ be POINT of c₁;
assume E32: not {c₂,c₃,c₄} is_collinear ;
func Plane c₂,c₃,c₄ -> PLANE of a₁ means :Def10: :: INCSP_1:def 10
{a₂,a₃,a₄} on a₅;
correctness by E32, Def8;

end;

:: deftheorem Def10 defines Plane INCSP_1:def 10 :

definition

let c₁ be IncSpace;
let c₂ be POINT of c₁;
let c₃ be LINE of c₁;
assume E33: not c₂ on c₃ ;
func Plane c₂,c₃ -> PLANE of a₁ means :Def11: :: INCSP_1:def 11
( a₂ on a₄ & a₃ on a₄ );
existence by Th44;
uniqueness

proof end;

end;

:: deftheorem Def11 defines Plane INCSP_1:def 11 :

definition

let c₁ be IncSpace;
let c₂, c₃ be LINE of c₁;
assume that
E34: c₂ <> c₃ and
E35: ex b₁ being POINT of c₁ st
( b₁ on c₂ & b₁ on c₃ ) ;
func Plane c₂,c₃ -> PLANE of a₁ means :Def12: :: INCSP_1:def 12
( a₂ on a₄ & a₃ on a₄ );
existence by E35, Th45;
uniqueness

proof end;

end;

:: deftheorem Def12 defines Plane INCSP_1:def 12 :

theorem Th50: :: INCSP_1:50

canceled;

theorem Th51: :: INCSP_1:51

canceled;

theorem Th52: :: INCSP_1:52

canceled;

theorem Th53: :: INCSP_1:53

canceled;

theorem Th54: :: INCSP_1:54

canceled;

theorem Th55: :: INCSP_1:55

canceled;

theorem Th56: :: INCSP_1:56

canceled;

theorem Th57: :: INCSP_1:57

for b₁ being IncSpace
for b₂, b₃ being POINT of b₁ st b₂ <> b₃ holds
Line b₂,b₃ = Line b₃,b₂

proof end;

theorem Th58: :: INCSP_1:58

for b₁ being IncSpace
for b₂, b₃, b₄ being POINT of b₁ st not {b₂,b₃,b₄} is_collinear holds
Plane b₂,b₃,b₄ = Plane b₂,b₄,b₃

proof end;

theorem Th59: :: INCSP_1:59

for b₁ being IncSpace
for b₂, b₃, b₄ being POINT of b₁ st not {b₂,b₃,b₄} is_collinear holds
Plane b₂,b₃,b₄ = Plane b₃,b₂,b₄

proof end;

theorem Th60: :: INCSP_1:60

for b₁ being IncSpace
for b₂, b₃, b₄ being POINT of b₁ st not {b₂,b₃,b₄} is_collinear holds
Plane b₂,b₃,b₄ = Plane b₃,b₄,b₂

proof end;

theorem Th61: :: INCSP_1:61

for b₁ being IncSpace
for b₂, b₃, b₄ being POINT of b₁ st not {b₂,b₃,b₄} is_collinear holds
Plane b₂,b₃,b₄ = Plane b₄,b₂,b₃

proof end;

theorem Th62: :: INCSP_1:62

for b₁ being IncSpace
for b₂, b₃, b₄ being POINT of b₁ st not {b₂,b₃,b₄} is_collinear holds
Plane b₂,b₃,b₄ = Plane b₄,b₃,b₂

proof end;

theorem Th63: :: INCSP_1:63

canceled;

theorem Th64: :: INCSP_1:64

for b₁ being IncSpace
for b₂, b₃ being LINE of b₁ st b₂ <> b₃ & ex b₄ being POINT of b₁ st
( b₄ on b₂ & b₄ on b₃ ) holds
Plane b₂,b₃ = Plane b₃,b₂

proof end;

theorem Th65: :: INCSP_1:65

for b₁ being IncSpace
for b₂, b₃, b₄ being POINT of b₁ st b₂ <> b₃ & b₄ on Line b₂,b₃ holds
{b₂,b₃,b₄} is_collinear

proof end;

theorem Th66: :: INCSP_1:66

for b₁ being IncSpace
for b₂, b₃, b₄ being POINT of b₁ st b₂ <> b₃ & b₂ <> b₄ & {b₂,b₃,b₄} is_collinear holds
Line b₂,b₃ = Line b₂,b₄

proof end;

theorem Th67: :: INCSP_1:67

for b₁ being IncSpace
for b₂, b₃, b₄ being POINT of b₁ st not {b₂,b₃,b₄} is_collinear holds
Plane b₂,b₃,b₄ = Plane b₄,(Line b₂,b₃)

proof end;

theorem Th68: :: INCSP_1:68

for b₁ being IncSpace
for b₂, b₃, b₄, b₅ being POINT of b₁ st not {b₂,b₃,b₄} is_collinear & b₅ on Plane b₂,b₃,b₄ holds
{b₂,b₃,b₄,b₅} is_coplanar

proof end;

theorem Th69: :: INCSP_1:69

for b₁ being IncSpace
for b₂, b₃, b₄ being POINT of b₁
for b₅ being LINE of b₁ st not b₂ on b₅ & {b₃,b₄} on b₅ & b₃ <> b₄ holds
Plane b₂,b₅ = Plane b₃,b₄,b₂

proof end;

theorem Th70: :: INCSP_1:70

for b₁ being IncSpace
for b₂, b₃, b₄ being POINT of b₁ st not {b₂,b₃,b₄} is_collinear holds
Plane b₂,b₃,b₄ = Plane (Line b₂,b₃),(Line b₂,b₄)

proof end;

Lemma39: for b₁ being IncSpace
for b₂ being PLANE of b₁ ex b₃, b₄, b₅, b₆ being POINT of b₁ st
( b₃ on b₂ & not {b₃,b₄,b₅,b₆} is_coplanar )

proof end;

theorem Th71: :: INCSP_1:71

for b₁ being IncSpace
for b₂ being PLANE of b₁ ex b₃, b₄, b₅ being POINT of b₁ st
( {b₃,b₄,b₅} on b₂ & not {b₃,b₄,b₅} is_collinear )

proof end;

theorem Th72: :: INCSP_1:72

for b₁ being IncSpace
for b₂ being PLANE of b₁ ex b₃, b₄, b₅, b₆ being POINT of b₁ st
( b₃ on b₂ & not {b₃,b₄,b₅,b₆} is_coplanar ) by Lemma39;

theorem Th73: :: INCSP_1:73

for b₁ being IncSpace
for b₂ being POINT of b₁
for b₃ being LINE of b₁ ex b₄ being POINT of b₁ st
( b₂ <> b₄ & b₄ on b₃ ) by Lemma26;

theorem Th74: :: INCSP_1:74

for b₁ being IncSpace
for b₂, b₃ being POINT of b₁
for b₄ being PLANE of b₁ st b₂ <> b₃ holds
ex b₅ being POINT of b₁ st
( b₅ on b₄ & not {b₂,b₃,b₅} is_collinear )

proof end;

theorem Th75: :: INCSP_1:75

for b₁ being IncSpace
for b₂, b₃, b₄ being POINT of b₁ st not {b₂,b₃,b₄} is_collinear holds
ex b₅ being POINT of b₁ st not {b₂,b₃,b₄,b₅} is_coplanar

proof end;

theorem Th76: :: INCSP_1:76

for b₁ being IncSpace
for b₂ being POINT of b₁
for b₃ being PLANE of b₁ ex b₄, b₅ being POINT of b₁ st
( {b₄,b₅} on b₃ & not {b₂,b₄,b₅} is_collinear )

proof end;

theorem Th77: :: INCSP_1:77

for b₁ being IncSpace
for b₂, b₃ being POINT of b₁ st b₂ <> b₃ holds
ex b₄, b₅ being POINT of b₁ st not {b₂,b₃,b₄,b₅} is_coplanar

proof end;

theorem Th78: :: INCSP_1:78

for b₁ being IncSpace
for b₂ being POINT of b₁ holds
not for b₃, b₄, b₅ being POINT of b₁ holds {b₂,b₃,b₄,b₅} is_coplanar

proof end;

theorem Th79: :: INCSP_1:79

for b₁ being IncSpace
for b₂ being POINT of b₁
for b₃ being PLANE of b₁ ex b₄ being LINE of b₁ st
( not b₂ on b₄ & b₄ on b₃ )

proof end;

theorem Th80: :: INCSP_1:80

for b₁ being IncSpace
for b₂ being POINT of b₁
for b₃ being PLANE of b₁ st b₂ on b₃ holds
ex b₄, b₅, b₆ being LINE of b₁ st
( b₅ <> b₆ & b₅ on b₃ & b₆ on b₃ & not b₄ on b₃ & b₂ on b₄ & b₂ on b₅ & b₂ on b₆ )

proof end;

theorem Th81: :: INCSP_1:81

for b₁ being IncSpace
for b₂ being POINT of b₁ ex b₃, b₄, b₅ being LINE of b₁ st
( b₂ on b₃ & b₂ on b₄ & b₂ on b₅ & ( for b₆ being PLANE of b₁ holds
( not b₃ on b₆ or not b₄ on b₆ or not b₅ on b₆ ) ) )

proof end;

theorem Th82: :: INCSP_1:82

for b₁ being IncSpace
for b₂ being POINT of b₁
for b₃ being LINE of b₁ ex b₄ being PLANE of b₁ st
( b₂ on b₄ & not b₃ on b₄ )

proof end;

theorem Th83: :: INCSP_1:83

for b₁ being IncSpace
for b₂ being LINE of b₁
for b₃ being PLANE of b₁ ex b₄ being POINT of b₁ st
( b₄ on b₃ & not b₄ on b₂ )

proof end;

theorem Th84: :: INCSP_1:84

for b₁ being IncSpace
for b₂ being LINE of b₁ ex b₃ being LINE of b₁ st
for b₄ being PLANE of b₁ holds
( not b₂ on b₄ or not b₃ on b₄ )

proof end;

theorem Th85: :: INCSP_1:85

for b₁ being IncSpace
for b₂ being LINE of b₁ ex b₃, b₄ being PLANE of b₁ st
( b₃ <> b₄ & b₂ on b₃ & b₂ on b₄ )

proof end;

theorem Th86: :: INCSP_1:86

canceled;

theorem Th87: :: INCSP_1:87

for b₁ being IncSpace
for b₂, b₃ being POINT of b₁
for b₄ being LINE of b₁
for b₅ being PLANE of b₁ st not b₄ on b₅ & {b₂,b₃} on b₄ & {b₂,b₃} on b₅ holds
b₂ = b₃ by Def8;

theorem Th88: :: INCSP_1:88

for b₁ being IncSpace
for b₂, b₃ being PLANE of b₁ holds
( not b₂ <> b₃ or for b₄ being POINT of b₁ holds
( not b₄ on b₂ or not b₄ on b₃ ) or ex b₄ being LINE of b₁ st
for b₅ being POINT of b₁ holds
( ( b₅ on b₂ & b₅ on b₃ ) iff b₅ on b₄ ) )

proof end;