:: Tarski Geometry Axioms. {P}art {V } -- Half-planes and Planes
:: by Roland Coghetto and Adam Grabowski
::
:: Received December 18, 2023
:: Copyright (c) 2023-2025 Association of Mizar Users

theorem Th1: :: GTARSKI5:1

for S being satisfying_CongruenceIdentity satisfying_BetweennessIdentity TarskiGeometryStruct
for a, b, c being POINT of S st a,b <= c,c holds
a = b

proof end;

definition

let S be non empty TarskiGeometryStruct ;
let a, b be POINT of S;
let A be Subset of S;

pred between a,A,b means :: GTARSKI5:def 1
( A is_line & not a in A & not b in A & ex t being POINT of S st
( t in A & between a,t,b ) );

end;

:: deftheorem defines between GTARSKI5:def 1 :
for S being non empty TarskiGeometryStruct
for a, b being POINT of S
for A being Subset of S holds
( between a,A,b iff ( A is_line & not a in A & not b in A & ex t being POINT of S st
( t in A & between a,t,b ) ) );

theorem :: GTARSKI5:2

for S being non empty satisfying_BetweennessIdentity TarskiGeometryStruct
for a being POINT of S
for A being Subset of S holds not between a,A,a by GTARSKI1:def 10;

definition

let S be non empty TarskiGeometryStruct ;
let a, b, p, q be POINT of S;

pred between a,p,q,b means :: GTARSKI5:def 2
( p <> q & between a, Line (p,q),b );

end;

:: deftheorem defines between GTARSKI5:def 2 :
for S being non empty TarskiGeometryStruct
for a, b, p, q being POINT of S holds
( between a,p,q,b iff ( p <> q & between a, Line (p,q),b ) );

:: 9.2 Satz

theorem :: GTARSKI5:3

for S being non empty satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct
for a, b being POINT of S
for A being Subset of S st between a,A,b holds
between b,A,a by GTARSKI3:14;

theorem Th4: :: GTARSKI5:4

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for a, b, c being POINT of S
for A being Subset of S st between a,b,c & A is_line & a in A & c in A holds
b in A

proof end;

theorem Th5: :: GTARSKI5:5

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for a, b, c being POINT of S
for A being Subset of S st between a,b,c & a <> b & A is_line & a in A & b in A holds
c in A

proof end;

theorem Th6: :: GTARSKI5:6

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for a, c, m, r being POINT of S
for A being Subset of S st between a,A,c & m in A & Middle a,m,c & r in A holds
for b being POINT of S st r out a,b & between r,b,a holds
between b,A,c

proof end;

:: 9.3 Lemma

theorem Th7: :: GTARSKI5:7

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for a, c, m, r being POINT of S
for A being Subset of S st between a,A,c & m in A & Middle a,m,c & r in A holds
for b being POINT of S st r out a,b holds
between b,A,c

proof end;

definition

let S be non empty satisfying_Tarski-model TarskiGeometryStruct ;
let a, b be POINT of S;
let A be Subset of S;

pred are_orthogonal A,a,b means :: GTARSKI5:def 3
are_lorthogonal A,a,a,b;

end;

:: deftheorem defines are_orthogonal GTARSKI5:def 3 :
for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for a, b being POINT of S
for A being Subset of S holds
( are_orthogonal A,a,b iff are_lorthogonal A,a,a,b );

definition

let S be non empty TarskiGeometryStruct ;
let K be Subset of S;

pred K is_half_line means :: GTARSKI5:def 4
ex p, a being POINT of S st
( p <> a & K = halfline (p,a) );

end;

:: deftheorem defines is_half_line GTARSKI5:def 4 :
for S being non empty TarskiGeometryStruct
for K being Subset of S holds
( K is_half_line iff ex p, a being POINT of S st
( p <> a & K = halfline (p,a) ) );

theorem Th8: :: GTARSKI5:8

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d, e being POINT of S st b <> c & c <> d & between b,c,d & ( between a,b,c or between b,a,c ) & ( between c,d,e or between c,e,d ) holds
between a,c,e

proof end;

theorem Th9: :: GTARSKI5:9

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, c, m, r, s being POINT of S
for A being Subset of S st r <> s & s,c <= r,a & between a,A,c & r in A & are_orthogonal A,r,a & s in A & are_orthogonal A,s,c holds
( ( Middle r,m,s implies for u being POINT of S holds
( r out u,a iff s out reflection (m,u),c ) ) & ( for u, v being POINT of S st r out u,a & s out v,c holds
between u,A,v ) )

proof end;

:: 9.4 Lemma

theorem Th10: :: GTARSKI5:10

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, c, m, r, s being POINT of S
for A being Subset of S st between a,A,c & r in A & are_orthogonal A,r,a & s in A & are_orthogonal A,s,c holds
( ( Middle r,m,s implies for u being POINT of S holds
( r out u,a iff s out reflection (m,u),c ) ) & ( for u, v being POINT of S st r out u,a & s out v,c holds
between u,A,v ) )

proof end;

theorem :: GTARSKI5:11

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b being POINT of S st a <> b holds
a out b,b by GTARSKI3:13;

:: Satz 9.5 (Gupta 1965)

theorem Th12: :: GTARSKI5:12

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, c, r being POINT of S
for A being Subset of S st between a,A,c & r in A holds
for b being POINT of S st r out a,b holds
between b,A,c

proof end;

:: Satz 9.6 (Satz von Pash, Exterior form - Gupta 1965)

theorem :: GTARSKI5:13

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c, p, q being POINT of S st between a,c,p & between b,q,c holds
ex x being POINT of S st
( between a,x,b & between p,q,x )

proof end;

:: 9.7 Definition

definition

let S be non empty TarskiGeometryStruct ;
let A be Subset of S;
let a, b be POINT of S;

pred A out a,b means :: GTARSKI5:def 5
ex c being POINT of S st
( between a,A,c & between b,A,c );

end;

:: deftheorem defines out GTARSKI5:def 5 :
for S being non empty TarskiGeometryStruct
for A being Subset of S
for a, b being POINT of S holds
( A out a,b iff ex c being POINT of S st
( between a,A,c & between b,A,c ) );

definition

let S be non empty TarskiGeometryStruct ;
let a, b, p, q be POINT of S;

pred p,q out a,b means :: GTARSKI5:def 6
( p <> q & Line (p,q) out a,b );

end;

:: deftheorem defines out GTARSKI5:def 6 :
for S being non empty TarskiGeometryStruct
for a, b, p, q being POINT of S holds
( p,q out a,b iff ( p <> q & Line (p,q) out a,b ) );

:: 9.8 Satz

theorem Th14: :: GTARSKI5:14

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c being POINT of S
for A being Subset of S st between a,A,c holds
( between b,A,c iff A out a,b )

proof end;

:: 9.9 Satz

theorem Th15: :: GTARSKI5:15

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b being POINT of S
for A being Subset of S st between a,A,b holds
not A out a,b

proof end;

:: 9.10 Lemma

theorem Th16: :: GTARSKI5:16

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a being POINT of S
for A being Subset of S st A is_line & not a in A holds
ex c being POINT of S st between a,A,c

proof end;

:: 9.11 Satz

theorem Th17: :: GTARSKI5:17

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a being POINT of S
for A being Subset of S st A is_line & not a in A holds
A out a,a

proof end;

:: 9.12 Satz

theorem :: GTARSKI5:18

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b being POINT of S
for A being Subset of S st A out a,b holds
A out b,a ;

:: 9.13 Satz

theorem Th19: :: GTARSKI5:19

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c being POINT of S
for A being Subset of S st A out a,b & A out b,c holds
A out a,c

proof end;

:: 9.14 Definition

definition

let S be non empty TarskiGeometryStruct ;
let A be Subset of S;
let a be POINT of S;

func half-plane (A,a) -> Subset of S equals :: GTARSKI5:def 7
{ x where x is POINT of S : A out x,a } ;

correctness
coherence
{ x where x is POINT of S : A out x,a } is Subset of S;

proof end;

end;

:: deftheorem defines half-plane GTARSKI5:def 7 :
for S being non empty TarskiGeometryStruct
for A being Subset of S
for a being POINT of S holds half-plane (A,a) = { x where x is POINT of S : A out x,a } ;

:: 9.15 Definition

definition

let S be non empty TarskiGeometryStruct ;
let p, q, a be POINT of S;
assume not Collinear p,q,a ;

func half-plane (p,q,a) -> set equals :: GTARSKI5:def 8
half-plane ((Line (p,q)),a);

correctness
coherence
half-plane ((Line (p,q)),a) is set ;
;

end;

:: deftheorem defines half-plane GTARSKI5:def 8 :
for S being non empty TarskiGeometryStruct
for p, q, a being POINT of S st not Collinear p,q,a holds
half-plane (p,q,a) = half-plane ((Line (p,q)),a);

theorem Th20: :: GTARSKI5:20

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a being POINT of S
for A being Subset of S st A is_line & not a in A holds
a in half-plane (A,a)

proof end;

theorem Th21: :: GTARSKI5:21

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b being POINT of S
for A being Subset of S st A is_line & not a in A & not b in A & b in half-plane (A,a) holds
a in half-plane (A,b)

proof end;

theorem Th22: :: GTARSKI5:22

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b being POINT of S
for A being Subset of S st b in half-plane (A,a) holds
half-plane (A,b) c= half-plane (A,a)

proof end;

theorem Th23: :: GTARSKI5:23

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b being POINT of S
for A being Subset of S st A is_line & not a in A & not b in A & b in half-plane (A,a) holds
half-plane (A,b) = half-plane (A,a)

proof end;

definition

let S be non empty TarskiGeometryStruct ;
let A be Subset of S;
let a, b be POINT of S;

pred A,a is_opposite-half-plane b means :: GTARSKI5:def 9
between a,A,b;

end;

:: deftheorem defines is_opposite-half-plane GTARSKI5:def 9 :
for S being non empty TarskiGeometryStruct
for A being Subset of S
for a, b being POINT of S holds
( A,a is_opposite-half-plane b iff between a,A,b );

theorem Th24: :: GTARSKI5:24

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b being POINT of S
for A being Subset of S st A out a,b holds
( A is_line & not a in A & not b in A )

proof end;

:: 9.17 Satz

theorem :: GTARSKI5:25

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c being POINT of S
for A being Subset of S st A out a,b & between a,c,b holds
A out c,a

proof end;

:: 9.18 Satz

theorem :: GTARSKI5:26

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, p being POINT of S
for A being Subset of S st A is_line & p in A & Collinear a,b,p holds
( between a,A,b iff ( between a,p,b & not a in A & not b in A ) )

proof end;

theorem Th27: :: GTARSKI5:27

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, p being POINT of S
for A being Subset of S st A is_line & p in A & p out a,b & not a in A holds
between b,A, reflection (p,a)

proof end;

theorem Th28: :: GTARSKI5:28

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, p being POINT of S
for A being Subset of S st A is_line & p in A & not a in A holds
between a,A, reflection (p,a)

proof end;

:: 9.19 Satz

theorem Th29: :: GTARSKI5:29

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, p being POINT of S
for A being Subset of S st A is_line & p in A & Collinear a,b,p holds
( A out a,b iff ( p out a,b & not a in A ) )

proof end;

:: 9.20 Definition

definition

let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ;
let A be Subset of S;
let r be POINT of S;
assume that
A1: A is_line and
A2: not r in A ;

func Plane (A,r) -> Subset of S means :Def10: :: GTARSKI5:def 10
ex r9 being POINT of S st
( between r,A,r9 & it = ((half-plane (A,r)) \/ A) \/ (half-plane (A,r9)) );

existence
ex b₁ being Subset of S ex r9 being POINT of S st
( between r,A,r9 & b₁ = ((half-plane (A,r)) \/ A) \/ (half-plane (A,r9)) )

proof end;

uniqueness
for b₁, b₂ being Subset of S st ex r9 being POINT of S st
( between r,A,r9 & b₁ = ((half-plane (A,r)) \/ A) \/ (half-plane (A,r9)) ) & ex r9 being POINT of S st
( between r,A,r9 & b₂ = ((half-plane (A,r)) \/ A) \/ (half-plane (A,r9)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines Plane GTARSKI5:def 10 :
for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for A being Subset of S
for r being POINT of S st A is_line & not r in A holds
for b₄ being Subset of S holds
( b₄ = Plane (A,r) iff ex r9 being POINT of S st
( between r,A,r9 & b₄ = ((half-plane (A,r)) \/ A) \/ (half-plane (A,r9)) ) );

theorem Th30: :: GTARSKI5:30

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for r being POINT of S
for A being Subset of S st A is_line & not r in A holds
half-plane (A,r) c= Plane (A,r)

proof end;

theorem Th31: :: GTARSKI5:31

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for r being POINT of S
for A being Subset of S st A is_line & not r in A holds
( A c= Plane (A,r) & r in Plane (A,r) )

proof end;

theorem Th32: :: GTARSKI5:32

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for r being POINT of S
for A being Subset of S st A is_line & not r in A holds
Plane (A,r) = { x where x is POINT of S : ( A out x,r or x in A or between r,A,x ) }

proof end;

definition

let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ;
let p, q, r be POINT of S;
assume not Collinear p,q,r ;

func Plane (p,q,r) -> Subset of S equals :Def11: :: GTARSKI5:def 11
Plane ((Line (p,q)),r);

coherence
Plane ((Line (p,q)),r) is Subset of S ;

end;

:: deftheorem Def11 defines Plane GTARSKI5:def 11 :
for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for p, q, r being POINT of S st not Collinear p,q,r holds
Plane (p,q,r) = Plane ((Line (p,q)),r);

definition

let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ;
let E be Subset of S;

pred E is_plane means :: GTARSKI5:def 12
ex p, q, r being POINT of S st
( not Collinear p,q,r & E = Plane (p,q,r) );

end;

:: deftheorem defines is_plane GTARSKI5:def 12 :
for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for E being Subset of S holds
( E is_plane iff ex p, q, r being POINT of S st
( not Collinear p,q,r & E = Plane (p,q,r) ) );

theorem :: GTARSKI5:33

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b being POINT of S
for A being Subset of S st between a,A,b holds
b in Plane (A,a)

proof end;

:: 9.21 Satz

theorem Th34: :: GTARSKI5:34

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for r, s being POINT of S
for A being Subset of S st A is_line & not r in A & s in Plane (A,r) & not s in A holds
Plane (A,r) = Plane (A,s)

proof end;

theorem :: GTARSKI5:35

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for p, q being POINT of S
for A, A9 being Subset of S st A,A9 Is p & A,A9 Is q holds
p = q by GTARSKI3:89;

theorem Th36: :: GTARSKI5:36

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, p being POINT of S
for A being Subset of S st A is_line & a in A & p in A holds
reflection (p,a) in A

proof end;

:: 9.22 Lemma

theorem Th37: :: GTARSKI5:37

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for p, r being POINT of S
for A, A9 being Subset of S st A,A9 Is p & r in A9 & r <> p holds
A9 c= Plane (A,r)

proof end;

theorem Th38: :: GTARSKI5:38

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for A, A9 being Subset of S st A is_line & A9 is_line & A <> A9 holds
ex r being POINT of S st
( not r in A & r in A9 )

proof end;

:: 9.23 Definition

definition

let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ;
let A, A9 be Subset of S;
assume that
A1: A is_line and
A2: A9 is_line and
A3: A <> A9 and
A4: not A /\ A9 is empty ;

func Plane (A,A9) -> Subset of S means :Def13: :: GTARSKI5:def 13
ex r being POINT of S st
( not r in A & r in A9 & it = Plane (A,r) );

existence
ex b₁ being Subset of S ex r being POINT of S st
( not r in A & r in A9 & b₁ = Plane (A,r) )

proof end;

uniqueness
for b₁, b₂ being Subset of S st ex r being POINT of S st
( not r in A & r in A9 & b₁ = Plane (A,r) ) & ex r being POINT of S st
( not r in A & r in A9 & b₂ = Plane (A,r) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def13 defines Plane GTARSKI5:def 13 :
for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for A, A9 being Subset of S st A is_line & A9 is_line & A <> A9 & not A /\ A9 is empty holds
for b₄ being Subset of S holds
( b₄ = Plane (A,A9) iff ex r being POINT of S st
( not r in A & r in A9 & b₄ = Plane (A,r) ) );

theorem Th39: :: GTARSKI5:39

for S being non empty TarskiGeometryStruct
for A, B being Subset of S
for x being POINT of S st A,B Is x holds
B,A Is x ;

theorem Th40: :: GTARSKI5:40

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for p being POINT of S
for A, A9 being Subset of S st A,A9 Is p holds
( A c= Plane (A9,A) & A9 c= Plane (A,A9) )

proof end;

theorem Th41: :: GTARSKI5:41

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for p being POINT of S
for A, A9 being Subset of S st A,A9 Is p holds
ex r being POINT of S st
( not r in A & r in A9 & Plane (A,A9) = Plane (A,r) & A9 = Line (r,p) & ex r9 being POINT of S st
( between r,p,r9 & p <> r9 & Collinear r,p,r9 & not r9 in A & Plane (A,r) = Plane (A,r9) ) )

proof end;

theorem Th42: :: GTARSKI5:42

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for p being POINT of S
for A, A9 being Subset of S st A,A9 Is p holds
Plane (A,A9) c= Plane (A9,A)

proof end;

:: 9.24 Satz

theorem Th43: :: GTARSKI5:43

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for p being POINT of S
for A, A9 being Subset of S st A,A9 Is p holds
( A c= Plane (A,A9) & A9 c= Plane (A,A9) & Plane (A,A9) = Plane (A9,A) )

proof end;

theorem Th44: :: GTARSKI5:44

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c, p, q, r being POINT of S
for E being Subset of S st a in E & b in E & a <> b & not Collinear p,q,r & E = Plane (p,q,r) & c in Line (p,q) & not c in Line (a,b) & not b in Line (p,q) holds
( Line (a,b) c= E & ex c being POINT of S st
( not Collinear a,b,c & E = Plane (a,b,c) ) )

proof end;

theorem Th45: :: GTARSKI5:45

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, p, q, r being POINT of S
for E being Subset of S st a in E & b in E & a <> b & not Collinear p,q,r & E = Plane (p,q,r) & not b in Line (p,q) & Line (p,q) <> Line (a,b) holds
( Line (a,b) c= E & ex c being POINT of S st
( not Collinear a,b,c & E = Plane (a,b,c) ) )

proof end;

:: Satz 9.25

theorem Th46: :: GTARSKI5:46

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b being POINT of S
for E being Subset of S st E is_plane & a in E & b in E & a <> b holds
( Line (a,b) c= E & ex c being POINT of S st
( not Collinear a,b,c & E = Plane (a,b,c) ) )

proof end;

:: Satz 9.26

theorem Th47: :: GTARSKI5:47

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c being POINT of S
for E being Subset of S st not Collinear a,b,c & E is_plane & a in E & b in E & c in E holds
E = Plane (a,b,c)

proof end;

theorem Th48: :: GTARSKI5:48

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a being POINT of S
for A being Subset of S st A is_line & not a in A holds
a in Plane (A,a)

proof end;

:: 9.27.(1) Satz

theorem Th49: :: GTARSKI5:49

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c being POINT of S st not Collinear a,b,c holds
ex E being Subset of S st
( Plane (a,b,c) = E & E is_plane & a in E & b in E & c in E )

proof end;

:: 9.27.(2) Satz

theorem Th50: :: GTARSKI5:50

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for c being POINT of S
for A being Subset of S st A is_line & not c in A holds
ex E being Subset of S st
( E is_plane & A c= E & c in E & Plane (A,c) = E )

proof end;

:: 9.27.(3) Satz

theorem :: GTARSKI5:51

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for p being POINT of S
for A, A9 being Subset of S st A,A9 Is p holds
ex E being Subset of S st
( E is_plane & A c= E & A9 c= E & Plane (A,A9) = E )

proof end;

:: 9.28 Folgerung

theorem Th52: :: GTARSKI5:52

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c being POINT of S st not Collinear a,b,c holds
for E1, E2 being Subset of S st E1 is_plane & a in E1 & b in E1 & c in E1 & E2 is_plane & a in E2 & b in E2 & c in E2 holds
E1 = E2

proof end;

:: 9.29 Folgerung

theorem Th53: :: GTARSKI5:53

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c being POINT of S st not Collinear a,b,c holds
( Plane (a,b,c) = Plane (b,c,a) & Plane (a,b,c) = Plane (c,a,b) & Plane (a,b,c) = Plane (b,a,c) & Plane (a,b,c) = Plane (a,c,b) & Plane (a,b,c) = Plane (c,b,a) )

proof end;

:: 9.30 Folgerung

theorem :: GTARSKI5:54

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for A being Subset of S st A is_line holds
for E1, E2 being Subset of S st E1 is_plane & E2 is_plane & A c= E1 & A c= E2 & E1 <> E2 holds
for x being POINT of S holds
( ( x in E1 & x in E2 ) iff x in A )

proof end;

theorem :: GTARSKI5:55

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for p, q, r, s being POINT of S st p,q out s,r holds
( s <> p & s <> q & r <> p & r <> q & p <> q )

proof end;

theorem :: GTARSKI5:56

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c being POINT of S holds not between a, Line (b,c),a by GTARSKI1:def 10;

theorem :: GTARSKI5:57

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b being POINT of S
for A being Subset of S st between a,A,b holds
a <> b by GTARSKI1:def 10;

theorem :: GTARSKI5:58

for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ex p, q being POINT of S st p <> q

proof end;

:: 9.31 Satz

theorem Th59: :: GTARSKI5:59

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for p, q, r, s being POINT of S st p,q out s,r & p,r out s,q holds
between q, Line (p,s),r

proof end;

:: 9.32.(i) Definition

definition

let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ;
let A be Subset of S;

pred A are_coplanar means :: GTARSKI5:def 14
ex E being Subset of S st
( E is_plane & A c= E );

end;

:: deftheorem defines are_coplanar GTARSKI5:def 14 :
for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for A being Subset of S holds
( A are_coplanar iff ex E being Subset of S st
( E is_plane & A c= E ) );

:: 9.32.(ii) Definition

definition

let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ;
let a, b, c, d be POINT of S;

pred a,b,c,d are_coplanar means :: GTARSKI5:def 15
ex E being Subset of S st
( E is_plane & a in E & b in E & c in E & d in E );

end;

:: deftheorem defines are_coplanar GTARSKI5:def 15 :
for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c, d being POINT of S holds
( a,b,c,d are_coplanar iff ex E being Subset of S st
( E is_plane & a in E & b in E & c in E & d in E ) );

theorem :: GTARSKI5:60

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c, d being POINT of S st a,b,c,d are_coplanar holds
( a,b,d,c are_coplanar & a,c,b,d are_coplanar & a,c,d,b are_coplanar & a,d,c,b are_coplanar & a,d,b,c are_coplanar & b,a,c,d are_coplanar & b,a,d,c are_coplanar & b,c,a,d are_coplanar & b,c,d,a are_coplanar & b,d,a,c are_coplanar & b,d,c,a are_coplanar & c,a,b,d are_coplanar & c,a,d,b are_coplanar & c,b,a,d are_coplanar & c,b,d,a are_coplanar & d,a,b,c are_coplanar & d,a,c,b are_coplanar & d,b,a,c are_coplanar & d,b,c,a are_coplanar ) ;

theorem Th61: :: GTARSKI5:61

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a being POINT of S holds a,a,a,a are_coplanar

proof end;

theorem Th62: :: GTARSKI5:62

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b being POINT of S holds a,a,a,b are_coplanar

proof end;

theorem Th63: :: GTARSKI5:63

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c being POINT of S holds a,a,b,c are_coplanar

proof end;

theorem Th64: :: GTARSKI5:64

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c, d, x being POINT of S st Collinear a,b,x & Collinear c,d,x & a <> x & c <> x holds
a,b,c,d are_coplanar

proof end;

theorem Th65: :: GTARSKI5:65

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c, d, x being POINT of S st Collinear b,a,x & Collinear c,d,x & b <> x & c <> x holds
a,b,c,d are_coplanar

proof end;

theorem Th66: :: GTARSKI5:66

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c, d, x being POINT of S st Collinear a,b,x & Collinear c,d,x & b <> x & c <> x holds
a,b,c,d are_coplanar

proof end;

theorem Th67: :: GTARSKI5:67

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c, d, x being POINT of S st Collinear a,b,x & Collinear c,d,x & ( ( b <> x & c <> x ) or ( b <> x & d <> x ) or ( a <> x & c <> x ) or ( a <> x & d <> x ) ) holds
a,b,c,d are_coplanar

proof end;

:: 9.33 Satz

theorem Th68: :: GTARSKI5:68

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c, d being POINT of S holds
( a,b,c,d are_coplanar iff ex x being POINT of S st
( ( Collinear a,b,x & Collinear c,d,x ) or ( Collinear a,c,x & Collinear b,d,x ) or ( Collinear a,d,x & Collinear b,c,x ) ) )

proof end;

theorem Th69: :: GTARSKI5:69

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c being POINT of S st not Collinear a,b,c holds
( Plane (a,b,c) is_plane & a in Plane (a,b,c) & b in Plane (a,b,c) & c in Plane (a,b,c) & ( for u, v being POINT of S st u in Plane (a,b,c) & v in Plane (a,b,c) & u <> v holds
Line (u,v) c= Plane (a,b,c) ) )

proof end;

:: 9.34 Satz

theorem :: GTARSKI5:70

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c being POINT of S st not Collinear a,b,c holds
for E being Subset of S st a in E & b in E & c in E & ( for u, v being POINT of S st u in E & v in E & u <> v holds
Line (u,v) c= E ) holds
Plane (a,b,c) c= E

proof end;

:: 9.37 Definition n = 2

definition

let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ;
let a, b be POINT of S;
let A be Subset of S;

pred between2 a,A,b means :: GTARSKI5:def 16
( A is_plane & not a in A & not b in A & ex t being POINT of S st
( t in A & between a,t,b ) );

end;

:: deftheorem defines between2 GTARSKI5:def 16 :
for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b being POINT of S
for A being Subset of S holds
( between2 a,A,b iff ( A is_plane & not a in A & not b in A & ex t being POINT of S st
( t in A & between a,t,b ) ) );

:: 9.38 Satz (n = 2)

theorem :: GTARSKI5:71

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b being POINT of S
for A being Subset of S st between2 a,A,b holds
between2 b,A,a by GTARSKI3:14;

theorem :: GTARSKI5:72

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c, p being POINT of S st between a,p,c & p out a,b holds
between b,p,c

proof end;

:: 9.39 Satz (n = 2)

theorem Th73: :: GTARSKI5:73

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, c, r being POINT of S
for A being Subset of S st between2 a,A,c & r in A holds
for b being POINT of S st r out a,b holds
between2 b,A,c

proof end;

:: 9.40 Definition n = 2

definition

let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ;
let a, b be POINT of S;
let A be Subset of S;

pred A out2 a,b means :: GTARSKI5:def 17
ex c being POINT of S st
( between2 a,A,c & between2 b,A,c );

end;

:: deftheorem defines out2 GTARSKI5:def 17 :
for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b being POINT of S
for A being Subset of S holds
( A out2 a,b iff ex c being POINT of S st
( between2 a,A,c & between2 b,A,c ) );

:: 9.41 Satz (n = 2)

theorem Th74: :: GTARSKI5:74

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c being POINT of S
for A being Subset of S st between2 a,A,c holds
( between2 b,A,c iff A out2 a,b )

proof end;

:: 9.9 Satz (Version n = 2)

theorem :: GTARSKI5:75

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b being POINT of S
for A being Subset of S st between2 a,A,b holds
not A out2 a,b

proof end;

:: 9.10 Lemma (Version n = 2)

theorem Th76: :: GTARSKI5:76

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a being POINT of S
for A being Subset of S st A is_plane & not a in A holds
ex c being POINT of S st between2 a,A,c

proof end;

:: 9.11 Satz (Version n = 2)

theorem Th77: :: GTARSKI5:77

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a being POINT of S
for A being Subset of S st A is_plane & not a in A holds
A out2 a,a

proof end;

:: 9.12 Satz (Version n = 2)

theorem :: GTARSKI5:78

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b being POINT of S
for A being Subset of S st A out2 a,b holds
A out2 b,a ;

:: 9.13 Satz (Version n = 2)

theorem Th79: :: GTARSKI5:79

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c being POINT of S
for A being Subset of S st A out2 a,b & A out2 b,c holds
A out2 a,c

proof end;

:: 9.43 Definition (n = 2)

definition

let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ;
let A be Subset of S;
let a be POINT of S;
assume that
A is_plane and
not a in A ;

func half-space3 (A,a) -> Subset of S equals :Def18: :: GTARSKI5:def 18
{ x where x is POINT of S : A out2 x,a } ;

correctness
coherence
{ x where x is POINT of S : A out2 x,a } is Subset of S;

proof end;

end;

:: deftheorem Def18 defines half-space3 GTARSKI5:def 18 :
for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for A being Subset of S
for a being POINT of S st A is_plane & not a in A holds
half-space3 (A,a) = { x where x is POINT of S : A out2 x,a } ;

definition

let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ;
let p, q, a be POINT of S;
assume not Collinear p,q,a ;

func half-space3 (p,q,a) -> set equals :: GTARSKI5:def 19
half-space3 ((Line (p,q)),a);

correctness
coherence
half-space3 ((Line (p,q)),a) is set ;
;

end;

:: deftheorem defines half-space3 GTARSKI5:def 19 :
for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for p, q, a being POINT of S st not Collinear p,q,a holds
half-space3 (p,q,a) = half-space3 ((Line (p,q)),a);

theorem Th80: :: GTARSKI5:80

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a being POINT of S
for A being Subset of S st A is_plane & not a in A holds
a in half-space3 (A,a)

proof end;

theorem Th81: :: GTARSKI5:81

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b being POINT of S
for A being Subset of S st A is_plane & not a in A & not b in A & b in half-space3 (A,a) holds
a in half-space3 (A,b)

proof end;

theorem Th82: :: GTARSKI5:82

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b being POINT of S
for A being Subset of S st A is_plane & not a in A & not b in A & b in half-space3 (A,a) holds
half-space3 (A,b) c= half-space3 (A,a)

proof end;

theorem Th83: :: GTARSKI5:83

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b being POINT of S
for A being Subset of S st A is_plane & not a in A & not b in A & b in half-space3 (A,a) holds
half-space3 (A,b) = half-space3 (A,a)

proof end;

:: 9.44 Definition (n = 2)

definition

let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ;
let A be Subset of S;
let r be POINT of S;
assume that
A1: A is_plane and
A2: not r in A ;

func space3 (A,r) -> Subset of S means :Def20: :: GTARSKI5:def 20
ex r9 being POINT of S st
( between2 r,A,r9 & it = ((half-space3 (A,r)) \/ A) \/ (half-space3 (A,r9)) );

existence
ex b₁ being Subset of S ex r9 being POINT of S st
( between2 r,A,r9 & b₁ = ((half-space3 (A,r)) \/ A) \/ (half-space3 (A,r9)) )

proof end;

uniqueness
for b₁, b₂ being Subset of S st ex r9 being POINT of S st
( between2 r,A,r9 & b₁ = ((half-space3 (A,r)) \/ A) \/ (half-space3 (A,r9)) ) & ex r9 being POINT of S st
( between2 r,A,r9 & b₂ = ((half-space3 (A,r)) \/ A) \/ (half-space3 (A,r9)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def20 defines space3 GTARSKI5:def 20 :
for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for A being Subset of S
for r being POINT of S st A is_plane & not r in A holds
for b₄ being Subset of S holds
( b₄ = space3 (A,r) iff ex r9 being POINT of S st
( between2 r,A,r9 & b₄ = ((half-space3 (A,r)) \/ A) \/ (half-space3 (A,r9)) ) );

theorem Th84: :: GTARSKI5:84

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for r being POINT of S
for A being Subset of S st A is_plane & not r in A holds
half-space3 (A,r) c= space3 (A,r)

proof end;

theorem :: GTARSKI5:85

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for r being POINT of S
for A being Subset of S st A is_plane & not r in A holds
( A c= space3 (A,r) & r in space3 (A,r) )

proof end;

theorem :: GTARSKI5:86

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for r being POINT of S
for A being Subset of S st A is_plane & not r in A holds
space3 (A,r) = { x where x is POINT of S : ( A out2 x,r or x in A or between2 r,A,x ) }

proof end;

:: 9.44 Definition (n = 2)

definition

let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ;
let p0, p1, p2, r be POINT of S;
assume not p0,p1,p2,r are_coplanar ;

func space3 (p0,p1,p2,r) -> Subset of S equals :Def21: :: GTARSKI5:def 21
space3 ((Plane (p0,p1,p2)),r);

coherence
space3 ((Plane (p0,p1,p2)),r) is Subset of S ;

end;

:: deftheorem Def21 defines space3 GTARSKI5:def 21 :
for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for p0, p1, p2, r being POINT of S st not p0,p1,p2,r are_coplanar holds
space3 (p0,p1,p2,r) = space3 ((Plane (p0,p1,p2)),r);

definition

let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ;
let E be Subset of S;

pred E is_space3 means :: GTARSKI5:def 22
ex r being POINT of S ex A being Subset of S st
( A is_plane & not r in A & E = space3 (A,r) );

end;

:: deftheorem defines is_space3 GTARSKI5:def 22 :
for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for E being Subset of S holds
( E is_space3 iff ex r being POINT of S ex A being Subset of S st
( A is_plane & not r in A & E = space3 (A,r) ) );

theorem Th87: :: GTARSKI5:87

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c, d being POINT of S
for A being Subset of S st A is_plane & not Collinear a,b,c & a in A & b in A & c in A & not d in A holds
not a,b,c,d are_coplanar by Th52;

theorem :: GTARSKI5:88

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for E being Subset of S st E is_space3 holds
ex a, b, c, d being POINT of S st
( not a,b,c,d are_coplanar & E = space3 (a,b,c,d) )

proof end;