:: INCSP_1 semantic presentation

definition

attr c₁ 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 c₁,the Lines of c₁;

end;

definition

attr c₁ 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 c₁,the Planes of c₁;
sel Inc3 c₁ -> Relation of the Lines of c₁,the Planes of c₁;

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;

definition

let S be IncProjStr ;
let A be POINT of S;
let L be LINE of S;
pred A on L means :Def1: :: INCSP_1:def 1
[A,L] in the Inc of S;

end;

:: deftheorem Def1 defines on INCSP_1:def 1 :

definition

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

end;

:: deftheorem Def2 defines on INCSP_1:def 2 :

definition

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

end;

:: deftheorem Def3 defines on INCSP_1:def 3 :

definition

let S be IncProjStr ;
let F be Subset of the Points of S;
let L be LINE of S;
pred F 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 :

definition

let S be IncStruct ;
let F be Subset of the Points of S;
let P be PLANE of S;
pred F 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 :

definition

let S be IncProjStr ;
let F be Subset of the Points of S;
attr F 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 :

notation

let S be IncProjStr ;
let F be Subset of the Points of S;
synonym F is_collinear for linear F;

end;

definition

let S be IncStruct ;
let F be Subset of the Points of S;
attr F 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 :

notation

let S be IncStruct ;
let F be Subset of the Points of S;
synonym F is_coplanar for planar F;

end;

theorem :: INCSP_1:1

canceled;

theorem :: INCSP_1:2

canceled;

theorem :: INCSP_1:3

canceled;

theorem :: INCSP_1:4

canceled;

theorem :: INCSP_1:5

canceled;

theorem :: INCSP_1:6

canceled;

theorem :: INCSP_1:7

canceled;

theorem :: INCSP_1:8

canceled;

theorem :: INCSP_1:9

canceled;

theorem :: INCSP_1:10

canceled;

theorem Th11: :: INCSP_1:11

for S being IncStruct
for A, B being POINT of S
for L being LINE of S holds
( {A,B} on L iff ( A on L & B on L ) )

proof end;

theorem Th12: :: INCSP_1:12

for S being IncStruct
for A, B, C being POINT of S
for L being LINE of S holds
( {A,B,C} on L iff ( A on L & B on L & C on L ) )

proof end;

theorem Th13: :: INCSP_1:13

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

proof end;

theorem Th14: :: INCSP_1:14

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

proof end;

theorem Th15: :: INCSP_1:15

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

proof end;

theorem Th16: :: INCSP_1:16

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

proof end;

theorem Th17: :: INCSP_1:17

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

proof end;

theorem Th18: :: INCSP_1:18

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 )

proof end;

theorem Th19: :: INCSP_1:19

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 )

proof end;

theorem Th20: :: INCSP_1:20

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

proof end;

theorem Th21: :: INCSP_1:21

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

proof end;

theorem :: INCSP_1:22

for S being IncStruct
for G, F being Subset of the Points of S st G c= F & F is_collinear holds
G is_collinear

proof end;

theorem :: INCSP_1:23

for S being IncStruct
for G, F being Subset of the Points of S st G c= F & F is_coplanar holds
G is_coplanar

proof end;

registration

let x, y, z, w be set ;
cluster {x,y,z,w} -> non empty ;
coherence by ENUMSET1:def 2;

end;

definition

let IT be IncStruct ;
attr IT is IncSpace-like means :Def8: :: INCSP_1:def 8
( ( for L being LINE of IT ex A, B being POINT of IT st
( A <> B & {A,B} on L ) ) & ( for A, B being POINT of IT ex L being LINE of IT st {A,B} on L ) & ( for A, B being POINT of IT
for K, L being LINE of IT st A <> B & {A,B} on K & {A,B} on L holds
K = L ) & ( for P being PLANE of IT ex A being POINT of IT st A on P ) & ( for A, B, C being POINT of IT ex P being PLANE of IT st {A,B,C} on P ) & ( for A, B, C being POINT of IT
for P, Q being PLANE of IT st not {A,B,C} is_collinear & {A,B,C} on P & {A,B,C} on Q holds
P = Q ) & ( for L being LINE of IT
for P being PLANE of IT st ex A, B being POINT of IT st
( A <> B & {A,B} on L & {A,B} on P ) holds
L on P ) & ( for A being POINT of IT
for P, Q being PLANE of IT st A on P & A on Q holds
ex B being POINT of IT st
( A <> B & B on P & B on Q ) ) & not for A, B, C, D being POINT of IT holds {A,B,C,D} is_coplanar & ( for A being POINT of IT
for L being LINE of IT
for P being PLANE of IT st A on L & L on P holds
A on P ) );

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 :: INCSP_1:24

canceled;

theorem :: INCSP_1:25

canceled;

theorem :: INCSP_1:26

canceled;

theorem :: INCSP_1:27

canceled;

theorem :: INCSP_1:28

canceled;

theorem :: INCSP_1:29

canceled;

theorem :: INCSP_1:30

canceled;

theorem :: INCSP_1:31

canceled;

theorem :: INCSP_1:32

canceled;

theorem :: INCSP_1:33

canceled;

theorem :: INCSP_1:34

canceled;

theorem Th35: :: INCSP_1:35

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

proof end;

theorem Th36: :: INCSP_1:36

for S being IncSpace
for A, B being POINT of S holds {A,A,B} is_collinear

proof end;

theorem Th37: :: INCSP_1:37

for S being IncSpace
for A, B, C being POINT of S holds {A,A,B,C} is_coplanar

proof end;

theorem Th38: :: INCSP_1:38

for S being IncSpace
for A, B, C, D being POINT of S st {A,B,C} is_collinear holds
{A,B,C,D} is_coplanar

proof end;

theorem Th39: :: INCSP_1:39

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_collinear

proof end;

theorem Th40: :: INCSP_1:40

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_collinear & {A,B,C} on P & not D on P holds
not {A,B,C,D} is_coplanar

proof end;

theorem :: INCSP_1:41

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

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:42

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

proof end;

theorem :: INCSP_1:43

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 )

proof end;

theorem Th44: :: INCSP_1:44

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

proof end;

theorem Th45: :: INCSP_1:45

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 )

proof end;

theorem :: INCSP_1:46

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 )

proof end;

theorem :: INCSP_1:47

for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is_collinear 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 Th48: :: INCSP_1:48

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 )

proof end;

theorem Th49: :: INCSP_1:49

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 )

proof end;

definition

let S be IncSpace;
let A, B be POINT of S;
assume A1: A <> B ;
func Line A,B -> LINE of S means :Def9: :: INCSP_1:def 9
{A,B} on it;
correctness by A1, Def8;

end;

:: deftheorem Def9 defines Line INCSP_1:def 9 :

definition

let S be IncSpace;
let A, B, C be POINT of S;
assume A1: not {A,B,C} is_collinear ;
func Plane A,B,C -> PLANE of S means :Def10: :: INCSP_1:def 10
{A,B,C} on it;
correctness by A1, Def8;

end;

:: deftheorem Def10 defines Plane INCSP_1:def 10 :

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 :Def11: :: INCSP_1:def 11
( A on it & L on it );
existence by Th44;
uniqueness

proof end;

end;

:: deftheorem Def11 defines Plane INCSP_1:def 11 :

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 ) ;
func Plane K,L -> PLANE of S means :Def12: :: INCSP_1:def 12
( K on it & L on it );
existence by A2, Th45;
uniqueness

proof end;

end;

:: deftheorem Def12 defines Plane INCSP_1:def 12 :

theorem :: INCSP_1:50

canceled;

theorem :: INCSP_1:51

canceled;

theorem :: INCSP_1:52

canceled;

theorem :: INCSP_1:53

canceled;

theorem :: INCSP_1:54

canceled;

theorem :: INCSP_1:55

canceled;

theorem :: INCSP_1:56

canceled;

theorem :: INCSP_1:57

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

proof end;

theorem Th58: :: INCSP_1:58

for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is_collinear holds
Plane A,B,C = Plane A,C,B

proof end;

theorem Th59: :: INCSP_1:59

for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is_collinear holds
Plane A,B,C = Plane B,A,C

proof end;

theorem :: INCSP_1:60

for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is_collinear holds
Plane A,B,C = Plane B,C,A

proof end;

theorem Th61: :: INCSP_1:61

for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is_collinear holds
Plane A,B,C = Plane C,A,B

proof end;

theorem :: INCSP_1:62

for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is_collinear holds
Plane A,B,C = Plane C,B,A

proof end;

theorem :: INCSP_1:63

canceled;

theorem :: INCSP_1:64

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

proof end;

theorem Th65: :: INCSP_1:65

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_collinear

proof end;

theorem :: INCSP_1:66

for S being IncSpace
for A, B, C being POINT of S st A <> B & A <> C & {A,B,C} is_collinear holds
Line A,B = Line A,C

proof end;

theorem :: INCSP_1:67

for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is_collinear holds
Plane A,B,C = Plane C,(Line A,B)

proof end;

theorem :: INCSP_1:68

for S being IncSpace
for A, B, C, D being POINT of S st not {A,B,C} is_collinear & D on Plane A,B,C holds
{A,B,C,D} is_coplanar

proof end;

theorem :: INCSP_1:69

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

proof end;

theorem :: INCSP_1:70

for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is_collinear 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_coplanar )

proof end;

theorem Th71: :: INCSP_1:71

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

proof end;

theorem :: INCSP_1:72

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_coplanar ) by Lm2;

theorem :: INCSP_1:73

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

theorem Th74: :: INCSP_1:74

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

proof end;

theorem Th75: :: INCSP_1:75

for S being IncSpace
for A, B, C being POINT of S st not {A,B,C} is_collinear holds
ex D being POINT of S st not {A,B,C,D} is_coplanar

proof end;

theorem Th76: :: INCSP_1:76

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

proof end;

theorem Th77: :: INCSP_1:77

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_coplanar

proof end;

theorem :: INCSP_1:78

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_coplanar

proof end;

theorem :: INCSP_1:79

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 )

proof end;

theorem Th80: :: INCSP_1:80

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 )

proof end;

theorem :: INCSP_1:81

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

proof end;

theorem :: INCSP_1:82

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 )

proof end;

theorem :: INCSP_1:83

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 )

proof end;

theorem :: INCSP_1:84

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 )

proof end;

theorem :: INCSP_1:85

for S being IncSpace
for L being LINE of S ex P, Q being PLANE of S st
( P <> Q & L on P & L on Q )

proof end;

theorem :: INCSP_1:86

canceled;

theorem :: INCSP_1:87

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 & {A,B} on L & {A,B} on P holds
A = B by Def8;

theorem :: INCSP_1:88

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

proof end;