:: by Roland Coghetto and Adam Grabowski

::

:: Received November 29, 2017

:: Copyright (c) 2017-2018 Association of Mizar Users

:: 2.1 Satz

theorem Satz2p1: :: GTARSKI3:1

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct

for a, b being POINT of S holds a,b equiv a,b

for a, b being POINT of S holds a,b equiv a,b

proof end;

:: 2.1 Satz bis

theorem Satz2p1bis: :: GTARSKI3:2

for S being satisfying_CongruenceEquivalenceRelation satisfying_SegmentConstruction TarskiGeometryStruct

for a, b being POINT of S holds a,b equiv a,b

for a, b being POINT of S holds a,b equiv a,b

proof end;

:: 2.2 Satz

theorem Satz2p2: :: GTARSKI3:3

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct

for a, b, c, d being POINT of S st a,b equiv c,d holds

c,d equiv a,b

for a, b, c, d being POINT of S st a,b equiv c,d holds

c,d equiv a,b

proof end;

:: 2.2 Satz bis

theorem Satz2p2bis: :: GTARSKI3:4

for S being satisfying_CongruenceEquivalenceRelation satisfying_SegmentConstruction TarskiGeometryStruct

for a, b, c, d being POINT of S st a,b equiv c,d holds

c,d equiv a,b

for a, b, c, d being POINT of S st a,b equiv c,d holds

c,d equiv a,b

proof end;

:: 2.3 Satz

theorem Satz2p3: :: GTARSKI3:5

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct

for a, b, c, d, e, f being POINT of S st a,b equiv c,d & c,d equiv e,f holds

a,b equiv e,f

for a, b, c, d, e, f being POINT of S st a,b equiv c,d & c,d equiv e,f holds

a,b equiv e,f

proof end;

:: 2.4 Satz

theorem Satz2p4: :: GTARSKI3:6

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct

for a, b, c, d being POINT of S st a,b equiv c,d holds

b,a equiv c,d

for a, b, c, d being POINT of S st a,b equiv c,d holds

b,a equiv c,d

proof end;

:: 2.5 Satz

theorem Satz2p5: :: GTARSKI3:7

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct

for a, b, c, d being POINT of S st a,b equiv c,d holds

a,b equiv d,c

for a, b, c, d being POINT of S st a,b equiv c,d holds

a,b equiv d,c

proof end;

:: 2.8 Satz

theorem Satz2p8: :: GTARSKI3:8

for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction TarskiGeometryStruct

for a, b being POINT of S holds a,a equiv b,b

for a, b being POINT of S holds a,a equiv b,b

proof end;

:: deftheorem defines satisfying_SST_A5 GTARSKI3:def 1 :

for S being TarskiGeometryStruct holds

( S is satisfying_SST_A5 iff for a, b, c, d, a9, b9, c9, d9 being POINT of S st a <> b & between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 & a,d equiv a9,d9 & b,d equiv b9,d9 holds

c,d equiv c9,d9 );

for S being TarskiGeometryStruct holds

( S is satisfying_SST_A5 iff for a, b, c, d, a9, b9, c9, d9 being POINT of S st a <> b & between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 & a,d equiv a9,d9 & b,d equiv b9,d9 holds

c,d equiv c9,d9 );

theorem EQUIV1: :: GTARSKI3:9

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct holds

( S is satisfying_SAS iff S is satisfying_SST_A5 )

( S is satisfying_SAS iff S is satisfying_SST_A5 )

proof end;

registration

for b_{1} being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct st b_{1} is satisfying_SST_A5 holds

b_{1} is satisfying_SAS
by EQUIV1;

end;

cluster satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_SST_A5 -> satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_SAS for TarskiGeometryStruct ;

coherence for b

b

registration

for b_{1} being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct st b_{1} is satisfying_SAS holds

b_{1} is satisfying_SST_A5
by EQUIV1;

end;

cluster satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_SAS -> satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_SST_A5 for TarskiGeometryStruct ;

coherence for b

b

:: deftheorem defines AFS GTARSKI3:def 2 :

for S being TarskiGeometryStruct

for a, b, c, d, a9, b9, c9, d9 being POINT of S holds

( a,b,c,d AFS a9,b9,c9,d9 iff ( between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 & a,d equiv a9,d9 & b,d equiv b9,d9 ) );

for S being TarskiGeometryStruct

for a, b, c, d, a9, b9, c9, d9 being POINT of S holds

( a,b,c,d AFS a9,b9,c9,d9 iff ( between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 & a,d equiv a9,d9 & b,d equiv b9,d9 ) );

theorem Axiom5AFS: :: GTARSKI3:10

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_SAS TarskiGeometryStruct

for a, b, c, d, a9, b9, c9, d9 being POINT of S st a,b,c,d AFS a9,b9,c9,d9 & a <> b holds

c,d equiv c9,d9

for a, b, c, d, a9, b9, c9, d9 being POINT of S st a,b,c,d AFS a9,b9,c9,d9 & a <> b holds

c,d equiv c9,d9

proof end;

:: 2.11 Satz

theorem Satz2p11: :: GTARSKI3:11

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS TarskiGeometryStruct

for a, b, c, a9, b9, c9 being POINT of S st between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 holds

a,c equiv a9,c9

for a, b, c, a9, b9, c9 being POINT of S st between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 holds

a,c equiv a9,c9

proof end;

:: 2.12 Satz

theorem Satz2p12: :: GTARSKI3:12

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS TarskiGeometryStruct

for q, a, b, c being POINT of S st q <> a holds

for x1, x2 being POINT of S st between q,a,x1 & a,x1 equiv b,c & between q,a,x2 & a,x2 equiv b,c holds

x1 = x2

for q, a, b, c being POINT of S st q <> a holds

for x1, x2 being POINT of S st between q,a,x1 & a,x1 equiv b,c & between q,a,x2 & a,x2 equiv b,c holds

x1 = x2

proof end;

:: 3.1 Satz

theorem Satz3p1: :: GTARSKI3:13

for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction TarskiGeometryStruct

for a, b being POINT of S holds between a,b,b

for a, b being POINT of S holds between a,b,b

proof end;

:: 3.2 Satz

theorem Satz3p2: :: GTARSKI3:14

for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct

for a, b, c being POINT of S st between a,b,c holds

between c,b,a

for a, b, c being POINT of S st between a,b,c holds

between c,b,a

proof end;

:: 3.3 Satz

theorem :: GTARSKI3:15

for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct

for a, b being POINT of S holds between a,a,b by Satz3p1, Satz3p2;

for a, b being POINT of S holds between a,a,b by Satz3p1, Satz3p2;

:: 3.4 Satz

theorem Satz3p4: :: GTARSKI3:16

for S being satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct

for a, b, c being POINT of S st between a,b,c & between b,a,c holds

a = b

for a, b, c being POINT of S st between a,b,c & between b,a,c holds

a = b

proof end;

Satz3p5p1: for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct

for a, b, c, d being POINT of S st between a,b,d & between b,c,d holds

between a,b,c

proof end;

Satz3p6p1: for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct

for a, b, c, d being POINT of S st between a,b,c & between a,c,d holds

between b,c,d

proof end;

Satz3p7p1: for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, d being POINT of S st between a,b,c & between b,c,d & b <> c holds

between a,c,d

proof end;

Satz3p5p2: for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, d being POINT of S st between a,b,d & between b,c,d holds

between a,c,d

proof end;

Satz3p6p2: for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, d being POINT of S st between a,b,c & between a,c,d holds

between a,b,d

proof end;

Satz3p7p2: for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, d being POINT of S st between a,b,c & between b,c,d & b <> c holds

between a,b,d

proof end;

:: 3.5 Satz

theorem :: GTARSKI3:17

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, d being POINT of S st between a,b,d & between b,c,d holds

( between a,b,c & between a,c,d ) by Satz3p5p1, Satz3p5p2;

for a, b, c, d being POINT of S st between a,b,d & between b,c,d holds

( between a,b,c & between a,c,d ) by Satz3p5p1, Satz3p5p2;

:: 3.6 Satz

theorem :: GTARSKI3:18

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, d being POINT of S st between a,b,c & between a,c,d holds

( between b,c,d & between a,b,d ) by Satz3p6p1, Satz3p6p2;

for a, b, c, d being POINT of S st between a,b,c & between a,c,d holds

( between b,c,d & between a,b,d ) by Satz3p6p1, Satz3p6p2;

:: 3.7 Satz

theorem :: GTARSKI3:19

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, d being POINT of S st between a,b,c & between b,c,d & b <> c holds

( between a,c,d & between a,b,d ) by Satz3p7p1, Satz3p7p2;

for a, b, c, d being POINT of S st between a,b,c & between b,c,d & b <> c holds

( between a,c,d & between a,b,d ) by Satz3p7p1, Satz3p7p2;

:: deftheorem defines between4 GTARSKI3:def 3 :

for S being TarskiGeometryStruct

for a, b, c, d being POINT of S holds

( between4 a,b,c,d iff ( between a,b,c & between a,b,d & between a,c,d & between b,c,d ) );

for S being TarskiGeometryStruct

for a, b, c, d being POINT of S holds

( between4 a,b,c,d iff ( between a,b,c & between a,b,d & between a,c,d & between b,c,d ) );

:: deftheorem defines between5 GTARSKI3:def 4 :

for S being TarskiGeometryStruct

for a, b, c, d, e being POINT of S holds

( between5 a,b,c,d,e iff ( between a,b,c & between a,b,d & between a,b,e & between a,c,d & between a,c,e & between a,d,e & between b,c,d & between b,c,e & between b,d,e & between c,d,e ) );

for S being TarskiGeometryStruct

for a, b, c, d, e being POINT of S holds

( between5 a,b,c,d,e iff ( between a,b,c & between a,b,d & between a,b,e & between a,c,d & between a,c,e & between a,d,e & between b,c,d & between b,c,e & between b,d,e & between c,d,e ) );

theorem :: GTARSKI3:20

for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct

for a, b, c being POINT of S st between a,b,c holds

between c,b,a by Satz3p2;

for a, b, c being POINT of S st between a,b,c holds

between c,b,a by Satz3p2;

theorem :: GTARSKI3:21

for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct

for a, b, c, d being POINT of S st between4 a,b,c,d holds

between4 d,c,b,a by Satz3p2;

for a, b, c, d being POINT of S st between4 a,b,c,d holds

between4 d,c,b,a by Satz3p2;

theorem :: GTARSKI3:22

for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct

for a, b, c, d, e being POINT of S st between5 a,b,c,d,e holds

between5 e,d,c,b,a by Satz3p2;

for a, b, c, d, e being POINT of S st between5 a,b,c,d,e holds

between5 e,d,c,b,a by Satz3p2;

theorem :: GTARSKI3:23

for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct

for a, b, c, d being POINT of S st between4 a,b,c,d holds

( between a,b,c & between a,b,d & between a,c,d & between b,c,d ) ;

for a, b, c, d being POINT of S st between4 a,b,c,d holds

( between a,b,c & between a,b,d & between a,c,d & between b,c,d ) ;

theorem :: GTARSKI3:24

for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct

for a, b, c, d, e being POINT of S st between5 a,b,c,d,e holds

( between a,b,c & between a,b,d & between a,b,e & between a,c,d & between a,c,e & between a,d,e & between b,c,d & between b,c,e & between b,d,e & between c,d,e & between4 a,b,c,d & between4 a,b,c,e & between4 a,c,d,e & between4 b,c,d,e ) ;

for a, b, c, d, e being POINT of S st between5 a,b,c,d,e holds

( between a,b,c & between a,b,d & between a,b,e & between a,c,d & between a,c,e & between a,d,e & between b,c,d & between b,c,e & between b,d,e & between c,d,e & between4 a,b,c,d & between4 a,b,c,e & between4 a,c,d,e & between4 b,c,d,e ) ;

theorem :: GTARSKI3:25

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, p being POINT of S st between a,b,c & between a,p,b holds

between4 a,p,b,c by Satz3p6p1, Satz3p6p2;

for a, b, c, p being POINT of S st between a,b,c & between a,p,b holds

between4 a,p,b,c by Satz3p6p1, Satz3p6p2;

theorem Satz3p11p3pb: :: GTARSKI3:26

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, p being POINT of S st between a,b,c & between b,p,c holds

between4 a,b,p,c by Satz3p5p1, Satz3p5p2;

for a, b, c, p being POINT of S st between a,b,c & between b,p,c holds

between4 a,b,p,c by Satz3p5p1, Satz3p5p2;

theorem :: GTARSKI3:27

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, d, p being POINT of S st between4 a,b,c,d & between a,p,b holds

between5 a,p,b,c,d

for a, b, c, d, p being POINT of S st between4 a,b,c,d & between a,p,b holds

between5 a,p,b,c,d

proof end;

theorem Satz3p11p4pb: :: GTARSKI3:28

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, d, p being POINT of S st between4 a,b,c,d & between b,p,c holds

between5 a,b,p,c,d

for a, b, c, d, p being POINT of S st between4 a,b,c,d & between b,p,c holds

between5 a,b,p,c,d

proof end;

theorem :: GTARSKI3:29

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, d, p being POINT of S st between4 a,b,c,d & between c,p,d holds

between5 a,b,c,p,d

for a, b, c, d, p being POINT of S st between4 a,b,c,d & between c,p,d holds

between5 a,b,c,p,d

proof end;

theorem :: GTARSKI3:30

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, p being POINT of S st between a,b,c & between a,c,p holds

( between4 a,b,c,p & ( a <> c implies between4 a,b,c,p ) ) by Satz3p6p1, Satz3p6p2;

for a, b, c, p being POINT of S st between a,b,c & between a,c,p holds

( between4 a,b,c,p & ( a <> c implies between4 a,b,c,p ) ) by Satz3p6p1, Satz3p6p2;

theorem :: GTARSKI3:31

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, p being POINT of S st between a,b,c & between b,c,p holds

( between b,c,p & ( b <> c implies between4 a,b,c,p ) ) by Satz3p7p1, Satz3p7p2;

for a, b, c, p being POINT of S st between a,b,c & between b,c,p holds

( between b,c,p & ( b <> c implies between4 a,b,c,p ) ) by Satz3p7p1, Satz3p7p2;

theorem :: GTARSKI3:32

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, d, p being POINT of S st between4 a,b,c,d & between a,d,p holds

( between5 a,b,c,d,p & ( a <> d implies between5 a,b,c,d,p ) )

for a, b, c, d, p being POINT of S st between4 a,b,c,d & between a,d,p holds

( between5 a,b,c,d,p & ( a <> d implies between5 a,b,c,d,p ) )

proof end;

theorem :: GTARSKI3:33

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, d, p being POINT of S st between4 a,b,c,d & between b,d,p holds

( between4 b,c,d,p & ( b <> d implies between5 a,b,c,d,p ) )

for a, b, c, d, p being POINT of S st between4 a,b,c,d & between b,d,p holds

( between4 b,c,d,p & ( b <> d implies between5 a,b,c,d,p ) )

proof end;

theorem :: GTARSKI3:34

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, d, p being POINT of S st between4 a,b,c,d & between c,d,p holds

( between c,d,p & ( c <> d implies between5 a,b,c,d,p ) )

for a, b, c, d, p being POINT of S st between4 a,b,c,d & between c,d,p holds

( between c,d,p & ( c <> d implies between5 a,b,c,d,p ) )

proof end;

registration

ex b_{1} being satisfying_Tarski-model TarskiGeometryStruct st b_{1} is satisfying_Lower_Dimension_Axiom
end;

cluster satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity satisfying_Pasch satisfying_Tarski-model satisfying_Lower_Dimension_Axiom satisfying_SST_A5 for TarskiGeometryStruct ;

existence ex b

proof end;

:: 3.13 Satz

theorem Satz3p13: :: GTARSKI3:35

for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ex a, b, c being POINT of S st

( not between a,b,c & not between b,c,a & not between c,a,b & a <> b & b <> c & c <> a )

( not between a,b,c & not between b,c,a & not between c,a,b & a <> b & b <> c & c <> a )

proof end;

:: 3.14 Satz

theorem Satz3p14: :: GTARSKI3:36

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_Lower_Dimension_Axiom TarskiGeometryStruct

for a, b being POINT of S ex c being POINT of S st

( between a,b,c & b <> c )

for a, b being POINT of S ex c being POINT of S st

( between a,b,c & b <> c )

proof end;

theorem Satz3p15p3: :: GTARSKI3:37

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Lower_Dimension_Axiom TarskiGeometryStruct

for a1, a2 being POINT of S st a1 <> a2 holds

ex a3 being POINT of S st

( between a1,a2,a3 & a1,a2,a3 are_mutually_distinct )

for a1, a2 being POINT of S st a1 <> a2 holds

ex a3 being POINT of S st

( between a1,a2,a3 & a1,a2,a3 are_mutually_distinct )

proof end;

theorem Satz3p15p4: :: GTARSKI3:38

for S being satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct

for a1, a2 being POINT of S st a1 <> a2 holds

ex a3, a4 being POINT of S st

( between4 a1,a2,a3,a4 & a1,a2,a3,a4 are_mutually_distinct )

for a1, a2 being POINT of S st a1 <> a2 holds

ex a3, a4 being POINT of S st

( between4 a1,a2,a3,a4 & a1,a2,a3,a4 are_mutually_distinct )

proof end;

theorem :: GTARSKI3:39

for S being satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct

for a1, a2 being POINT of S st a1 <> a2 holds

ex a3, a4, a5 being POINT of S st

( between5 a1,a2,a3,a4,a5 & a1,a2,a3,a4,a5 are_mutually_distinct )

for a1, a2 being POINT of S st a1 <> a2 holds

ex a3, a4, a5 being POINT of S st

( between5 a1,a2,a3,a4,a5 & a1,a2,a3,a4,a5 are_mutually_distinct )

proof end;

:: 3.17 Satz

theorem Satz3p17: :: GTARSKI3:40

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, p, a9, b9, c9 being POINT of S st between a,b,c & between a9,b9,c & between a,p,a9 holds

ex q being POINT of S st

( between p,q,c & between b,q,b9 )

for a, b, c, p, a9, b9, c9 being POINT of S st between a,b,c & between a9,b9,c & between a,p,a9 holds

ex q being POINT of S st

( between p,q,c & between b,q,b9 )

proof end;

:: deftheorem defines IFS GTARSKI3:def 5 :

for S being TarskiGeometryStruct

for a, b, c, d, a9, b9, c9, d9 being POINT of S holds

( a,b,c,d IFS a9,b9,c9,d9 iff ( between a,b,c & between a9,b9,c9 & a,c equiv a9,c9 & b,c equiv b9,c9 & a,d equiv a9,d9 & c,d equiv c9,d9 ) );

for S being TarskiGeometryStruct

for a, b, c, d, a9, b9, c9, d9 being POINT of S holds

( a,b,c,d IFS a9,b9,c9,d9 iff ( between a,b,c & between a9,b9,c9 & a,c equiv a9,c9 & b,c equiv b9,c9 & a,d equiv a9,d9 & c,d equiv c9,d9 ) );

:: 4.2 Satz

theorem Satz4p2: :: GTARSKI3:41

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, d, a9, b9, c9, d9 being POINT of S st a,b,c,d IFS a9,b9,c9,d9 holds

b,d equiv b9,d9

for a, b, c, d, a9, b9, c9, d9 being POINT of S st a,b,c,d IFS a9,b9,c9,d9 holds

b,d equiv b9,d9

proof end;

:: 4.3 Satz

theorem Satz4p3: :: GTARSKI3:42

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, a9, b9, c9 being POINT of S st between a,b,c & between a9,b9,c9 & a,c equiv a9,c9 & b,c equiv b9,c9 holds

a,b equiv a9,b9

for a, b, c, a9, b9, c9 being POINT of S st between a,b,c & between a9,b9,c9 & a,c equiv a9,c9 & b,c equiv b9,c9 holds

a,b equiv a9,b9

proof end;

:: 4.5 Satz

theorem Satz4p5: :: GTARSKI3:43

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, a9, c9 being POINT of S st between a,b,c & a,c equiv a9,c9 holds

ex b9 being POINT of S st

( between a9,b9,c9 & a,b,c cong a9,b9,c9 )

for a, b, c, a9, c9 being POINT of S st between a,b,c & a,c equiv a9,c9 holds

ex b9 being POINT of S st

( between a9,b9,c9 & a,b,c cong a9,b9,c9 )

proof end;

:: 4.6 Satz

theorem Satz4p6: :: GTARSKI3:44

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, a9, b9, c9 being POINT of S st between a,b,c & a,b,c cong a9,b9,c9 holds

between a9,b9,c9

for a, b, c, a9, b9, c9 being POINT of S st between a,b,c & a,b,c cong a9,b9,c9 holds

between a9,b9,c9

proof end;

:: 4.11 Satz

theorem :: GTARSKI3:45

for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct

for a, b, c being POINT of S st Collinear a,b,c holds

( Collinear b,c,a & Collinear c,a,b & Collinear c,b,a & Collinear b,a,c & Collinear a,c,b ) by Satz3p2;

for a, b, c being POINT of S st Collinear a,b,c holds

( Collinear b,c,a & Collinear c,a,b & Collinear c,b,a & Collinear b,a,c & Collinear a,c,b ) by Satz3p2;

:: 4.12 Sazz

theorem :: GTARSKI3:46

for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction TarskiGeometryStruct

for a, b being POINT of S holds Collinear a,a,b by Satz3p1;

for a, b being POINT of S holds Collinear a,a,b by Satz3p1;

theorem Lm4p13p1: :: GTARSKI3:47

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct

for a, b, c, a9, b9, c9 being POINT of S st a,b,c cong a9,b9,c9 holds

b,c,a cong b9,c9,a9

for a, b, c, a9, b9, c9 being POINT of S st a,b,c cong a9,b9,c9 holds

b,c,a cong b9,c9,a9

proof end;

:: 4.13 Satz

theorem Satz4p13: :: GTARSKI3:48

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, a9, b9, c9 being POINT of S st Collinear a,b,c & a,b,c cong a9,b9,c9 holds

Collinear a9,b9,c9

for a, b, c, a9, b9, c9 being POINT of S st Collinear a,b,c & a,b,c cong a9,b9,c9 holds

Collinear a9,b9,c9

proof end;

theorem Lm4p14p1: :: GTARSKI3:49

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct

for a, b, c, a9, b9, c9 being POINT of S st b,a,c cong b9,a9,c9 holds

a,b,c cong a9,b9,c9

for a, b, c, a9, b9, c9 being POINT of S st b,a,c cong b9,a9,c9 holds

a,b,c cong a9,b9,c9

proof end;

theorem Lm4p14p2: :: GTARSKI3:50

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct

for a, b, c, a9, b9, c9 being POINT of S st a,c,b cong a9,c9,b9 holds

a,b,c cong a9,b9,c9

for a, b, c, a9, b9, c9 being POINT of S st a,c,b cong a9,c9,b9 holds

a,b,c cong a9,b9,c9

proof end;

:: 4.14 Satz

theorem Satz4p14: :: GTARSKI3:51

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, a9, b9 being POINT of S st Collinear a,b,c & a,b equiv a9,b9 holds

ex c9 being POINT of S st a,b,c cong a9,b9,c9

for a, b, c, a9, b9 being POINT of S st Collinear a,b,c & a,b equiv a9,b9 holds

ex c9 being POINT of S st a,b,c cong a9,b9,c9

proof end;

:: deftheorem defines FS GTARSKI3:def 6 :

for S being TarskiGeometryStruct

for a, b, c, d, a9, b9, c9, d9 being POINT of S holds

( a,b,c,d FS a9,b9,c9,d9 iff ( Collinear a,b,c & a,b,c cong a9,b9,c9 & a,d equiv a9,d9 & b,d equiv b9,d9 ) );

for S being TarskiGeometryStruct

for a, b, c, d, a9, b9, c9, d9 being POINT of S holds

( a,b,c,d FS a9,b9,c9,d9 iff ( Collinear a,b,c & a,b,c cong a9,b9,c9 & a,d equiv a9,d9 & b,d equiv b9,d9 ) );

:: 4.16 Satz

theorem Satz4p16: :: GTARSKI3:52

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, d, a9, b9, c9, d9 being POINT of S st a,b,c,d FS a9,b9,c9,d9 & a <> b holds

c,d equiv c9,d9

for a, b, c, d, a9, b9, c9, d9 being POINT of S st a,b,c,d FS a9,b9,c9,d9 & a <> b holds

c,d equiv c9,d9

proof end;

:: 4.17 Satz

theorem Satz4p17: :: GTARSKI3:53

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, p, q being POINT of S st a <> b & Collinear a,b,c & a,p equiv a,q & b,p equiv b,q holds

c,p equiv c,q

for a, b, c, p, q being POINT of S st a <> b & Collinear a,b,c & a,p equiv a,q & b,p equiv b,q holds

c,p equiv c,q

proof end;

:: 4.18 Satz

theorem Satz4p18: :: GTARSKI3:54

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, c9 being POINT of S st a <> b & Collinear a,b,c & a,c equiv a,c9 & b,c equiv b,c9 holds

c = c9

for a, b, c, c9 being POINT of S st a <> b & Collinear a,b,c & a,c equiv a,c9 & b,c equiv b,c9 holds

c = c9

proof end;

:: 4.19 Satz

theorem Satz4p19: :: GTARSKI3:55

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, c9 being POINT of S st between a,c,b & a,c equiv a,c9 & b,c equiv b,c9 holds

c = c9

for a, b, c, c9 being POINT of S st between a,c,b & a,c equiv a,c9 & b,c equiv b,c9 holds

c = c9

proof end;

:: 5.1 Satz

theorem Satz5p1: :: GTARSKI3:56

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, d being POINT of S st a <> b & between a,b,c & between a,b,d & not between a,c,d holds

between a,d,c

for a, b, c, d being POINT of S st a <> b & between a,b,c & between a,b,d & not between a,c,d holds

between a,d,c

proof end;

:: 5.2 Satz

theorem Satz5p2: :: GTARSKI3:57

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, d being POINT of S st a <> b & between a,b,c & between a,b,d & not between b,c,d holds

between b,d,c

for a, b, c, d being POINT of S st a <> b & between a,b,c & between a,b,d & not between b,c,d holds

between b,d,c

proof end;

:: 5.3 Satz

theorem Satz5p3: :: GTARSKI3:58

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, d being POINT of S st between a,b,d & between a,c,d & not between a,b,c holds

between a,c,b

for a, b, c, d being POINT of S st between a,b,d & between a,c,d & not between a,b,c holds

between a,c,b

proof end;

:: deftheorem defines <= GTARSKI3:def 7 :

for S being TarskiGeometryStruct

for a, b, c, d being POINT of S holds

( a,b <= c,d iff ex y being POINT of S st

( between c,y,d & a,b equiv c,y ) );

for S being TarskiGeometryStruct

for a, b, c, d being POINT of S holds

( a,b <= c,d iff ex y being POINT of S st

( between c,y,d & a,b equiv c,y ) );

:: 5.5 Satz

theorem Satz5p5: :: GTARSKI3:59

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, d being POINT of S holds

( a,b <= c,d iff ex x being POINT of S st

( between a,b,x & a,x equiv c,d ) )

for a, b, c, d being POINT of S holds

( a,b <= c,d iff ex x being POINT of S st

( between a,b,x & a,x equiv c,d ) )

proof end;

:: 5.6 Satz

theorem Satz5p6: :: GTARSKI3:60

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, d, a9, b9, c9, d9 being POINT of S st a,b <= c,d & a,b equiv a9,b9 & c,d equiv c9,d9 holds

a9,b9 <= c9,d9

for a, b, c, d, a9, b9, c9, d9 being POINT of S st a,b <= c,d & a,b equiv a9,b9 & c,d equiv c9,d9 holds

a9,b9 <= c9,d9

proof end;

:: 5.7 Satz

:: 5.8 Satz

theorem :: GTARSKI3:62

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, d, e, f being POINT of S st a,b <= c,d & c,d <= e,f holds

a,b <= e,f

for a, b, c, d, e, f being POINT of S st a,b <= c,d & c,d <= e,f holds

a,b <= e,f

proof end;

:: 5.9 Satz

theorem :: GTARSKI3:63

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, d being POINT of S st a,b <= c,d & c,d <= a,b holds

a,b equiv c,d

for a, b, c, d being POINT of S st a,b <= c,d & c,d <= a,b holds

a,b equiv c,d

proof end;

:: 5.10 Satz

theorem Satz5p10: :: GTARSKI3:64

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, d being POINT of S holds

( a,b <= c,d or c,d <= a,b )

for a, b, c, d being POINT of S holds

( a,b <= c,d or c,d <= a,b )

proof end;

:: 5.11 Satz

theorem :: GTARSKI3:65

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c being POINT of S holds a,a <= b,c

for a, b, c being POINT of S holds a,a <= b,c

proof end;

:: 5.12 Lemma 1

theorem :: GTARSKI3:66

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct

for a, b, c, d being POINT of S st a,b <= c,d holds

b,a <= c,d by Satz2p4;

for a, b, c, d being POINT of S st a,b <= c,d holds

b,a <= c,d by Satz2p4;

:: 5.12 Lemma 2

theorem Lemma5p12p2: :: GTARSKI3:67

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, d being POINT of S st a,b <= c,d holds

a,b <= d,c

for a, b, c, d being POINT of S st a,b <= c,d holds

a,b <= d,c

proof end;

:: 5.12 Lemma 3

theorem Lemma5p12p3: :: GTARSKI3:68

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c being POINT of S st between a,b,c & a,c equiv a,b holds

c = b

for a, b, c being POINT of S st between a,b,c & a,c equiv a,b holds

c = b

proof end;

theorem Lemma5p12p4: :: GTARSKI3:69

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c being POINT of S st between a,c,b & a,b <= a,c holds

b = c

for a, b, c being POINT of S st between a,c,b & a,b <= a,c holds

b = c

proof end;

:: 5.12 Satz

theorem Satz5p12: :: GTARSKI3:70

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c being POINT of S st Collinear a,b,c holds

( between a,b,c iff ( a,b <= a,c & b,c <= a,c ) )

for a, b, c being POINT of S st Collinear a,b,c holds

( between a,b,c iff ( a,b <= a,c & b,c <= a,c ) )

proof end;

:: deftheorem defines out GTARSKI3:def 8 :

for S being TarskiGeometryStruct

for a, b, p being POINT of S holds

( p out a,b iff ( p <> a & p <> b & ( between p,a,b or between p,b,a ) ) );

for S being TarskiGeometryStruct

for a, b, p being POINT of S holds

( p out a,b iff ( p <> a & p <> b & ( between p,a,b or between p,b,a ) ) );

:: 6.2 Satz

theorem Satz6p2: :: GTARSKI3:71

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, p being POINT of S st a <> p & b <> p & c <> p & between a,p,c holds

( between b,p,c iff p out a,b )

for a, b, c, p being POINT of S st a <> p & b <> p & c <> p & between a,p,c holds

( between b,p,c iff p out a,b )

proof end;

:: 6.3 Satz

theorem Satz6p3: :: GTARSKI3:72

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, p being POINT of S holds

( p out a,b iff ( a <> p & b <> p & ex c being POINT of S st

( c <> p & between a,p,c & between b,p,c ) ) )

for a, b, p being POINT of S holds

( p out a,b iff ( a <> p & b <> p & ex c being POINT of S st

( c <> p & between a,p,c & between b,p,c ) ) )

proof end;

:: 6.4 Satz

theorem :: GTARSKI3:73

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, p being POINT of S holds

( p out a,b iff ( Collinear a,p,b & not between a,p,b ) )

for a, b, p being POINT of S holds

( p out a,b iff ( Collinear a,p,b & not between a,p,b ) )

proof end;

:: 6.5 Satz

theorem :: GTARSKI3:74

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, p being POINT of S st a <> p holds

p out a,a by Satz3p1;

for a, p being POINT of S st a <> p holds

p out a,a by Satz3p1;

:: 6.6 Satz

theorem :: GTARSKI3:75

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, p being POINT of S st p out a,b holds

p out b,a ;

for a, b, p being POINT of S st p out a,b holds

p out b,a ;

:: 6.7 Satz

theorem :: GTARSKI3:76

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, p being POINT of S st p out a,b & p out b,c holds

p out a,c by Satz3p6p2, Satz5p3, Satz5p1;

for a, b, c, p being POINT of S st p out a,b & p out b,c holds

p out a,c by Satz3p6p2, Satz5p3, Satz5p1;

theorem Lemmapsegcon2: :: GTARSKI3:77

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, p being POINT of S ex x being POINT of S st

( ( between p,a,x or between p,x,a ) & p,x equiv b,c )

for a, b, c, p being POINT of S ex x being POINT of S st

( ( between p,a,x or between p,x,a ) & p,x equiv b,c )

proof end;

:: 6.11 Satz a)

theorem :: GTARSKI3:78

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, r being POINT of S st r <> a & b <> c holds

ex x being POINT of S st

( a out x,r & a,x equiv b,c )

for a, b, c, r being POINT of S st r <> a & b <> c holds

ex x being POINT of S st

( a out x,r & a,x equiv b,c )

proof end;

definition

let S be TarskiGeometryStruct ;

let a, p be POINT of S;

coherence

{ x where x is POINT of S : p out x,a } is set ;

end;
let a, p be POINT of S;

coherence

{ x where x is POINT of S : p out x,a } is set ;

:: deftheorem defines halfline GTARSKI3:def 9 :

for S being TarskiGeometryStruct

for a, p being POINT of S holds halfline (p,a) = { x where x is POINT of S : p out x,a } ;

for S being TarskiGeometryStruct

for a, p being POINT of S holds halfline (p,a) = { x where x is POINT of S : p out x,a } ;

:: 6.11 Satz b)

theorem Satz6p11pb: :: GTARSKI3:79

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, r, x, y being POINT of S st r <> a & b <> c & a out x,r & a,x equiv b,c & a out y,r & a,y equiv b,c holds

x = y

for a, b, c, r, x, y being POINT of S st r <> a & b <> c & a out x,r & a,x equiv b,c & a out y,r & a,y equiv b,c holds

x = y

proof end;

:: 6.13 Satz

theorem Satz6p13: :: GTARSKI3:80

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, p being POINT of S st p out a,b holds

( p,a <= p,b iff between p,a,b )

for a, b, p being POINT of S st p out a,b holds

( p,a <= p,b iff between p,a,b )

proof end;

definition

let S be non empty TarskiGeometryStruct ;

let p, q be POINT of S;

{ x where x is POINT of S : Collinear p,q,x } is Subset of S

end;
let p, q be POINT of S;

func Line (p,q) -> Subset of S equals :: GTARSKI3:def 10

{ x where x is POINT of S : Collinear p,q,x } ;

coherence { x where x is POINT of S : Collinear p,q,x } ;

{ x where x is POINT of S : Collinear p,q,x } is Subset of S

proof end;

:: deftheorem defines Line GTARSKI3:def 10 :

for S being non empty TarskiGeometryStruct

for p, q being POINT of S holds Line (p,q) = { x where x is POINT of S : Collinear p,q,x } ;

for S being non empty TarskiGeometryStruct

for p, q being POINT of S holds Line (p,q) = { x where x is POINT of S : Collinear p,q,x } ;

:: 6.15 Satz

theorem :: GTARSKI3:81

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for p, q, r being POINT of S st p <> q & p <> r & between q,p,r holds

Line (p,q) = ((halfline (p,q)) \/ {p}) \/ (halfline (p,r))

for p, q, r being POINT of S st p <> q & p <> r & between q,p,r holds

Line (p,q) = ((halfline (p,q)) \/ {p}) \/ (halfline (p,r))

proof end;

:: deftheorem defines is_line GTARSKI3:def 11 :

for S being non empty TarskiGeometryStruct

for A being Subset of S holds

( A is_line iff ex p, q being POINT of S st

( p <> q & A = Line (p,q) ) );

for S being non empty TarskiGeometryStruct

for A being Subset of S holds

( A is_line iff ex p, q being POINT of S st

( p <> q & A = Line (p,q) ) );

:: 6.16 Satz

theorem :: GTARSKI3:82

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for p, q, s being POINT of S st p <> q & s <> p & s in Line (p,q) holds

Line (p,q) = Line (p,s)

for p, q, s being POINT of S st p <> q & s <> p & s in Line (p,q) holds

Line (p,q) = Line (p,s)

proof end;

:: 6.17 Satz

theorem Satz6p17: :: GTARSKI3:83

for S being non empty satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct

for p, q being POINT of S holds

( p in Line (p,q) & q in Line (p,q) & Line (p,q) = Line (q,p) )

for p, q being POINT of S holds

( p in Line (p,q) & q in Line (p,q) & Line (p,q) = Line (q,p) )

proof end;

theorem Thequiv1: :: GTARSKI3:84

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c being Element of S holds

( ( a <> b & Collinear a,b,c ) iff c on_line a,b ) ;

for a, b, c being Element of S holds

( ( a <> b & Collinear a,b,c ) iff c on_line a,b ) ;

theorem Thequiv2: :: GTARSKI3:85

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for a, b, x, y being POINT of S st a,b equal_line x,y holds

Line (a,b) = Line (x,y)

for a, b, x, y being POINT of S st a,b equal_line x,y holds

Line (a,b) = Line (x,y)

proof end;

theorem :: GTARSKI3:86

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for a, b, x, y being POINT of S st a <> b & x <> y & Line (a,b) = Line (x,y) holds

a,b equal_line x,y

for a, b, x, y being POINT of S st a <> b & x <> y & Line (a,b) = Line (x,y) holds

a,b equal_line x,y

proof end;

:: 6.18 Satz

theorem Satz6p18: :: GTARSKI3:87

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for A being Subset of S

for a, b being POINT of S st A is_line & a <> b & a in A & b in A holds

A = Line (a,b)

for A being Subset of S

for a, b being POINT of S st A is_line & a <> b & a in A & b in A holds

A = Line (a,b)

proof end;

:: 6.19 Satz

theorem Satz6p19: :: GTARSKI3:88

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for A, B being Subset of S

for a, b being POINT of S st a <> b & A is_line & a in A & b in A & B is_line & a in B & b in B holds

A = B

for A, B being Subset of S

for a, b being POINT of S st a <> b & A is_line & a in A & b in A & B is_line & a in B & b in B holds

A = B

proof end;

:: 6.21 Satz

theorem :: GTARSKI3:89

:: 6.23 Satz

theorem :: GTARSKI3:90

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for a, b, c being POINT of S st ex p, q being POINT of S st p <> q holds

( Collinear a,b,c iff ex A being Subset of S st

( A is_line & a in A & b in A & c in A ) )

for a, b, c being POINT of S st ex p, q being POINT of S st p <> q holds

( Collinear a,b,c iff ex A being Subset of S st

( A is_line & a in A & b in A & c in A ) )

proof end;

:: 6.24 Satz

theorem Satz6p24: :: GTARSKI3:91

for S being satisfying_A8 TarskiGeometryStruct holds

not for a, b, c being POINT of S holds Collinear a,b,c

not for a, b, c being POINT of S holds Collinear a,b,c

proof end;

:: 6.25 Satz

theorem :: GTARSKI3:92

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for a, b being POINT of S st S is satisfying_A8 & a <> b holds

ex c being POINT of S st not Collinear a,b,c

for a, b being POINT of S st S is satisfying_A8 & a <> b holds

ex c being POINT of S st not Collinear a,b,c

proof end;

theorem Satz6p28Lem01: :: GTARSKI3:93

for S being satisfying_Tarski-model TarskiGeometryStruct

for p, a, b being POINT of S st p out a,b & p,a <= p,b holds

between p,a,b by Satz6p13;

for p, a, b being POINT of S st p out a,b & p,a <= p,b holds

between p,a,b by Satz6p13;

theorem Satz6p28Lem02: :: GTARSKI3:94

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, d, e, f, g, h being Element of S st not c,d <= a,b & a,b equiv e,f & c,d equiv g,h holds

e,f <= g,h

for a, b, c, d, e, f, g, h being Element of S st not c,d <= a,b & a,b equiv e,f & c,d equiv g,h holds

e,f <= g,h

proof end;

theorem :: GTARSKI3:95

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, a1, b1, c1 being Element of S st b out a,c & b1 out a1,c1 & b,a equiv b1,a1 & b,c equiv b1,c1 holds

a,c equiv a1,c1

for a, b, c, a1, b1, c1 being Element of S st b out a,c & b1 out a1,c1 & b,a equiv b1,a1 & b,c equiv b1,c1 holds

a,c equiv a1,c1

proof end;

:: deftheorem DEFM defines Middle GTARSKI3:def 12 :

for S being TarskiGeometryStruct

for a, b, m being POINT of S holds

( Middle a,m,b iff ( between a,m,b & m,a equiv m,b ) );

for S being TarskiGeometryStruct

for a, b, m being POINT of S holds

( Middle a,m,b iff ( between a,m,b & m,a equiv m,b ) );

:: 7.2 Satz

theorem :: GTARSKI3:96

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct

for a, b, m being POINT of S st Middle a,m,b holds

Middle b,m,a by Satz3p2, Satz2p2;

for a, b, m being POINT of S st Middle a,m,b holds

Middle b,m,a by Satz3p2, Satz2p2;

:: 7.3 Satz

theorem Satz7p3: :: GTARSKI3:97

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity TarskiGeometryStruct

for a, m being POINT of S holds

( Middle a,m,a iff m = a ) by GTARSKI1:def 10, Satz3p1, Satz2p1;

for a, m being POINT of S holds

( Middle a,m,a iff m = a ) by GTARSKI1:def 10, Satz3p1, Satz2p1;

theorem Satz7p4existence: :: GTARSKI3:98

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity TarskiGeometryStruct

for a, p being POINT of S ex p9 being POINT of S st Middle p,a,p9

for a, p being POINT of S ex p9 being POINT of S st Middle p,a,p9

proof end;

theorem Satz7p4uniqueness: :: GTARSKI3:99

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS TarskiGeometryStruct

for a, p, p1, p2 being POINT of S st Middle p,a,p1 & Middle p,a,p2 holds

p1 = p2

for a, p, p1, p2 being POINT of S st Middle p,a,p1 & Middle p,a,p2 holds

p1 = p2

proof end;

definition

let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity TarskiGeometryStruct ;

let a, p be POINT of S;

existence

ex b_{1} being POINT of S st Middle p,a,b_{1}
by Satz7p4existence;

uniqueness

for b_{1}, b_{2} being POINT of S st Middle p,a,b_{1} & Middle p,a,b_{2} holds

b_{1} = b_{2}
by Satz7p4uniqueness;

end;
let a, p be POINT of S;

existence

ex b

uniqueness

for b

b

:: deftheorem DEFR defines reflection GTARSKI3:def 13 :

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity TarskiGeometryStruct

for a, p, b_{4} being POINT of S holds

( b_{4} = reflection (a,p) iff Middle p,a,b_{4} );

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity TarskiGeometryStruct

for a, p, b

( b

:: 7.6 Satz

theorem :: GTARSKI3:100

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity TarskiGeometryStruct

for a, p, p9 being POINT of S holds

( reflection (a,p) = p9 iff Middle p,a,p9 ) by DEFR;

for a, p, p9 being POINT of S holds

( reflection (a,p) = p9 iff Middle p,a,p9 ) by DEFR;

:: 7.7 Satz

theorem Satz7p7: :: GTARSKI3:101

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct

for a, p being POINT of S holds reflection (a,(reflection (a,p))) = p

for a, p being POINT of S holds reflection (a,(reflection (a,p))) = p

proof end;

:: 7.8 Satz

theorem :: GTARSKI3:102

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct

for a, p9 being POINT of S ex p being POINT of S st reflection (a,p) = p9

for a, p9 being POINT of S ex p being POINT of S st reflection (a,p) = p9

proof end;

:: 7.9 Satz

theorem Satz7p9: :: GTARSKI3:103

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct

for a, p, p9 being POINT of S st reflection (a,p) = reflection (a,p9) holds

p = p9

for a, p, p9 being POINT of S st reflection (a,p) = reflection (a,p9) holds

p = p9

proof end;

:: 7.10 Satz

theorem Satz7p10: :: GTARSKI3:104

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity TarskiGeometryStruct

for a, p being POINT of S holds

( reflection (a,p) = p iff p = a )

for a, p being POINT of S holds

( reflection (a,p) = p iff p = a )

proof end;

:: 7.13 Satz

theorem Satz7p13: :: GTARSKI3:105

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, p, q being POINT of S holds p,q equiv reflection (a,p), reflection (a,q)

for a, p, q being POINT of S holds p,q equiv reflection (a,p), reflection (a,q)

proof end;

Lemma7p15a: for S being satisfying_Tarski-model TarskiGeometryStruct

for a, p, q, r being POINT of S st between p,q,r holds

between reflection (a,p), reflection (a,q), reflection (a,r)

proof end;

:: 7.15 Satz

theorem Satz7p15: :: GTARSKI3:106

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, p, q, r being POINT of S holds

( between p,q,r iff between reflection (a,p), reflection (a,q), reflection (a,r) )

for a, p, q, r being POINT of S holds

( between p,q,r iff between reflection (a,p), reflection (a,q), reflection (a,r) )

proof end;

Lemma7p16a: for S being satisfying_Tarski-model TarskiGeometryStruct

for a, p, q, r, s being POINT of S st p,q equiv r,s holds

reflection (a,p), reflection (a,q) equiv reflection (a,r), reflection (a,s)

proof end;

:: 7.16 Satz

theorem Satz7p16: :: GTARSKI3:107

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, p, q, r, s being POINT of S holds

( p,q equiv r,s iff reflection (a,p), reflection (a,q) equiv reflection (a,r), reflection (a,s) )

for a, p, q, r, s being POINT of S holds

( p,q equiv r,s iff reflection (a,p), reflection (a,q) equiv reflection (a,r), reflection (a,s) )

proof end;

:: 7.17 Satz

theorem Satz7p17: :: GTARSKI3:108

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, p, p9 being POINT of S st Middle p,a,p9 & Middle p,b,p9 holds

a = b

for a, b, p, p9 being POINT of S st Middle p,a,p9 & Middle p,b,p9 holds

a = b

proof end;

:: 7.18 Satz

theorem :: GTARSKI3:109

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, p being POINT of S st reflection (a,p) = reflection (b,p) holds

a = b

for a, b, p being POINT of S st reflection (a,p) = reflection (b,p) holds

a = b

proof end;

:: 7.19 Satz

theorem :: GTARSKI3:110

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, p being POINT of S holds

( reflection (b,(reflection (a,p))) = reflection (a,(reflection (b,p))) iff a = b )

for a, b, p being POINT of S holds

( reflection (b,(reflection (a,p))) = reflection (a,(reflection (b,p))) iff a = b )

proof end;

:: 7.20 Satz

theorem Satz7p20: :: GTARSKI3:111

for S being satisfying_Tarski-model TarskiGeometryStruct

for a, b, m being POINT of S st Collinear a,m,b & m,a equiv m,b & not a = b holds

Middle a,m,b

for a, b, m being POINT of S st Collinear a,m,b & m,a equiv m,b & not a = b holds

Middle a,m,b

proof end;

:: 7.21 Satz

theorem :: GTARSKI3:112

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for a, b, c, d, p being POINT of S st not Collinear a,b,c & b <> d & a,b equiv c,d & b,c equiv d,a & Collinear a,p,c & Collinear b,p,d holds

( Middle a,p,c & Middle b,p,d )

for a, b, c, d, p being POINT of S st not Collinear a,b,c & b <> d & a,b equiv c,d & b,c equiv d,a & Collinear a,p,c & Collinear b,p,d holds

( Middle a,p,c & Middle b,p,d )

proof end;

theorem Satz7p22part1: :: GTARSKI3:113

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for c, a1, a2, b1, b2, m1, m2 being POINT of S st between a1,c,a2 & between b1,c,b2 & c,a1 equiv c,b1 & c,a2 equiv c,b2 & Middle a1,m1,b1 & Middle a2,m2,b2 & c,a1 <= c,a2 holds

between m1,c,m2

for c, a1, a2, b1, b2, m1, m2 being POINT of S st between a1,c,a2 & between b1,c,b2 & c,a1 equiv c,b1 & c,a2 equiv c,b2 & Middle a1,m1,b1 & Middle a2,m2,b2 & c,a1 <= c,a2 holds

between m1,c,m2

proof end;

theorem Satz7p22part2: :: GTARSKI3:114

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for c, a1, a2, b1, b2, m1, m2 being POINT of S st between a1,c,a2 & between b1,c,b2 & c,a1 equiv c,b1 & c,a2 equiv c,b2 & Middle a1,m1,b1 & Middle a2,m2,b2 & c,a2 <= c,a1 holds

between m1,c,m2

for c, a1, a2, b1, b2, m1, m2 being POINT of S st between a1,c,a2 & between b1,c,b2 & c,a1 equiv c,b1 & c,a2 equiv c,b2 & Middle a1,m1,b1 & Middle a2,m2,b2 & c,a2 <= c,a1 holds

between m1,c,m2

proof end;

theorem Satz7p22: :: GTARSKI3:115

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for c, a1, a2, b1, b2, m1, m2 being POINT of S st between a1,c,a2 & between b1,c,b2 & c,a1 equiv c,b1 & c,a2 equiv c,b2 & Middle a1,m1,b1 & Middle a2,m2,b2 holds

between m1,c,m2

for c, a1, a2, b1, b2, m1, m2 being POINT of S st between a1,c,a2 & between b1,c,b2 & c,a1 equiv c,b1 & c,a2 equiv c,b2 & Middle a1,m1,b1 & Middle a2,m2,b2 holds

between m1,c,m2

proof end;

definition

let S be TarskiGeometryStruct ;

let a1, a2, b1, b2, c, m1, m2 be POINT of S;

end;
let a1, a2, b1, b2, c, m1, m2 be POINT of S;

pred Krippenfigur a1,m1,b1,c,b2,m2,a2 means :: GTARSKI3:def 14

( between a1,c,a2 & between b1,c,b2 & c,a1 equiv c,b1 & c,a2 equiv c,b2 & Middle a1,m1,b1 & Middle a2,m2,b2 );

( between a1,c,a2 & between b1,c,b2 & c,a1 equiv c,b1 & c,a2 equiv c,b2 & Middle a1,m1,b1 & Middle a2,m2,b2 );

:: deftheorem defines Krippenfigur GTARSKI3:def 14 :

for S being TarskiGeometryStruct

for a1, a2, b1, b2, c, m1, m2 being POINT of S holds

( Krippenfigur a1,m1,b1,c,b2,m2,a2 iff ( between a1,c,a2 & between b1,c,b2 & c,a1 equiv c,b1 & c,a2 equiv c,b2 & Middle a1,m1,b1 & Middle a2,m2,b2 ) );

for S being TarskiGeometryStruct

for a1, a2, b1, b2, c, m1, m2 being POINT of S holds

( Krippenfigur a1,m1,b1,c,b2,m2,a2 iff ( between a1,c,a2 & between b1,c,b2 & c,a1 equiv c,b1 & c,a2 equiv c,b2 & Middle a1,m1,b1 & Middle a2,m2,b2 ) );

:: Krippenfigur

theorem :: GTARSKI3:116

for S being non empty satisfying_Tarski-model TarskiGeometryStruct

for c, a1, a2, b1, b2, m1, m2 being POINT of S st Krippenfigur a1,m1,b1,c,b2,m2,a2 holds

between m1,c,m2 by Satz7p22;

for c, a1, a2, b1, b2, m1, m2 being POINT of S st Krippenfigur a1,m1,b1,c,b2,m2,a2 holds

between m1,c,m2 by Satz7p22;

registration

not for b_{1} being satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct holds b_{1} is empty
by GTARSKI2:def 2;

end;

cluster non empty satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity satisfying_Pasch satisfying_Tarski-model satisfying_Lower_Dimension_Axiom satisfying_SST_A5 for TarskiGeometryStruct ;

existence not for b

::$ 7.25 Satz

theorem :: GTARSKI3:117

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct

for a, b, c being POINT of S st c,a equiv c,b holds

ex x being POINT of S st Middle a,x,b

for a, b, c being POINT of S st c,a equiv c,b holds

ex x being POINT of S st Middle a,x,b

proof end;

definition

let S be TarskiGeometryStruct ;

end;
attr S is (TE) means :: GTARSKI3:def 16

for a, b, p, q, r, s being POINT of S st a,b equiv p,q & a,b equiv r,s holds

p,q equiv r,s;

for a, b, p, q, r, s being POINT of S st a,b equiv p,q & a,b equiv r,s holds

p,q equiv r,s;

attr S is (SC) means :: GTARSKI3:def 18

for a, b, c, q being POINT of S ex x being POINT of S st

( between q,a,x & a,x equiv b,c );

for a, b, c, q being POINT of S ex x being POINT of S st

( between q,a,x & a,x equiv b,c );

attr S is (FS) means :: GTARSKI3:def 19

for a, b, c, d, a9, b9, c9, d9 being POINT of S st a <> b & between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 & a,d equiv a9,d9 & b,d equiv b9,d9 holds

c,d equiv c9,d9;

for a, b, c, d, a9, b9, c9, d9 being POINT of S st a <> b & between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 & a,d equiv a9,d9 & b,d equiv b9,d9 holds

c,d equiv c9,d9;

attr S is (Pa) means :: GTARSKI3:def 21

for a, b, c, p, q being POINT of S st between a,p,c & between b,q,c holds

ex x being POINT of S st

( between p,x,b & between q,x,a );

for a, b, c, p, q being POINT of S st between a,p,c & between b,q,c holds

ex x being POINT of S st

( between p,x,b & between q,x,a );

attr S is (Lo2) means :: GTARSKI3:def 22

ex a, b, c being POINT of S st

( not between a,b,c & not between b,c,a & not between c,a,b );

ex a, b, c being POINT of S st

( not between a,b,c & not between b,c,a & not between c,a,b );

attr S is (Up2) means :: GTARSKI3:def 23

for a, b, c, p, q being POINT of S st p <> q & a,p equiv a,q & b,p equiv b,q & c,p equiv c,q & not between a,b,c & not between b,c,a holds

between c,a,b;

for a, b, c, p, q being POINT of S st p <> q & a,p equiv a,q & b,p equiv b,q & c,p equiv c,q & not between a,b,c & not between b,c,a holds

between c,a,b;

attr S is (Eu) means :: GTARSKI3:def 24

for a, b, c, d, t being POINT of S st between a,d,t & between b,d,c & a <> d holds

ex x, y being POINT of S st

( between a,b,x & between a,c,y & between x,t,y );

for a, b, c, d, t being POINT of S st between a,d,t & between b,d,c & a <> d holds

ex x, y being POINT of S st

( between a,b,x & between a,c,y & between x,t,y );

:: deftheorem defines (RE) GTARSKI3:def 15 :

for S being TarskiGeometryStruct holds

( S is (RE) iff for a, b being POINT of S holds a,b equiv b,a );

for S being TarskiGeometryStruct holds

( S is (RE) iff for a, b being POINT of S holds a,b equiv b,a );

:: deftheorem defines (TE) GTARSKI3:def 16 :

for S being TarskiGeometryStruct holds

( S is (TE) iff for a, b, p, q, r, s being POINT of S st a,b equiv p,q & a,b equiv r,s holds

p,q equiv r,s );

for S being TarskiGeometryStruct holds

( S is (TE) iff for a, b, p, q, r, s being POINT of S st a,b equiv p,q & a,b equiv r,s holds

p,q equiv r,s );

:: deftheorem defines (IE) GTARSKI3:def 17 :

for S being TarskiGeometryStruct holds

( S is (IE) iff for a, b, c being POINT of S st a,b equiv c,c holds

a = b );

for S being TarskiGeometryStruct holds

( S is (IE) iff for a, b, c being POINT of S st a,b equiv c,c holds

a = b );

:: deftheorem defines (SC) GTARSKI3:def 18 :

for S being TarskiGeometryStruct holds

( S is (SC) iff for a, b, c, q being POINT of S ex x being POINT of S st

( between q,a,x & a,x equiv b,c ) );

for S being TarskiGeometryStruct holds

( S is (SC) iff for a, b, c, q being POINT of S ex x being POINT of S st

( between q,a,x & a,x equiv b,c ) );

:: deftheorem defines (FS) GTARSKI3:def 19 :

for S being TarskiGeometryStruct holds

( S is (FS) iff for a, b, c, d, a9, b9, c9, d9 being POINT of S st a <> b & between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 & a,d equiv a9,d9 & b,d equiv b9,d9 holds

c,d equiv c9,d9 );

for S being TarskiGeometryStruct holds

( S is (FS) iff for a, b, c, d, a9, b9, c9, d9 being POINT of S st a <> b & between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 & a,d equiv a9,d9 & b,d equiv b9,d9 holds

c,d equiv c9,d9 );

:: deftheorem defines (IB) GTARSKI3:def 20 :

for S being TarskiGeometryStruct holds

( S is (IB) iff for a, b being POINT of S st between a,b,a holds

a = b );

for S being TarskiGeometryStruct holds

( S is (IB) iff for a, b being POINT of S st between a,b,a holds

a = b );

:: deftheorem defines (Pa) GTARSKI3:def 21 :

for S being TarskiGeometryStruct holds

( S is (Pa) iff for a, b, c, p, q being POINT of S st between a,p,c & between b,q,c holds

ex x being POINT of S st

( between p,x,b & between q,x,a ) );

for S being TarskiGeometryStruct holds

( S is (Pa) iff for a, b, c, p, q being POINT of S st between a,p,c & between b,q,c holds

ex x being POINT of S st

( between p,x,b & between q,x,a ) );

:: deftheorem defines (Lo2) GTARSKI3:def 22 :

for S being TarskiGeometryStruct holds

( S is (Lo2) iff ex a, b, c being POINT of S st

( not between a,b,c & not between b,c,a & not between c,a,b ) );

for S being TarskiGeometryStruct holds

( S is (Lo2) iff ex a, b, c being POINT of S st

( not between a,b,c & not between b,c,a & not between c,a,b ) );

:: deftheorem defines (Up2) GTARSKI3:def 23 :

for S being TarskiGeometryStruct holds

( S is (Up2) iff for a, b, c, p, q being POINT of S st p <> q & a,p equiv a,q & b,p equiv b,q & c,p equiv c,q & not between a,b,c & not between b,c,a holds

between c,a,b );

for S being TarskiGeometryStruct holds

( S is (Up2) iff for a, b, c, p, q being POINT of S st p <> q & a,p equiv a,q & b,p equiv b,q & c,p equiv c,q & not between a,b,c & not between b,c,a holds

between c,a,b );

:: deftheorem defines (Eu) GTARSKI3:def 24 :

for S being TarskiGeometryStruct holds

( S is (Eu) iff for a, b, c, d, t being POINT of S st between a,d,t & between b,d,c & a <> d holds

ex x, y being POINT of S st

( between a,b,x & between a,c,y & between x,t,y ) );

for S being TarskiGeometryStruct holds

( S is (Eu) iff for a, b, c, d, t being POINT of S st between a,d,t & between b,d,c & a <> d holds

ex x, y being POINT of S st

( between a,b,x & between a,c,y & between x,t,y ) );

:: deftheorem defines (Co) GTARSKI3:def 25 :

for S being TarskiGeometryStruct holds

( S is (Co) iff for X, Y being set st ex a being POINT of S st

for x, y being POINT of S st x in X & y in Y holds

between a,x,y holds

ex b being POINT of S st

for x, y being POINT of S st x in X & y in Y holds

between x,b,y );

for S being TarskiGeometryStruct holds

( S is (Co) iff for X, Y being set st ex a being POINT of S st

for x, y being POINT of S st x in X & y in Y holds

between a,x,y holds

ex b being POINT of S st

for x, y being POINT of S st x in X & y in Y holds

between x,b,y );

:: deftheorem defines (FS') GTARSKI3:def 26 :

for S being TarskiGeometryStruct holds

( S is (FS') iff for a, b, c, d, a9, b9, c9, d9 being POINT of S st a <> b & between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 & a,d equiv a9,d9 & b,d equiv b9,d9 holds

d,c equiv c9,d9 );

for S being TarskiGeometryStruct holds

( S is (FS') iff for a, b, c, d, a9, b9, c9, d9 being POINT of S st a <> b & between a,b,c & between a9,b9,c9 & a,b equiv a9,b9 & b,c equiv b9,c9 & a,d equiv a9,d9 & b,d equiv b9,d9 holds

d,c equiv c9,d9 );

theorem :: GTARSKI3:118

theorem :: GTARSKI3:119

for S being TarskiGeometryStruct holds

( S is satisfying_CongruenceEquivalenceRelation iff S is (TE) ) ;

( S is satisfying_CongruenceEquivalenceRelation iff S is (TE) ) ;

theorem :: GTARSKI3:120

theorem :: GTARSKI3:121

theorem :: GTARSKI3:122

theorem :: GTARSKI3:123

theorem :: GTARSKI3:124

theorem :: GTARSKI3:125

theorem :: GTARSKI3:126

theorem :: GTARSKI3:127

for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct holds

( S is satisfying_SAS iff S is (FS) )

( S is satisfying_SAS iff S is (FS) )

proof end;

registration

coherence

for b_{1} being TarskiGeometryStruct st b_{1} is (RE) holds

b_{1} is satisfying_CongruenceSymmetry
;

coherence

for b_{1} being TarskiGeometryStruct st b_{1} is (TE) holds

b_{1} is satisfying_CongruenceEquivalenceRelation
;

coherence

for b_{1} being TarskiGeometryStruct st b_{1} is (IE) holds

b_{1} is satisfying_CongruenceIdentity
;

coherence

for b_{1} being TarskiGeometryStruct st b_{1} is (SC) holds

b_{1} is satisfying_SegmentConstruction
;

coherence

for b_{1} being TarskiGeometryStruct st b_{1} is (IB) holds

b_{1} is satisfying_BetweennessIdentity
;

coherence

for b_{1} being TarskiGeometryStruct st b_{1} is (Pa) holds

b_{1} is satisfying_Pasch
;

coherence

for b_{1} being TarskiGeometryStruct st b_{1} is (Lo2) holds

b_{1} is satisfying_Lower_Dimension_Axiom
;

coherence

for b_{1} being TarskiGeometryStruct st b_{1} is (Up2) holds

b_{1} is satisfying_Upper_Dimension_Axiom
;

coherence

for b_{1} being TarskiGeometryStruct st b_{1} is (Eu) holds

b_{1} is satisfying_Euclid_Axiom
;

coherence

for b_{1} being TarskiGeometryStruct st b_{1} is (Co) holds

b_{1} is satisfying_Continuity_Axiom
;

end;
for b

b

coherence

for b

b

coherence

for b

b

coherence

for b

b

coherence

for b

b

coherence

for b

b

coherence

for b

b

coherence

for b

b

coherence

for b

b

coherence

for b

b

registration

coherence

for b_{1} being TarskiGeometryStruct st b_{1} is satisfying_CongruenceSymmetry holds

b_{1} is (RE)
;

coherence

for b_{1} being TarskiGeometryStruct st b_{1} is satisfying_CongruenceEquivalenceRelation holds

b_{1} is (TE)
;

coherence

for b_{1} being TarskiGeometryStruct st b_{1} is satisfying_CongruenceIdentity holds

b_{1} is (IE)
;

coherence

for b_{1} being TarskiGeometryStruct st b_{1} is satisfying_SegmentConstruction holds

b_{1} is (SC)
;

coherence

for b_{1} being TarskiGeometryStruct st b_{1} is satisfying_BetweennessIdentity holds

b_{1} is (IB)
;

coherence

for b_{1} being TarskiGeometryStruct st b_{1} is satisfying_Pasch holds

b_{1} is (Pa)
;

coherence

for b_{1} being TarskiGeometryStruct st b_{1} is satisfying_Lower_Dimension_Axiom holds

b_{1} is (Lo2)
;

coherence

for b_{1} being TarskiGeometryStruct st b_{1} is satisfying_Upper_Dimension_Axiom holds

b_{1} is (Up2)
;

coherence

for b_{1} being TarskiGeometryStruct st b_{1} is satisfying_Euclid_Axiom holds

b_{1} is (Eu)
;

coherence

for b_{1} being non empty TarskiGeometryStruct st b_{1} is satisfying_Continuity_Axiom holds

b_{1} is (Co)
by ThMak1;

end;
for b

b

coherence

for b

b

coherence

for b

b

coherence

for b

b

coherence

for b

b

coherence

for b

b

coherence

for b

b

coherence

for b

b

coherence

for b

b

coherence

for b

b

registration
end;

registration

coherence

for b_{1} being (RE) (TE) TarskiGeometryStruct st b_{1} is (FS) holds

b_{1} is satisfying_SAS
by ThMak2;

end;
for b

b

registration

ex b_{1} being (RE) (TE) TarskiGeometryStruct st b_{1} is (FS)
end;

cluster satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation (RE) (TE) (FS) for TarskiGeometryStruct ;

existence ex b

proof end;

theorem :: GTARSKI3:131

registration

coherence

for b_{1} being (RE) (TE) TarskiGeometryStruct st b_{1} is (FS') holds

b_{1} is (FS)
by ThMak3;

end;
for b

b

registration
end;

registration

ex b_{1} being (RE) (TE) TarskiGeometryStruct st b_{1} is (FS')
end;

cluster satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation (RE) (TE) (FS') for TarskiGeometryStruct ;

existence ex b

proof end;

registration

ex b_{1} being (RE) (TE) (FS') TarskiGeometryStruct st b_{1} is (SC)
end;

cluster satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_SAS satisfying_SST_A5 (RE) (TE) (SC) (FS) (FS') for TarskiGeometryStruct ;

existence ex b

proof end;

theorem :: GTARSKI3:132

for S being (TE) (SC) TarskiGeometryStruct

for a, b being POINT of S holds a,b equiv a,b by Satz2p1bis;

for a, b being POINT of S holds a,b equiv a,b by Satz2p1bis;

theorem :: GTARSKI3:133

theorem :: GTARSKI3:134

for S being (TE) (SC) TarskiGeometryStruct

for a, b, c, d being POINT of S st a,b equiv c,d holds

c,d equiv a,b by Satz2p2bis;

for a, b, c, d being POINT of S st a,b equiv c,d holds

c,d equiv a,b by Satz2p2bis;

theorem ThMak4: :: GTARSKI3:135

for S being (TE) (SC) (FS') TarskiGeometryStruct

for a, b, c, d, e, f being POINT of S st a <> b & between b,a,c & between d,a,e & b,a equiv d,a & a,c equiv a,e & b,f equiv d,f holds

f,c equiv e,f

for a, b, c, d, e, f being POINT of S st a <> b & between b,a,c & between d,a,e & b,a equiv d,a & a,c equiv a,e & b,f equiv d,f holds

f,c equiv e,f

proof end;

:: deftheorem defines (RE') GTARSKI3:def 27 :

for S being TarskiGeometryStruct holds

( S is (RE') iff for a, b, c, d being POINT of S st a <> b & between b,a,c holds

d,c equiv c,d );

for S being TarskiGeometryStruct holds

( S is (RE') iff for a, b, c, d being POINT of S st a <> b & between b,a,c holds

d,c equiv c,d );

registration

coherence

for b_{1} being TarskiGeometryStruct st b_{1} is (TE) & b_{1} is (SC) & b_{1} is (FS') holds

b_{1} is (RE')
by ThMak5;

end;
for b

b

registration
end;

registration
end;

registration

ex b_{1} being non empty (IE) (SC) TarskiGeometryStruct st b_{1} is trivial
end;

cluster non empty trivial satisfying_CongruenceIdentity satisfying_SegmentConstruction (IE) (SC) for TarskiGeometryStruct ;

existence ex b

proof end;

registration

ex b_{1} being non empty (TE) (IE) (SC) TarskiGeometryStruct st b_{1} is (RE')
end;

cluster non empty satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction (TE) (IE) (SC) (RE') for TarskiGeometryStruct ;

existence ex b

proof end;

registration

ex b_{1} being non empty (TE) (IE) (SC) TarskiGeometryStruct st b_{1} is (FS')
end;

cluster non empty satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction (TE) (IE) (SC) (FS') for TarskiGeometryStruct ;

existence ex b

proof end;

theorem :: GTARSKI3:139

:: Main results

registration

coherence

for b_{1} being TarskiGeometryStruct st b_{1} is (RE) & b_{1} is (TE) & b_{1} is (FS) holds

b_{1} is (FS')
by ThMak3;

end;
for b

b

registration

coherence

for b_{1} being non empty TarskiGeometryStruct st b_{1} is (TE) & b_{1} is (IE) & b_{1} is (SC) & b_{1} is (FS') holds

b_{1} is (FS)
by ThMak7;

end;
for b

b

registration

coherence

for b_{1} being non empty TarskiGeometryStruct st b_{1} is (TE) & b_{1} is (IE) & b_{1} is (SC) & b_{1} is (FS') holds

b_{1} is (RE)
by ThMak6;

end;
for b

b

registration

coherence

for b_{1} being non empty TarskiGeometryStruct st b_{1} is (TE) & b_{1} is (IE) & b_{1} is (SC) & b_{1} is (FS') holds

b_{1} is satisfying_SAS
;

end;
for b

b

registration

ex b_{1} being non empty TarskiGeometryStruct st

( b_{1} is (RE) & b_{1} is (TE) & b_{1} is (IE) & b_{1} is (SC) & b_{1} is (FS) & b_{1} is (IB) & b_{1} is (Pa) & b_{1} is (Lo2) & b_{1} is (Up2) & b_{1} is (Eu) & b_{1} is (Co) )
end;

cluster non empty (RE) (TE) (IE) (SC) (FS) (IB) (Pa) (Lo2) (Up2) (Eu) (Co) for TarskiGeometryStruct ;

existence ex b

( b

proof end;

definition

mode Makarios_CE2 is non empty (RE) (TE) (IE) (SC) (FS) (IB) (Pa) (Lo2) (Up2) (Eu) (Co) TarskiGeometryStruct ;

end;
definition

mode Makarios_CE'2 is non empty (TE) (IE) (SC) (IB) (Pa) (Lo2) (Up2) (Eu) (Co) (FS') TarskiGeometryStruct ;

end;
theorem :: GTARSKI3:143

for TP being Makarios_CE2 holds

( TP is satisfying_Tarski-model & TP is satisfying_Lower_Dimension_Axiom & TP is satisfying_Upper_Dimension_Axiom & TP is satisfying_Euclid_Axiom & TP is satisfying_Continuity_Axiom ) ;

( TP is satisfying_Tarski-model & TP is satisfying_Lower_Dimension_Axiom & TP is satisfying_Upper_Dimension_Axiom & TP is satisfying_Euclid_Axiom & TP is satisfying_Continuity_Axiom ) ;

theorem :: GTARSKI3:144

for TP being Makarios_CE'2 holds

( TP is satisfying_Tarski-model & TP is satisfying_Lower_Dimension_Axiom & TP is satisfying_Upper_Dimension_Axiom & TP is satisfying_Euclid_Axiom & TP is satisfying_Continuity_Axiom ) ;

( TP is satisfying_Tarski-model & TP is satisfying_Lower_Dimension_Axiom & TP is satisfying_Upper_Dimension_Axiom & TP is satisfying_Euclid_Axiom & TP is satisfying_Continuity_Axiom ) ;