gtarski3.miz



    begin

    reserve S for satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct,

a,b,c,d,e,f for POINT of S;

    ::$Notion-Name

    theorem :: GTARSKI3:1

    

     Satz2p1: (a,b) equiv (a,b)

    proof

      (b,a) equiv (a,b) by GTARSKI1:def 5;

      hence thesis by GTARSKI1:def 6;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:2

    

     Satz2p1bis: for S be satisfying_CongruenceEquivalenceRelation satisfying_SegmentConstruction TarskiGeometryStruct holds for a,b be POINT of S holds (a,b) equiv (a,b)

    proof

      let S be satisfying_CongruenceEquivalenceRelation satisfying_SegmentConstruction TarskiGeometryStruct;

      let a,b be POINT of S;

      ex c be POINT of S st between (a,a,c) & (a,c) equiv (a,b) by GTARSKI1:def 8;

      hence thesis by GTARSKI1:def 6;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:3

    

     Satz2p2: (a,b) equiv (c,d) implies (c,d) equiv (a,b)

    proof

      assume

       A1: (a,b) equiv (c,d);

      (a,b) equiv (a,b) by Satz2p1;

      hence thesis by A1, GTARSKI1:def 6;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:4

    

     Satz2p2bis: for S be satisfying_CongruenceEquivalenceRelation satisfying_SegmentConstruction TarskiGeometryStruct holds for a,b,c,d be POINT of S st (a,b) equiv (c,d) holds (c,d) equiv (a,b)

    proof

      let S be satisfying_CongruenceEquivalenceRelation satisfying_SegmentConstruction TarskiGeometryStruct;

      let a,b,c,d be POINT of S;

      assume

       A1: (a,b) equiv (c,d);

      (a,b) equiv (a,b) by Satz2p1bis;

      hence thesis by A1, GTARSKI1:def 6;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:5

    

     Satz2p3: (a,b) equiv (c,d) & (c,d) equiv (e,f) implies (a,b) equiv (e,f)

    proof

      assume

       A1: (a,b) equiv (c,d) & (c,d) equiv (e,f);

      then (c,d) equiv (a,b) by Satz2p2;

      hence thesis by A1, GTARSKI1:def 6;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:6

    

     Satz2p4: (a,b) equiv (c,d) implies (b,a) equiv (c,d)

    proof

      assume

       A1: (a,b) equiv (c,d);

      (b,a) equiv (a,b) by GTARSKI1:def 5;

      hence thesis by A1, Satz2p3;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:7

    

     Satz2p5: (a,b) equiv (c,d) implies (a,b) equiv (d,c)

    proof

      assume

       A1: (a,b) equiv (c,d);

      (c,d) equiv (d,c) by GTARSKI1:def 5;

      hence thesis by A1, Satz2p3;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:8

    

     Satz2p8: for S be satisfying_CongruenceIdentity satisfying_SegmentConstruction TarskiGeometryStruct holds for a,b be POINT of S holds (a,a) equiv (b,b)

    proof

      let S be satisfying_CongruenceIdentity satisfying_SegmentConstruction TarskiGeometryStruct;

      let a,b be POINT of S;

      ex c be POINT of S st between (a,a,c) & (a,c) equiv (b,b) by GTARSKI1:def 8;

      hence thesis by GTARSKI1:def 7;

    end;

    definition

      let S be TarskiGeometryStruct;

      :: GTARSKI3:def1

      attr S is satisfying_SST_A5 means for a,b,c,d,a9,b9,c9,d9 be 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);

    end

    theorem :: GTARSKI3:9

    

     EQUIV1: S is satisfying_SAS iff S is satisfying_SST_A5

    proof

      thus S is satisfying_SAS implies S is satisfying_SST_A5

      proof

        assume

         A1: S is satisfying_SAS;

        now

          let a,b,c,d,a9,b9,c9,d9 be POINT of S;

          assume

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

          then (a,b,d) cong (a9,b9,d9);

          then (d,c) equiv (d9,c9) by A1, A2;

          then (c,d) equiv (d9,c9) by Satz2p4;

          hence (c,d) equiv (c9,d9) by Satz2p5;

        end;

        hence thesis;

      end;

      thus S is satisfying_SST_A5 implies S is satisfying_SAS

      proof

        assume

         A3: S is satisfying_SST_A5;

        now

          let a,b,c,x,a1,b1,c1,x1 be POINT of S;

          assume a <> b & (a,b,c) cong (a1,b1,c1) & between (a,b,x) & between (a1,b1,x1) & (b,x) equiv (b1,x1);

          then (x,c) equiv (x1,c1) by A3;

          then (c,x) equiv (x1,c1) by Satz2p4;

          hence (c,x) equiv (c1,x1) by Satz2p5;

        end;

        hence thesis;

      end;

    end;

    registration

      cluster satisfying_SST_A5 -> satisfying_SAS for satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct;

      coherence by EQUIV1;

    end

    registration

      cluster satisfying_SAS -> satisfying_SST_A5 for satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct;

      coherence by EQUIV1;

    end

    definition

      let S be TarskiGeometryStruct;

      let a,b,c,d,a9,b9,c9,d9 be POINT of S;

      :: GTARSKI3:def2

      pred a,b,c,d AFS a9,b9,c9,d9 means 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);

    end

    theorem :: GTARSKI3:10

    

     Axiom5AFS: for S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_SAS TarskiGeometryStruct holds for a,b,c,d,a9,b9,c9,d9 be POINT of S st (a,b,c,d) AFS (a9,b9,c9,d9) & a <> b holds (c,d) equiv (c9,d9)

    proof

      let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_SAS TarskiGeometryStruct;

      let a,b,c,d,a9,b9,c9,d9 be POINT of S;

      assume

       A1: (a,b,c,d) AFS (a9,b9,c9,d9) & a <> b;

      S is satisfying_SST_A5;

      hence thesis by A1;

    end;

    reserve S for satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS TarskiGeometryStruct,

q,a,b,c,a9,b9,c9,x1,x2 for POINT of S;

    ::$Notion-Name

    theorem :: GTARSKI3:11

    

     Satz2p11: between (a,b,c) & between (a9,b9,c9) & (a,b) equiv (a9,b9) & (b,c) equiv (b9,c9) implies (a,c) equiv (a9,c9)

    proof

      assume

       A1: between (a,b,c) & between (a9,b9,c9) & (a,b) equiv (a9,b9) & (b,c) equiv (b9,c9);

      

       A2: S is satisfying_SST_A5;

      (b,a) equiv (a9,b9) by A1, Satz2p4;

      then

       A3: (a,b,c,a) AFS (a9,b9,c9,a9) by A1, Satz2p5, Satz2p8;

      per cases ;

        suppose a = b;

        hence thesis by A1, Satz2p2, GTARSKI1:def 7;

      end;

        suppose a <> b;

        then (c,a) equiv (c9,a9) by A3, A2;

        then (a,c) equiv (c9,a9) by Satz2p4;

        hence thesis by Satz2p5;

      end;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:12

    

     Satz2p12: q <> a implies (for x1, x2 st between (q,a,x1) & (a,x1) equiv (b,c) & between (q,a,x2) & (a,x2) equiv (b,c) holds x1 = x2)

    proof

      assume

       A1: q <> a;

      

       A2: S is satisfying_SST_A5;

      hereby

        let x1, x2;

        assume

         A3: between (q,a,x1) & (a,x1) equiv (b,c) & between (q,a,x2) & (a,x2) equiv (b,c);

        then (b,c) equiv (a,x2) by Satz2p2;

        then

         A4: (a,x1) equiv (a,x2) by A3, Satz2p3;

        (q,a) equiv (q,a) & (a,x1) equiv (a,x1) by Satz2p1;

        then (q,a,x1,x1) AFS (q,a,x1,x2) by A3, A4, Satz2p11;

        then (x1,x1) equiv (x1,x2) by A1, A2;

        hence x1 = x2 by Satz2p2, GTARSKI1:def 7;

      end;

    end;

    begin

    ::$Notion-Name

    theorem :: GTARSKI3:13

    

     Satz3p1: for S be satisfying_CongruenceIdentity satisfying_SegmentConstruction TarskiGeometryStruct holds for a,b be POINT of S holds between (a,b,b)

    proof

      let S be satisfying_CongruenceIdentity satisfying_SegmentConstruction TarskiGeometryStruct;

      let a,b be POINT of S;

      ex x be POINT of S st between (a,b,x) & (b,x) equiv (b,b) by GTARSKI1:def 8;

      hence thesis by GTARSKI1:def 7;

    end;

    reserve S for satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct,

a,b,c,d for POINT of S;

    ::$Notion-Name

    theorem :: GTARSKI3:14

    

     Satz3p2: between (a,b,c) implies between (c,b,a)

    proof

      assume

       A1: between (a,b,c);

       between (b,c,c) by Satz3p1;

      then ex x be POINT of S st between (b,x,b) & between (c,x,a) by A1, GTARSKI1:def 11;

      hence thesis by GTARSKI1:def 10;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:15

     between (a,a,b) by Satz3p1, Satz3p2;

    ::$Notion-Name

    theorem :: GTARSKI3:16

    

     Satz3p4: for S be satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct holds for a,b,c be POINT of S st between (a,b,c) & between (b,a,c) holds a = b

    proof

      let S be satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct;

      let a,b,c be POINT of S;

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

      then

      consider x be POINT of S such that

       A1: between (b,x,b) & between (a,x,a) by GTARSKI1:def 11;

      x = a & x = b by A1, GTARSKI1:def 10;

      hence thesis;

    end;

    

     Satz3p5p1: between (a,b,d) & between (b,c,d) implies between (a,b,c)

    proof

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

      then

      consider x be POINT of S such that

       A1: between (b,x,b) & between (c,x,a) by GTARSKI1:def 11;

      b = x by A1, GTARSKI1:def 10;

      hence thesis by A1, Satz3p2;

    end;

    

     Satz3p6p1: between (a,b,c) & between (a,c,d) implies between (b,c,d)

    proof

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

      then between (c,b,a) & between (d,c,a) by Satz3p2;

      then between (d,c,b) by Satz3p5p1;

      hence thesis by Satz3p2;

    end;

    reserve S for satisfying_Tarski-model TarskiGeometryStruct,

a,b,c,d for POINT of S;

    

     Satz3p7p1: between (a,b,c) & between (b,c,d) & b <> c implies between (a,c,d)

    proof

      assume

       A1: between (a,b,c) & between (b,c,d) & b <> c;

      consider x be POINT of S such that

       A2: between (a,c,x) & (c,x) equiv (c,d) by GTARSKI1:def 8;

      

       A3: between (b,c,x) by A1, A2, Satz3p6p1;

      (c,d) equiv (c,d) by Satz2p1;

      hence thesis by A1, A2, A3, Satz2p12;

    end;

    

     Satz3p5p2: between (a,b,d) & between (b,c,d) implies between (a,c,d)

    proof

      assume

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

      then between (a,b,c) by Satz3p5p1;

      hence thesis by A1, Satz3p7p1;

    end;

    

     Satz3p6p2: between (a,b,c) & between (a,c,d) implies between (a,b,d)

    proof

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

      then between (c,b,a) & between (d,c,a) by Satz3p2;

      then between (d,b,a) by Satz3p5p2;

      hence thesis by Satz3p2;

    end;

    

     Satz3p7p2: between (a,b,c) & between (b,c,d) & b <> c implies between (a,b,d)

    proof

      assume

       A1: between (a,b,c) & between (b,c,d) & b <> c;

      then between (c,b,a) & between (d,c,b) by Satz3p2;

      then between (d,b,a) by A1, Satz3p7p1;

      hence thesis by Satz3p2;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:17

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

    ::$Notion-Name

    theorem :: GTARSKI3:18

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

    ::$Notion-Name

    theorem :: GTARSKI3:19

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

    ::$Notion-Name

    definition

      let S be TarskiGeometryStruct;

      let a,b,c,d be POINT of S;

      :: GTARSKI3:def3

      pred between4 a,b,c,d means between (a,b,c) & between (a,b,d) & between (a,c,d) & between (b,c,d);

    end

    ::$Notion-Name

    definition

      let S be TarskiGeometryStruct;

      let a,b,c,d,e be POINT of S;

      :: GTARSKI3:def4

      pred between5 a,b,c,d,e means 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);

    end

    reserve S for satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct,

a,b,c,d,e for POINT of S;

    ::$Notion-Name

    theorem :: GTARSKI3:20

     between (a,b,c) implies between (c,b,a) by Satz3p2;

    ::$Notion-Name

    theorem :: GTARSKI3:21

     between4 (a,b,c,d) implies between4 (d,c,b,a) by Satz3p2;

    ::$Notion-Name

    theorem :: GTARSKI3:22

     between5 (a,b,c,d,e) implies between5 (e,d,c,b,a) by Satz3p2;

    ::$Notion-Name

    theorem :: GTARSKI3:23

    for S be satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct holds for a,b,c,d be 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);

    ::$Notion-Name

    theorem :: GTARSKI3:24

     between5 (a,b,c,d,e) implies 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);

    reserve S for satisfying_Tarski-model TarskiGeometryStruct,

a,b,c,d,p for POINT of S;

    ::$Notion-Name

    theorem :: GTARSKI3:25

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

    ::$Notion-Name

    theorem :: GTARSKI3:26

    

     Satz3p11p3pb: between (a,b,c) & between (b,p,c) implies between4 (a,b,p,c) by Satz3p5p1, Satz3p5p2;

    ::$Notion-Name

    theorem :: GTARSKI3:27

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

    proof

      assume

       A1: between4 (a,b,c,d) & between (a,p,b);

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

      hence thesis by A1, Satz3p5p2;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:28

    

     Satz3p11p4pb: between4 (a,b,c,d) & between (b,p,c) implies between5 (a,b,p,c,d)

    proof

      assume

       A1: between4 (a,b,c,d) & between (b,p,c);

      then between (a,b,p) & between (p,c,d) & between (b,p,c) & between (b,p,d) & between (a,p,c) by Satz3p5p1, Satz3p5p2, Satz3p6p1, Satz3p6p2;

      hence thesis by A1, Satz3p5p2;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:29

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

    proof

      assume

       A1: between4 (a,b,c,d) & between (c,p,d);

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

      hence thesis by A1, Satz3p5p1;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:30

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

    ::$Notion-Name

    theorem :: GTARSKI3:31

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

    ::$Notion-Name

    theorem :: GTARSKI3:32

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

    proof

      assume

       A1: between4 (a,b,c,d) & between (a,d,p);

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

      hence thesis by A1, Satz3p6p1;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:33

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

    proof

      assume

       A1: between4 (a,b,c,d) & between (b,d,p);

      hence between4 (b,c,d,p) by Satz3p6p1, Satz3p6p2;

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

      proof

        assume b <> d;

        then between (a,b,p) & between (a,d,p) by A1, Satz3p7p1, Satz3p7p2;

        hence thesis by A1, Satz3p6p1, Satz3p6p2;

      end;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:34

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

    proof

      assume

       A1: between4 (a,b,c,d) & between (c,d,p);

      hence between (c,d,p);

      hereby

        assume c <> d;

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

        hence between5 (a,b,c,d,p) by A1, Satz3p7p2;

      end;

    end;

    registration

      cluster satisfying_Lower_Dimension_Axiom for satisfying_Tarski-model TarskiGeometryStruct;

      existence

      proof

        take TarskiEuclid2Space ;

        thus thesis;

      end;

    end

    ::$Notion-Name

    theorem :: GTARSKI3:35

    

     Satz3p13: for S be satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_Lower_Dimension_Axiom TarskiGeometryStruct holds ex a,b,c be 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

    proof

      let S be satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_Lower_Dimension_Axiom TarskiGeometryStruct;

      consider a,b,c be POINT of S such that

       A1: not between (a,b,c) & not between (b,c,a) & not between (c,a,b) by GTARSKI2:def 7;

      take a, b, c;

      thus thesis by A1, Satz3p1;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:36

    

     Satz3p14: for S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_Lower_Dimension_Axiom TarskiGeometryStruct holds for a,b be POINT of S holds ex c be POINT of S st between (a,b,c) & b <> c

    proof

      let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_Lower_Dimension_Axiom TarskiGeometryStruct;

      let a,b be POINT of S;

      consider u,v,w be POINT of S such that

       A1: not between (u,v,w) & not between (v,w,u) & not between (w,u,v) & u <> v & v <> w & w <> u by Satz3p13;

      consider x be POINT of S such that

       A2: between (a,b,x) & (b,x) equiv (u,v) by GTARSKI1:def 8;

      b <> x by A1, A2, Satz2p2, GTARSKI1:def 7;

      hence thesis by A2;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:37

    

     Satz3p15p3: for S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Lower_Dimension_Axiom TarskiGeometryStruct holds for a1,a2 be POINT of S st a1 <> a2 holds ex a3 be POINT of S st between (a1,a2,a3) & (a1,a2,a3) are_mutually_distinct

    proof

      let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Lower_Dimension_Axiom TarskiGeometryStruct;

      let a1,a2 be POINT of S;

      assume

       A1: a1 <> a2;

      consider a3 be POINT of S such that

       A2: between (a1,a2,a3) & a2 <> a3 by Satz3p14;

      a1 <> a3 by A2, GTARSKI1:def 10;

      hence thesis by A1, A2, ZFMISC_1:def 5;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:38

    

     Satz3p15p4: for S be satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct holds for a1,a2 be POINT of S st a1 <> a2 holds ex a3,a4 be POINT of S st between4 (a1,a2,a3,a4) & (a1,a2,a3,a4) are_mutually_distinct

    proof

      let S be satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct;

      let a1,a2 be POINT of S;

      assume a1 <> a2;

      then

      consider a3 be POINT of S such that

       A1: between (a1,a2,a3) & (a1,a2,a3) are_mutually_distinct by Satz3p15p3;

      consider a4 be POINT of S such that

       A2: between (a2,a3,a4) & (a2,a3,a4) are_mutually_distinct by A1, Satz3p15p3;

      take a3, a4;

      thus between4 (a1,a2,a3,a4) by A1, A2, Satz3p7p1, Satz3p7p2;

      thus (a1,a2,a3,a4) are_mutually_distinct by A1, Satz3p7p1, GTARSKI1:def 10, A2;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:39

    for S be satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct holds for a1,a2 be POINT of S st a1 <> a2 holds ex a3,a4,a5 be POINT of S st between5 (a1,a2,a3,a4,a5) & (a1,a2,a3,a4,a5) are_mutually_distinct

    proof

      let S be satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct;

      let a1,a2 be POINT of S;

      assume a1 <> a2;

      then

      consider a3,a4 be POINT of S such that

       A1: between4 (a1,a2,a3,a4) & (a1,a2,a3,a4) are_mutually_distinct by Satz3p15p4;

      consider a5 be POINT of S such that

       A2: between (a3,a4,a5) & (a3,a4,a5) are_mutually_distinct by A1, Satz3p15p3;

      take a3, a4, a5;

       between (a1,a3,a5) & between (a1,a4,a5) & between (a2,a3,a5) & between (a2,a4,a5) by A1, A2, Satz3p7p1, Satz3p7p2;

      hence between5 (a1,a2,a3,a4,a5) by A1, A2, Satz3p6p2;

      thus (a1,a2,a3,a4,a5) are_mutually_distinct by A1, A2, Satz3p7p1, GTARSKI1:def 10;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:40

    

     Satz3p17: for S be satisfying_Tarski-model TarskiGeometryStruct holds for a,b,c,p,a9,b9,c9 be POINT of S st between (a,b,c) & between (a9,b9,c) & between (a,p,a9) holds ex q be POINT of S st between (p,q,c) & between (b,q,b9)

    proof

      let S be satisfying_Tarski-model TarskiGeometryStruct;

      let a,b,c,p,a9,b9,c9 be POINT of S;

      assume

       A1: between (a,b,c) & between (a9,b9,c) & between (a,p,a9);

      then between (c,b9,a9) by Satz3p2;

      then

      consider x be POINT of S such that

       A2: between (b9,x,a) & between (p,x,c) by A1, GTARSKI1:def 11;

       between (c,b,a) by A1, Satz3p2;

      then

      consider q be POINT of S such that

       A3: between (x,q,c) & between (b,q,b9) by A2, GTARSKI1:def 11;

       between (p,q,c) by A2, A3, Satz3p5p2;

      hence thesis by A3;

    end;

    begin

    definition

      let S be TarskiGeometryStruct;

      let a,b,c,d,a9,b9,c9,d9 be POINT of S;

      :: GTARSKI3:def5

      pred a,b,c,d IFS a9,b9,c9,d9 means 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);

    end

    reserve S for satisfying_Tarski-model TarskiGeometryStruct,

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

    ::$Notion-Name

    theorem :: GTARSKI3:41

    

     Satz4p2: (a,b,c,d) IFS (a9,b9,c9,d9) implies (b,d) equiv (b9,d9)

    proof

      assume

       A1: (a,b,c,d) IFS (a9,b9,c9,d9);

      per cases ;

        suppose

         A2: a = c;

        now

          thus c = b by A1, A2, GTARSKI1:def 10;

          a9 = c9 by A1, A2, Satz2p2, GTARSKI1:def 7;

          hence c9 = b9 by A1, GTARSKI1:def 10;

        end;

        hence thesis by A1;

      end;

        suppose

         A3: a <> c;

        consider e be POINT of S such that

         A4: between (a,c,e) & (c,e) equiv (a,c) by GTARSKI1:def 8;

        

         A5: c <> e by A3, A4, Satz2p2, GTARSKI1:def 7;

        consider e9 be POINT of S such that

         A6: between (a9,c9,e9) & (c9,e9) equiv (c,e) by GTARSKI1:def 8;

        

         A7: (c,e) equiv (c9,e9) by A6, Satz2p2;

        S is satisfying_SST_A5;

        then

         A8: (e,d) equiv (e9,d9) by A3, A4, A6, A1, A7;

        (c,b) equiv (b9,c9) by A1, Satz2p4;

        then

         A9: (c,b) equiv (c9,b9) by Satz2p5;

        (e9,c9) equiv (c,e) by A6, Satz2p4;

        then (e9,c9) equiv (e,c) by Satz2p5;

        then

         A17: (e,c) equiv (e9,c9) by Satz2p2;

        

         A18: between (e,c,b)

        proof

           between (b,c,e) & between (a,b,e) by A1, A4, Satz3p6p1, Satz3p6p2;

          hence thesis by Satz3p2;

        end;

        

         A19: between (e9,c9,b9)

        proof

           between (b9,c9,e9) & between (a9,b9,e9) by A1, A6, Satz3p6p1, Satz3p6p2;

          hence thesis by Satz3p2;

        end;

        S is satisfying_SST_A5;

        hence thesis by A19, A18, A8, A9, A17, A1, A5;

      end;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:42

    

     Satz4p3: between (a,b,c) & between (a9,b9,c9) & (a,c) equiv (a9,c9) & (b,c) equiv (b9,c9) implies (a,b) equiv (a9,b9)

    proof

      assume

       A1: between (a,b,c) & between (a9,b9,c9) & (a,c) equiv (a9,c9) & (b,c) equiv (b9,c9);

      then (c,a) equiv (a9,c9) by Satz2p4;

      then (a,b,c,a) IFS (a9,b9,c9,a9) by A1, Satz2p8, Satz2p5;

      then (a,b) equiv (b9,a9) by Satz4p2, Satz2p4;

      hence thesis by Satz2p5;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:43

    

     Satz4p5: between (a,b,c) & (a,c) equiv (a9,c9) implies ex b9 st between (a9,b9,c9) & (a,b,c) cong (a9,b9,c9)

    proof

      assume

       A1: between (a,b,c) & (a,c) equiv (a9,c9);

      consider d9 be POINT of S such that

       A2: between (c9,a9,d9) & (a9,d9) equiv (c9,a9) by GTARSKI1:def 8;

      per cases ;

        suppose a9 = d9;

        then c9 = a9 by A2, Satz2p2, GTARSKI1:def 7;

        then a = c by A1, GTARSKI1:def 7;

        then

         A2BIS: a = b by A1, GTARSKI1:def 10;

        take a9;

        thus thesis by A2BIS, Satz2p8, A1, Satz3p1, Satz3p2;

      end;

        suppose

         A2TER: a9 <> d9;

        consider b9 be POINT of S such that

         A3: between (d9,a9,b9) & (a9,b9) equiv (a,b) by GTARSKI1:def 8;

        consider c99 be POINT of S such that

         A4: between (d9,b9,c99) & (b9,c99) equiv (b,c) by GTARSKI1:def 8;

        

         A5: between (a9,b9,c99) & between (d9,a9,c99) by A3, A4, Satz3p6p1, Satz3p6p2;

        

         A6: (a,b) equiv (a9,b9) by A3, Satz2p2;

        

         A7: (b,c) equiv (b9,c99) by A4, Satz2p2;

        then

         A8: (a,c) equiv (a9,c99) by A1, A5, A6, Satz2p11;

        

         A9: c99 = c9

        proof

          

           A10: between (d9,a9,c9) by A2, Satz3p2;

          

           A11: between (d9,a9,c99) by A3, A4, Satz3p6p2;

          

           A12: (a9,c9) equiv (a,c) by A1, Satz2p2;

          (a9,c99) equiv (a,c) by A8, Satz2p2;

          hence thesis by A2TER, A10, A11, A12, Satz2p12;

        end;

         between (a9,b9,c9) by A3, A4, Satz3p6p1, A9;

        hence thesis by A6, A7, A1, A9, GTARSKI1:def 3;

      end;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:44

    

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

    proof

      assume

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

      consider b99 be POINT of S such that

       A3: between (a9,b99,c9) & (a,b,c) cong (a9,b99,c9) by A1, Satz4p5;

      

       A5: (a9,b99) equiv (a,b) & (b99,c9) equiv (b,c) by A3, Satz2p2;

      then (a9,b99) equiv (a9,b9) & (b99,c9) equiv (b9,c9) by A1, Satz2p3;

      then (c9,b99) equiv (b9,c9) by Satz2p4;

      then (a9,b99,c9,b99) IFS (a9,b99,c9,b9) by A5, A3, A1, Satz2p1, Satz2p3, Satz2p5;

      then (b99,b9) equiv (b99,b99) by Satz2p2, Satz4p2;

      hence thesis by A3, GTARSKI1:def 7;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:45

    for S be satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct holds for a,b,c be 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;

    ::$Notion-Name

    theorem :: GTARSKI3:46

    for S be satisfying_CongruenceIdentity satisfying_SegmentConstruction TarskiGeometryStruct holds for a,b be POINT of S holds Collinear (a,a,b) by Satz3p1;

    theorem :: GTARSKI3:47

    

     Lm4p13p1: for S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct holds for a,b,c,a9,b9,c9 be POINT of S st (a,b,c) cong (a9,b9,c9) holds (b,c,a) cong (b9,c9,a9)

    proof

      let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct;

      let a,b,c,a9,b9,c9 be POINT of S;

      assume

       A1: (a,b,c) cong (a9,b9,c9);

      then (b,a) equiv (a9,b9) & (c,a) equiv (a9,c9) by Satz2p4;

      hence (b,c,a) cong (b9,c9,a9) by A1, Satz2p5;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:48

    

     Satz4p13: for S be satisfying_Tarski-model TarskiGeometryStruct holds for a,b,c,a9,b9,c9 be POINT of S st Collinear (a,b,c) & (a,b,c) cong (a9,b9,c9) holds Collinear (a9,b9,c9)

    proof

      let S be satisfying_Tarski-model TarskiGeometryStruct;

      let a,b,c,a9,b9,c9 be POINT of S;

      assume

       A1: Collinear (a,b,c) & (a,b,c) cong (a9,b9,c9);

      

       A4: between (b,c,a) implies between (b9,c9,a9)

      proof

        assume

         A5: between (b,c,a);

        (b,c,a) cong (b9,c9,a9) by A1, Lm4p13p1;

        hence between (b9,c9,a9) by A5, Satz4p6;

      end;

       between (c,a,b) implies between (c9,a9,b9)

      proof

        assume

         A8: between (c,a,b);

        (b,c,a) cong (b9,c9,a9) by A1, Lm4p13p1;

        then (c,a,b) cong (c9,a9,b9) by Lm4p13p1;

        hence between (c9,a9,b9) by A8, Satz4p6;

      end;

      hence thesis by A1, A4, Satz4p6;

    end;

    theorem :: GTARSKI3:49

    

     Lm4p14p1: for S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct holds for a,b,c,a9,b9,c9 be POINT of S st (b,a,c) cong (b9,a9,c9) holds (a,b,c) cong (a9,b9,c9)

    proof

      let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct;

      let a,b,c,a9,b9,c9 be POINT of S;

      assume

       A1: (b,a,c) cong (b9,a9,c9);

      then (a,b) equiv (b9,a9) by Satz2p4;

      hence (a,b,c) cong (a9,b9,c9) by A1, Satz2p5;

    end;

    theorem :: GTARSKI3:50

    

     Lm4p14p2: for S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct holds for a,b,c,a9,b9,c9 be POINT of S st (a,c,b) cong (a9,c9,b9) holds (a,b,c) cong (a9,b9,c9)

    proof

      let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct;

      let a,b,c,a9,b9,c9 be POINT of S;

      assume

       A1: (a,c,b) cong (a9,c9,b9);

      then (b,c) equiv (c9,b9) by Satz2p4;

      hence thesis by A1, Satz2p5;

    end;

    reserve S for satisfying_Tarski-model TarskiGeometryStruct,

a,b,c,d,a9,b9,c9,d9,p,q for POINT of S;

    ::$Notion-Name

    theorem :: GTARSKI3:51

    

     Satz4p14: Collinear (a,b,c) & (a,b) equiv (a9,b9) implies ex c9 be POINT of S st (a,b,c) cong (a9,b9,c9)

    proof

      assume

       A1: Collinear (a,b,c) & (a,b) equiv (a9,b9);

      per cases ;

        suppose

         A2: between (a,b,c);

        consider c9 be POINT of S such that

         A3: between (a9,b9,c9) & (b9,c9) equiv (b,c) by GTARSKI1:def 8;

        

         A4: (b,c) equiv (b9,c9) by A3, Satz2p2;

        then (a,c) equiv (a9,c9) by A1, A3, A2, Satz2p11;

        hence thesis by A1, A4, GTARSKI1:def 3;

      end;

        suppose between (c,a,b);

        then

         A5: between (b,a,c) by Satz3p2;

        consider c9 be POINT of S such that

         A6: between (b9,a9,c9) & (a9,c9) equiv (a,c) by GTARSKI1:def 8;

        (b,a) equiv (a9,b9) by A1, Satz2p4;

        then

         A7: (b,a) equiv (b9,a9) by Satz2p5;

        (a,c) equiv (a9,c9) by A6, Satz2p2;

        then (b,a,c) cong (b9,a9,c9) by A5, A6, A7, Satz2p11;

        hence thesis by Lm4p14p1;

      end;

        suppose between (b,c,a);

        then ex y be POINT of S st between (a9,y,b9) & (a,c,b) cong (a9,y,b9) by A1, Satz3p2, Satz4p5;

        hence thesis by Lm4p14p2;

      end;

    end;

    definition

      let S be TarskiGeometryStruct;

      let a,b,c,d,a9,b9,c9,d9 be POINT of S;

      :: GTARSKI3:def6

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

    end

    ::$Notion-Name

    theorem :: GTARSKI3:52

    

     Satz4p16: (a,b,c,d) FS (a9,b9,c9,d9) & a <> b implies (c,d) equiv (c9,d9)

    proof

      assume

       A1: (a,b,c,d) FS (a9,b9,c9,d9) & a <> b;

      then Collinear (a,b,c);

      per cases ;

        suppose

         A2: between (a,b,c);

        then

         A3: between (a9,b9,c9) by A1, Satz4p6;

        

         A4: (a,b) equiv (a9,b9) & (a,c) equiv (a9,c9) & (b,c) equiv (b9,c9) by A1, GTARSKI1:def 3;

        S is satisfying_SST_A5;

        hence thesis by A1, A4, A2, A3;

      end;

        suppose

         A5: between (b,c,a);

        (b,c,a) cong (b9,c9,a9) by A1, Lm4p13p1;

        then (b,c,a,d) IFS (b9,c9,a9,d9) by A5, Satz4p6, A1;

        hence thesis by Satz4p2;

      end;

        suppose between (c,a,b);

        then

         A6: between (b,a,c) by Satz3p2;

        

         A7: (b,a,c) cong (b9,a9,c9) by A1, Lm4p14p1;

        

         A8: between (b9,a9,c9) by A6, A7, Satz4p6;

        S is satisfying_SST_A5;

        hence thesis by A1, A8, A6, A7;

      end;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:53

    

     Satz4p17: a <> b & Collinear (a,b,c) & (a,p) equiv (a,q) & (b,p) equiv (b,q) implies (c,p) equiv (c,q)

    proof

      assume

       A1: a <> b & Collinear (a,b,c) & (a,p) equiv (a,q) & (b,p) equiv (b,q);

      (a,b,c,p) FS (a,b,c,q)

      proof

        (a,b) equiv (a,b) & (a,c) equiv (a,c) & (b,c) equiv (b,c) by Satz2p1;

        hence thesis by A1, GTARSKI1:def 3;

      end;

      hence (c,p) equiv (c,q) by A1, Satz4p16;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:54

    

     Satz4p18: a <> b & Collinear (a,b,c) & (a,c) equiv (a,c9) & (b,c) equiv (b,c9) implies c = c9

    proof

      assume a <> b & Collinear (a,b,c) & (a,c) equiv (a,c9) & (b,c) equiv (b,c9);

      then (c,c) equiv (c,c9) by Satz4p17;

      hence thesis by Satz2p2, GTARSKI1:def 7;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:55

    

     Satz4p19: between (a,c,b) & (a,c) equiv (a,c9) & (b,c) equiv (b,c9) implies c = c9

    proof

      assume

       A1: between (a,c,b) & (a,c) equiv (a,c9) & (b,c) equiv (b,c9);

      

       A2: a = b implies c = c9

      proof

        assume a = b;

        then a = c by A1, GTARSKI1:def 10;

        hence thesis by A1, Satz2p2, GTARSKI1:def 7;

      end;

      a <> b implies c = c9

      proof

        assume

         A3: a <> b;

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

        hence thesis by A1, A3, Satz4p18;

      end;

      hence thesis by A2;

    end;

    begin

    reserve S for satisfying_Tarski-model TarskiGeometryStruct,

a,b,c,d,e,f,a9,b9,c9,d9 for POINT of S;

    ::$Notion-Name

    theorem :: GTARSKI3:56

    

     Satz5p1: a <> b & between (a,b,c) & between (a,b,d) implies between (a,c,d) or between (a,d,c)

    proof

      assume

       A1: a <> b & between (a,b,c) & between (a,b,d);

      then between (b,d,c) or between (b,c,d) by GTARSKI1: 37;

      hence thesis by A1, Satz3p5p2;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:57

    

     Satz5p2: a <> b & between (a,b,c) & between (a,b,d) implies between (b,c,d) or between (b,d,c)

    proof

      assume

       A1: a <> b & between (a,b,c) & between (a,b,d);

      then between (a,c,d) or between (a,d,c) by Satz5p1;

      hence thesis by A1, Satz3p6p1;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:58

    

     Satz5p3: between (a,b,d) & between (a,c,d) implies between (a,b,c) or between (a,c,b)

    proof

      assume

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

      per cases ;

        suppose a = b;

        hence thesis by Satz3p1, Satz3p2;

      end;

        suppose

         A2: a <> b;

        consider p be POINT of S such that

         A3: between (d,a,p) & (a,p) equiv (a,b) by GTARSKI1:def 8;

        

         A4: a <> p by A3, Satz2p2, A2, GTARSKI1:def 7;

         between (p,a,d) by A3, Satz3p2;

        then between (p,a,b) & between (p,a,c) by A1, Satz3p5p1;

        hence thesis by A4, Satz5p2;

      end;

    end;

    definition

      let S be TarskiGeometryStruct;

      let a,b,c,d be POINT of S;

      :: GTARSKI3:def7

      pred a,b <= c,d means ex y be POINT of S st between (c,y,d) & (a,b) equiv (c,y);

    end

    ::$Notion-Name

    theorem :: GTARSKI3:59

    

     Satz5p5: (a,b) <= (c,d) iff (ex x be POINT of S st between (a,b,x) & (a,x) equiv (c,d))

    proof

      

       A1: (a,b) <= (c,d) implies (ex x be POINT of S st between (a,b,x) & (a,x) equiv (c,d))

      proof

        assume (a,b) <= (c,d);

        then

        consider y be POINT of S such that

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

         Collinear (c,y,d) by A2;

        then

        consider x be POINT of S such that

         A3: (c,y,d) cong (a,b,x) by A2, Satz2p2, Satz4p14;

        (a,x) equiv (c,d) by A3, Satz2p2;

        hence thesis by A2, A3, Satz4p6;

      end;

      (ex x be POINT of S st between (a,b,x) & (a,x) equiv (c,d)) implies (a,b) <= (c,d)

      proof

        assume ex x be POINT of S st between (a,b,x) & (a,x) equiv (c,d);

        then

        consider x be POINT of S such that

         A4: between (a,b,x) & (a,x) equiv (c,d);

        

         A5: Collinear (x,a,b) by A4;

        (x,a) equiv (c,d) by A4, Satz2p4;

        then

        consider y be POINT of S such that

         A6: (x,a,b) cong (d,c,y) by A5, Satz2p5, Satz4p14;

        (a,b,x) cong (c,y,d)

        proof

          

           A9: (a,x) equiv (c,d)

          proof

            (a,x) equiv (d,c) by A6, Satz2p4;

            hence thesis by Satz2p5;

          end;

          (b,x) equiv (y,d)

          proof

            (b,x) equiv (d,y) by A6, Satz2p4;

            hence thesis by Satz2p5;

          end;

          hence thesis by A6, A9;

        end;

        hence thesis by A4, Satz4p6;

      end;

      hence thesis by A1;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:60

    

     Satz5p6: (a,b) <= (c,d) & (a,b) equiv (a9,b9) & (c,d) equiv (c9,d9) implies (a9,b9) <= (c9,d9)

    proof

      assume

       A1: (a,b) <= (c,d) & (a,b) equiv (a9,b9) & (c,d) equiv (c9,d9);

      then

      consider x be POINT of S such that

       A2: between (a,b,x) & (a,x) equiv (c,d) by Satz5p5;

       Collinear (a,b,x) by A2;

      then

      consider y be POINT of S such that

       A3: (a,b,x) cong (a9,b9,y) by A1, Satz4p14;

      (a9,y) equiv (c9,d9)

      proof

        (a9,y) equiv (a,x) by A3, Satz2p2;

        then (a9,y) equiv (c,d) by A2, Satz2p3;

        hence thesis by A1, Satz2p3;

      end;

      hence (a9,b9) <= (c9,d9) by A2, A3, Satz4p6, Satz5p5;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:61

    (a,b) <= (a,b)

    proof

       between (a,b,b) by Satz3p1;

      hence thesis by Satz2p1;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:62

    (a,b) <= (c,d) & (c,d) <= (e,f) implies (a,b) <= (e,f)

    proof

      assume

       A1: (a,b) <= (c,d) & (c,d) <= (e,f);

      then

      consider x be POINT of S such that

       A2: between (a,b,x) & (a,x) equiv (c,d) by Satz5p5;

      consider y be POINT of S such that

       A3: between (c,d,y) & (c,y) equiv (e,f) by A1, Satz5p5;

       Collinear (c,d,y) by A3;

      then

      consider q be POINT of S such that

       A4: (c,d,y) cong (a,x,q) by A2, Satz2p2, Satz4p14;

      

       A5: between (a,b,q)

      proof

         between (a,x,q) by A3, A4, Satz4p6;

        hence thesis by A2, Satz3p6p2;

      end;

      (a,q) equiv (e,f)

      proof

        (a,q) equiv (c,y) by A4, Satz2p2;

        hence thesis by A3, Satz2p3;

      end;

      hence thesis by A5, Satz5p5;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:63

    (a,b) <= (c,d) & (c,d) <= (a,b) implies (a,b) equiv (c,d)

    proof

      assume

       A1: (a,b) <= (c,d) & (c,d) <= (a,b);

      then

      consider y be POINT of S such that

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

      consider p be POINT of S such that

       A3: between (c,d,p) & (c,p) equiv (a,b) by A1, Satz5p5;

      consider q be POINT of S such that

       A4: between (a,q,b) & (c,d) equiv (a,q) by A1;

      consider r be POINT of S such that

       A5: between (d,c,r) & (c,r) equiv (a,b) by GTARSKI1:def 8;

      

       A6: c = y implies (a,b) equiv (c,d)

      proof

        assume

         A7: c = y;

        then a = b by A2, GTARSKI1:def 7;

        then a = q by A4, GTARSKI1:def 10;

        hence thesis by A7, A2, A4, GTARSKI1:def 7;

      end;

      c <> y implies (a,b) equiv (c,d)

      proof

        assume

         A8: c <> y;

        

         A9: between (d,y,c) & between (p,d,c) by A2, A3, Satz3p2;

        

         A10: r <> c

        proof

          assume r = c;

          then a = b by A5, Satz2p2, GTARSKI1:def 7;

          hence contradiction by A2, Satz2p2, A8, GTARSKI1:def 7;

        end;

        

         A11: between (r,c,y)

        proof

           between (y,c,r) by A5, A9, Satz3p6p1;

          hence thesis by Satz3p2;

        end;

        

         A12: c <> d by A2, A8, GTARSKI1:def 10;

        

         A13: between (r,c,p)

        proof

           between (r,c,d) by A5, Satz3p2;

          hence thesis by A3, A12, Satz3p7p2;

        end;

        (c,y) equiv (a,b) by A2, Satz2p2;

        then y = p by A3, A10, A11, A13, Satz2p12;

        then between (d,p,c) & between (p,d,c) by A2, A3, Satz3p2;

        then p = d by Satz3p4;

        hence thesis by A3, Satz2p2;

      end;

      hence thesis by A6;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:64

    

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

    proof

      consider x be POINT of S such that

       A1: between (b,a,x) & (a,x) equiv (c,d) by GTARSKI1:def 8;

      consider y be POINT of S such that

       A2: between (x,a,y) & (a,y) equiv (c,d) by GTARSKI1:def 8;

      

       A3: x = a implies (a,b) <= (c,d) or (c,d) <= (a,b)

      proof

        assume x = a;

        then

         A4: c = d by A1, Satz2p2, GTARSKI1:def 7;

        ex q be POINT of S st between (c,c,q) & (c,q) equiv (a,b) by GTARSKI1:def 8;

        hence thesis by A4, Satz5p5;

      end;

      x <> a implies (a,b) <= (c,d) or (c,d) <= (a,b)

      proof

        assume

         A5: x <> a;

        

         A6: between (x,a,b) by A1, Satz3p2;

        then

         A7: between (x,y,b) or between (x,b,y) by A2, A5, Satz5p1;

         between (x,y,b) implies (c,d) <= (a,b)

        proof

          assume between (x,y,b);

          then between (a,y,b) by A2, Satz3p6p1;

          hence thesis by A2, Satz2p2;

        end;

        hence thesis by A2, A6, A7, Satz3p6p1, Satz5p5;

      end;

      hence thesis by A3;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:65

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

    proof

      ex x be POINT of S st between (a,a,x) & (a,x) equiv (b,c) by GTARSKI1:def 8;

      hence thesis by Satz5p5;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:66

    for S be satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct holds for a,b,c,d be POINT of S holds (a,b) <= (c,d) implies (b,a) <= (c,d) by Satz2p4;

    ::$Notion-Name

    theorem :: GTARSKI3:67

    

     Lemma5p12p2: (a,b) <= (c,d) implies (a,b) <= (d,c)

    proof

      assume (a,b) <= (c,d);

      then ex x be POINT of S st between (a,b,x) & (a,x) equiv (c,d) by Satz5p5;

      hence thesis by Satz2p5, Satz5p5;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:68

    

     Lemma5p12p3: between (a,b,c) & (a,c) equiv (a,b) implies c = b

    proof

      assume

       A1: between (a,b,c) & (a,c) equiv (a,b);

      then

       A2: between (c,b,a) by Satz3p2;

      

       A3: (c,b,a) cong (b,c,a)

      proof

        

         A4: (c,a) equiv (a,b) by A1, Satz2p4;

        (a,b) equiv (a,c) by A1, Satz2p2;

        then (b,a) equiv (a,c) by Satz2p4;

        hence thesis by A4, Satz2p5, GTARSKI1:def 5;

      end;

       between (b,c,a) by A2, A3, Satz4p6;

      hence thesis by A2, Satz3p4;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:69

    

     Lemma5p12p4: between (a,c,b) & (a,b) <= (a,c) implies b = c

    proof

      assume

       A1: between (a,c,b) & (a,b) <= (a,c);

      then

      consider x be POINT of S such that

       A2: between (a,b,x) & (a,x) equiv (a,c) by Satz5p5;

      c = x by A1, A2, Lemma5p12p3, Satz3p6p2;

      hence thesis by A1, A2, Satz3p6p1, GTARSKI1:def 10;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:70

    

     Satz5p12: Collinear (a,b,c) implies ( between (a,b,c) iff ((a,b) <= (a,c) & (b,c) <= (a,c)))

    proof

      assume

       A1: Collinear (a,b,c);

      thus between (a,b,c) implies (a,b) <= (a,c) & (b,c) <= (a,c)

      proof

        assume

         A2: between (a,b,c);

        hence (a,b) <= (a,c) by Satz2p1;

        thus (b,c) <= (a,c)

        proof

           between (c,b,a) by A2, Satz3p2;

          then (c,b) <= (c,a) by Satz2p1;

          then (b,c) <= (c,a) by Satz2p4;

          hence thesis by Lemma5p12p2;

        end;

      end;

      thus (a,b) <= (a,c) & (b,c) <= (a,c) implies between (a,b,c)

      proof

        assume

         A3: (a,b) <= (a,c) & (b,c) <= (a,c);

        

         A4: between (c,a,b) implies between (a,b,c)

        proof

          assume

           A5: between (c,a,b);

          (c,b) <= (a,c) by A3, Satz2p4;

          then a = b by A5, Lemma5p12p2, Lemma5p12p4;

          hence thesis by Satz3p1, Satz3p2;

        end;

         between (b,c,a) implies between (a,b,c)

        proof

          assume between (b,c,a);

          then b = c by A3, Satz3p2, Lemma5p12p4;

          hence thesis by Satz3p1;

        end;

        hence thesis by A1, A4;

      end;

    end;

    begin

    definition

      let S be TarskiGeometryStruct;

      let a,b,p be POINT of S;

      :: GTARSKI3:def8

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

    end

    reserve p for POINT of S;

    ::$Notion-Name

    theorem :: GTARSKI3:71

    

     Satz6p2: a <> p & b <> p & c <> p & between (a,p,c) implies ( between (b,p,c) iff p out (a,b))

    proof

      assume

       A1: a <> p & b <> p & c <> p & between (a,p,c);

      thus between (b,p,c) implies p out (a,b)

      proof

        assume between (b,p,c);

        then between (c,p,b) & between (c,p,a) by A1, Satz3p2;

        hence thesis by A1, Satz5p2;

      end;

      thus p out (a,b) implies between (b,p,c)

      proof

        assume

         A2: p out (a,b);

        

         A3: between (p,a,b) implies between (b,p,c)

        proof

          assume between (p,a,b);

          then between (b,a,p) by Satz3p2;

          hence thesis by A1, Satz3p7p1;

        end;

         between (p,b,a) implies between (b,p,c)

        proof

          assume between (p,b,a);

          then between (a,b,p) by Satz3p2;

          hence thesis by A1, Satz3p6p1;

        end;

        hence thesis by A2, A3;

      end;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:72

    

     Satz6p3: p out (a,b) iff (a <> p & b <> p & (ex c st c <> p & between (a,p,c) & between (b,p,c)))

    proof

      thus p out (a,b) implies (a <> p & b <> p & (ex c st (c <> p & between (a,p,c) & between (b,p,c))))

      proof

        assume

         A1: p out (a,b);

        consider c be POINT of S such that

         A2: between (a,p,c) & (p,c) equiv (p,a) by GTARSKI1:def 8;

        

         A3: p <> c by A1, A2, Satz2p2, GTARSKI1:def 7;

        

         A4: between (p,a,b) implies (ex c st (c <> p & between (a,p,c) & between (b,p,c)))

        proof

          assume between (p,a,b);

           between (b,p,c) by A1, A2, A3, Satz6p2;

          hence thesis by A2, A3;

        end;

         between (p,b,a) implies (ex c st (c <> p & between (a,p,c) & between (b,p,c)))

        proof

          assume between (p,b,a);

           between (b,p,c) by A1, A2, A3, Satz6p2;

          hence thesis by A2, A3;

        end;

        hence thesis by A1, A4;

      end;

      thus a <> p & b <> p & (ex c st (c <> p & between (a,p,c) & between (b,p,c))) implies p out (a,b) by Satz6p2;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:73

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

    proof

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

      proof

        assume

         A1: p out (a,b);

         between (p,b,a) implies Collinear (a,p,b) & not between (a,p,b)

        proof

          assume between (p,b,a);

          hence Collinear (a,p,b);

          thus not between (a,p,b)

          proof

            assume

             A2: between (a,p,b);

            then between (b,p,a) by Satz3p2;

            hence contradiction by A1, A2, Satz3p4;

          end;

        end;

        hence thesis by Satz3p2, Satz3p4, A1;

      end;

      hence thesis by Satz3p1, Satz3p2;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:74

    a <> p implies p out (a,a) by Satz3p1;

    ::$Notion-Name

    theorem :: GTARSKI3:75

    p out (a,b) implies p out (b,a);

    ::$Notion-Name

    theorem :: GTARSKI3:76

    p out (a,b) & p out (b,c) implies p out (a,c) by Satz3p6p2, Satz5p3, Satz5p1;

    ::$Notion-Name

    theorem :: GTARSKI3:77

    

     Lemmapsegcon2: ex x be POINT of S st ( between (p,a,x) or between (p,x,a)) & (p,x) equiv (b,c)

    proof

      set q = p;

      consider r be POINT of S such that

       A1: between (a,q,r) & (q,r) equiv (a,q) by GTARSKI1:def 8;

      consider x be POINT of S such that

       A2: between (r,q,x) & (q,x) equiv (b,c) by GTARSKI1:def 8;

      

       A3: r = q implies (( between (q,a,x) or between (q,x,a)) & (q,x) equiv (b,c)) by A1, A2, Satz2p2, GTARSKI1:def 7;

      r <> q implies (( between (q,a,x) or between (q,x,a)) & (q,x) equiv (b,c))

      proof

        assume

         A4: r <> q;

         between (r,q,a) by A1, Satz3p2;

        hence thesis by A2, A4, Satz5p2;

      end;

      hence thesis by A3;

    end;

    reserve r for POINT of S;

    ::$Notion-Name

    theorem :: GTARSKI3:78

    r <> a & b <> c implies ex x be POINT of S st (a out (x,r) & (a,x) equiv (b,c))

    proof

      assume

       A1: r <> a & b <> c;

      consider x be POINT of S such that

       A2: ( between (a,r,x) or between (a,x,r)) & (a,x) equiv (b,c) by Lemmapsegcon2;

      a out (x,r) by A1, A2, Satz2p2, GTARSKI1:def 7;

      hence thesis by A2;

    end;

    definition

      let S be TarskiGeometryStruct;

      let a,p be POINT of S;

      :: GTARSKI3:def9

      func halfline (p,a) -> set equals { x where x be POINT of S : p out (x,a) };

      coherence ;

    end

    reserve x,y for POINT of S;

    ::$Notion-Name

    theorem :: GTARSKI3:79

    

     Satz6p11pb: r <> a & b <> c & (a out (x,r) & (a,x) equiv (b,c)) & (a out (y,r) & (a,y) equiv (b,c)) implies x = y

    proof

      assume

       A1: r <> a & b <> c & (a out (x,r) & (a,x) equiv (b,c)) & (a out (y,r) & (a,y) equiv (b,c));

      consider s be POINT of S such that

       A2: s <> a & between (x,a,s) & between (r,a,s) by A1, Satz6p3;

      consider t be POINT of S such that

       A3: t <> a & between (y,a,t) & between (r,a,t) by A1, Satz6p3;

      

       A4: between (a,s,t) implies x = y

      proof

        assume between (a,s,t);

        then between (x,s,t) & between (x,a,t) by A2, Satz3p7p1, Satz3p7p2;

        then between (t,a,x) & between (t,a,y) by A3, Satz3p2;

        hence thesis by A1, A3, Satz2p12;

      end;

       between (a,t,s) implies x = y

      proof

        assume between (a,t,s);

        then between (y,t,s) & between (y,a,s) by A3, Satz3p7p1, Satz3p7p2;

        then between (s,a,y) & between (s,a,x) by A2, Satz3p2;

        hence thesis by A1, A2, Satz2p12;

      end;

      hence thesis by A4, A1, A2, A3, Satz5p2;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:80

    

     Satz6p13: p out (a,b) implies ((p,a) <= (p,b) iff between (p,a,b))

    proof

      assume

       A1: p out (a,b);

      

       A2: (p,a) <= (p,b) implies between (p,a,b)

      proof

        assume

         A3: (p,a) <= (p,b);

        consider y be POINT of S such that

         A4: between (p,y,b) & (p,a) equiv (p,y) by A3;

        

         A5: p out (y,b) by A1, A4, GTARSKI1:def 7;

        (p,y) equiv (p,y) by Satz2p1;

        hence thesis by A4, A1, A5, Satz6p11pb;

      end;

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

      proof

        assume

         A6: between (p,a,b);

        then Collinear (p,a,b);

        hence thesis by A6, Satz5p12;

      end;

      hence thesis by A2;

    end;

    ::$Notion-Name

    definition

      let S be non empty TarskiGeometryStruct;

      let p,q be POINT of S;

      :: GTARSKI3:def10

      func Line (p,q) -> Subset of S equals { x where x be POINT of S : Collinear (p,q,x) };

      coherence

      proof

        set X = { x where x be POINT of S : Collinear (p,q,x) };

        X c= the carrier of S

        proof

          let x be object;

          assume x in X;

          then ex y be POINT of S st x = y & Collinear (p,q,y);

          hence thesis;

        end;

        hence thesis;

      end;

    end

    reserve S for non empty satisfying_Tarski-model TarskiGeometryStruct;

    reserve p,q,r,s for POINT of S;

    ::$Notion-Name

    theorem :: GTARSKI3:81

    p <> q & p <> r & between (q,p,r) implies ( Line (p,q)) = ((( halfline (p,q)) \/ {p}) \/ ( halfline (p,r)))

    proof

      assume that

       A1A: p <> q and

       A1B: p <> r and

       A1C: between (q,p,r);

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

      proof

        let t be object;

        assume t in ( Line (p,q));

        then

        consider x be Element of S such that

         A2: t = x & Collinear (p,q,x);

        

         A3: between (q,x,p) & p <> x implies x in ( halfline (p,q))

        proof

          assume between (q,x,p) & p <> x;

          then p out (x,q) by A1A, Satz3p2;

          hence thesis;

        end;

        

         A4: between (x,p,q) & x = q implies p = x by GTARSKI1:def 10;

        

         A5: between (x,p,q) & p <> x & x <> q implies x in ( halfline (p,r))

        proof

          assume

           A6: between (x,p,q) & p <> x & x <> q;

          then between (q,p,r) & between (q,p,x) by A1C, Satz3p2;

          then p out (x,r) by A1A, A1B, A6, Satz5p2;

          hence thesis;

        end;

         between (p,q,x) & p <> x implies x in ( halfline (p,q))

        proof

          assume between (p,q,x) & p <> x;

          then p out (x,q) by A1A;

          hence thesis;

        end;

        then (x in ( halfline (p,q)) or x in {p}) or x in ( halfline (p,r)) by A2, A3, A5, A4, TARSKI:def 1;

        then (x in (( halfline (p,q)) \/ {p})) or x in ( halfline (p,r)) by XBOOLE_0:def 3;

        hence thesis by A2, XBOOLE_0:def 3;

      end;

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

      proof

        let t be object;

        assume t in ((( halfline (p,q)) \/ {p}) \/ ( halfline (p,r)));

        then t in (( halfline (p,q)) \/ {p}) or t in ( halfline (p,r)) by XBOOLE_0:def 3;

        then t in ( halfline (p,q)) or t in {p} or t in ( halfline (p,r)) by XBOOLE_0:def 3;

        per cases by TARSKI:def 1;

          suppose t in ( halfline (p,q));

          then

          consider x be POINT of S such that

           A7: t = x & p out (x,q);

           Collinear (p,q,x) by A7, Satz3p2;

          hence thesis by A7;

        end;

          suppose

           A8: t = p;

          then

          reconsider x = t as POINT of S;

           Collinear (p,q,p) by Satz3p1;

          hence thesis by A8;

        end;

          suppose t in ( halfline (p,r));

          then

          consider x be POINT of S such that

           A9: t = x & p out (x,r);

          

           A10: between (p,x,r) implies between (p,q,x) or between (q,x,p) or between (x,p,q)

          proof

            assume between (p,x,r);

            then between (q,p,x) by A1C, Satz3p5p1;

            hence thesis by Satz3p2;

          end;

           between (p,r,x) implies between (p,q,x) or between (q,x,p) or between (x,p,q)

          proof

            assume between (p,r,x);

            then between (q,p,x) by A1B, A1C, Satz3p7p2;

            hence thesis by Satz3p2;

          end;

          then Collinear (p,q,x) by A9, A10;

          hence thesis by A9;

        end;

      end;

    end;

    definition

      let S be non empty TarskiGeometryStruct;

      let A be Subset of S;

      :: GTARSKI3:def11

      pred A is_line means ex p,q be POINT of S st p <> q & A = ( Line (p,q));

    end

    ::$Notion-Name

    theorem :: GTARSKI3:82

    p <> q & s <> p & s in ( Line (p,q)) implies ( Line (p,q)) = ( Line (p,s))

    proof

      assume that

       A1A: p <> q and

       A1B: s <> p and

       A1C: s in ( Line (p,q));

      consider x be POINT of S such that

       A2: s = x & Collinear (p,q,x) by A1C;

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

      proof

        let t be object;

        assume t in ( Line (p,q));

        then

        consider y be POINT of S such that

         A3: t = y & Collinear (p,q,y);

        

         A4: between (p,q,y) implies between (p,s,y) or between (s,y,p) or between (y,p,s)

        proof

          assume

           A5: between (p,q,y);

          

           A6: between (p,q,s) implies between (p,s,y) or between (s,y,p) or between (y,p,s)

          proof

            assume between (p,q,s);

            then between (p,y,s) or between (p,s,y) by A1A, A5, Satz5p1;

            hence thesis by Satz3p2;

          end;

          

           A7: between (q,s,p) implies between (p,s,y) or between (s,y,p) or between (y,p,s)

          proof

            assume between (q,s,p);

            then between (p,s,q) by Satz3p2;

            hence thesis by A5, Satz3p6p2;

          end;

           between (s,p,q) implies between (p,s,y) or between (s,y,p) or between (y,p,s)

          proof

            assume between (s,p,q);

            then between (s,p,y) by A1A, A5, Satz3p7p2;

            hence thesis by Satz3p2;

          end;

          hence thesis by A2, A6, A7;

        end;

        

         A8: between (q,y,p) implies between (p,s,y) or between (s,y,p) or between (y,p,s)

        proof

          assume between (q,y,p);

          then

           A9: between (p,y,q) by Satz3p2;

          

           A10: between (p,q,s) implies between (p,s,y) or between (s,y,p) or between (y,p,s)

          proof

            assume between (p,q,s);

            then between (p,y,s) by A9, Satz3p6p2;

            hence thesis by Satz3p2;

          end;

          

           A11: between (q,s,p) implies between (p,s,y) or between (s,y,p) or between (y,p,s)

          proof

            assume between (q,s,p);

            then between (p,s,q) by Satz3p2;

            then between (p,s,y) or between (p,y,s) by A9, Satz5p3;

            hence thesis by Satz3p2;

          end;

           between (s,p,q) implies between (p,s,y) or between (s,y,p) or between (y,p,s)

          proof

            assume between (s,p,q);

            then between (s,p,y) by A9, Satz3p5p1;

            hence thesis by Satz3p2;

          end;

          hence thesis by A2, A10, A11;

        end;

         between (y,p,q) implies between (p,s,y) or between (s,y,p) or between (y,p,s)

        proof

          assume

           A12: between (y,p,q);

          

           A13: between (q,s,p) implies between (p,s,y) or between (s,y,p) or between (y,p,s)

          proof

            assume

             A14: between (q,s,p);

             between (q,p,y) by A12, Satz3p2;

            then between (s,p,y) by A14, Satz3p6p1;

            hence thesis by Satz3p2;

          end;

           between (s,p,q) implies between (p,s,y) or between (s,y,p) or between (y,p,s)

          proof

            assume between (s,p,q);

            then between (q,p,s) & between (q,p,y) by A12, Satz3p2;

            then between (p,s,y) or between (p,y,s) by A1A, Satz5p2;

            hence thesis by Satz3p2;

          end;

          hence thesis by A2, A12, A1A, Satz3p7p2, A13;

        end;

        then Collinear (p,s,y) by A4, A8, A3;

        hence thesis by A3;

      end;

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

      proof

        let t be object;

        assume t in ( Line (p,s));

        then

        consider y be POINT of S such that

         A15: t = y & Collinear (p,s,y);

        

         A16: between (p,s,y) implies between (p,q,y) or between (q,y,p) or between (y,p,q)

        proof

          assume

           A17: between (p,s,y);

          

           A18: between (q,s,p) implies between (p,q,y) or between (q,y,p) or between (y,p,q)

          proof

            assume between (q,s,p);

            then between (p,s,q) by Satz3p2;

            then between (p,q,y) or between (p,y,q) by A17, A1B, Satz5p1;

            hence thesis by Satz3p2;

          end;

           between (s,p,q) implies between (p,q,y) or between (q,y,p) or between (y,p,q)

          proof

            assume between (s,p,q);

            then between (q,p,s) by Satz3p2;

            then between (q,p,y) by A1B, A17, Satz3p7p2;

            hence thesis by Satz3p2;

          end;

          hence thesis by A17, Satz3p6p2, A18, A2;

        end;

        

         A19: between (s,y,p) implies between (p,q,y) or between (q,y,p) or between (y,p,q)

        proof

          assume

           A20: between (s,y,p);

          

           A21: between (p,q,s) implies between (p,q,y) or between (q,y,p) or between (y,p,q)

          proof

            assume

             A22: between (p,q,s);

             between (p,y,s) by A20, Satz3p2;

            then between (p,q,y) or between (p,y,q) by A22, Satz5p3;

            hence thesis by Satz3p2;

          end;

          

           A23: between (q,s,p) implies between (p,q,y) or between (q,y,p) or between (y,p,q)

          proof

            assume between (q,s,p);

            then

             A25: between (p,s,q) by Satz3p2;

             between (p,y,s) by A20, Satz3p2;

            then between (p,y,q) by A25, Satz3p6p2;

            hence thesis by Satz3p2;

          end;

           between (s,p,q) implies between (p,q,y) or between (q,y,p) or between (y,p,q)

          proof

            assume between (s,p,q);

            then

             A26: between (q,p,s) by Satz3p2;

             between (p,y,s) by A20, Satz3p2;

            then between (q,p,y) by A26, Satz3p5p1;

            hence thesis by Satz3p2;

          end;

          hence thesis by A21, A23, A2;

        end;

         between (y,p,s) implies between (p,q,y) or between (q,y,p) or between (y,p,q)

        proof

          assume

           A27: between (y,p,s);

          

           A28: between (q,s,p) implies between (p,q,y) or between (q,y,p) or between (y,p,q)

          proof

            assume between (q,s,p);

            then between (p,s,q) by Satz3p2;

            hence thesis by A27, A1B, Satz3p7p2;

          end;

           between (s,p,q) implies between (p,q,y) or between (q,y,p) or between (y,p,q)

          proof

            assume

             A29: between (s,p,q);

             between (s,p,y) by A27, Satz3p2;

            then between (p,q,y) or between (p,y,q) by Satz5p2, A29, A1B;

            hence thesis by Satz3p2;

          end;

          hence thesis by A27, Satz3p5p1, A28, A2;

        end;

        then Collinear (p,q,y) by A15, A16, A19;

        hence thesis by A15;

      end;

    end;

    reserve S for non empty satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct,

a,b,p,q for POINT of S;

    ::$Notion-Name

    theorem :: GTARSKI3:83

    

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

    proof

      thus p in ( Line (p,q))

      proof

         Collinear (p,q,p) by Satz3p1;

        hence thesis;

      end;

       Collinear (p,q,q) by Satz3p1;

      hence q in ( Line (p,q));

      thus ( Line (p,q)) = ( Line (q,p))

      proof

        

         A2: ( Line (p,q)) c= ( Line (q,p))

        proof

          let x be object;

          assume x in ( Line (p,q));

          then

          consider y be POINT of S such that

           A3: y = x and

           A4: Collinear (p,q,y);

           Collinear (q,p,y) by A4, Satz3p2;

          hence thesis by A3;

        end;

        ( Line (q,p)) c= ( Line (p,q))

        proof

          let x be object;

          assume x in ( Line (q,p));

          then

          consider y be POINT of S such that

           A5: y = x and

           A6: Collinear (q,p,y);

           Collinear (p,q,y) by A6, Satz3p2;

          hence thesis by A5;

        end;

        hence thesis by A2;

      end;

    end;

    reserve S for non empty satisfying_Tarski-model TarskiGeometryStruct,

A,B for Subset of S,

a,b,c,p,q,r,s for POINT of S;

    theorem :: GTARSKI3:84

    

     Thequiv1: for S be satisfying_Tarski-model TarskiGeometryStruct holds for a,b,c be Element of S holds (a <> b & Collinear (a,b,c)) iff c on_line (a,b);

    theorem :: GTARSKI3:85

    

     Thequiv2: for S be satisfying_Tarski-model non empty TarskiGeometryStruct holds for a,b,x,y be POINT of S st (a,b) equal_line (x,y) holds ( Line (a,b)) = ( Line (x,y))

    proof

      let S be satisfying_Tarski-model non empty TarskiGeometryStruct;

      let a,b,x,y be POINT of S;

      assume

       A1: (a,b) equal_line (x,y);

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

      proof

        

         A2: ( Line (a,b)) c= ( Line (x,y))

        proof

          let z be object;

          assume z in ( Line (a,b));

          then

          consider z9 be POINT of S such that

           A3: z = z9 and

           A4: Collinear (a,b,z9);

          z9 on_line (x,y) by A1, A4, Thequiv1;

          then Collinear (x,y,z9);

          hence z in ( Line (x,y)) by A3;

        end;

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

        proof

          let z be object;

          assume z in ( Line (x,y));

          then

          consider z9 be POINT of S such that

           A5: z = z9 and

           A6: Collinear (x,y,z9);

          z9 on_line (a,b) by A6, A1, Thequiv1;

          then Collinear (a,b,z9);

          hence thesis by A5;

        end;

        hence thesis by A2;

      end;

      hence thesis;

    end;

    theorem :: GTARSKI3:86

    for S be satisfying_Tarski-model non empty TarskiGeometryStruct holds for a,b,x,y be POINT of S st a <> b & x <> y & ( Line (a,b)) = ( Line (x,y)) holds (a,b) equal_line (x,y)

    proof

      let S be satisfying_Tarski-model non empty TarskiGeometryStruct;

      let a,b,x,y be POINT of S;

      assume that

       A1: a <> b and

       A1A: x <> y and

       A2: ( Line (a,b)) = ( Line (x,y));

      for c be POINT of S holds c on_line (a,b) iff c on_line (x,y)

      proof

        let c be POINT of S;

        hereby

          assume c on_line (a,b);

          then Collinear (a,b,c);

          then c in ( Line (x,y)) by A2;

          then ex z be POINT of S st c = z & Collinear (x,y,z);

          hence c on_line (x,y) by A1A;

        end;

        assume c on_line (x,y);

        then Collinear (x,y,c);

        then c in ( Line (a,b)) by A2;

        then ex z be POINT of S st c = z & Collinear (a,b,z);

        hence c on_line (a,b) by A1;

      end;

      hence thesis by A1, A1A;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:87

    

     Satz6p18: A is_line & a <> b & a in A & b in A implies A = ( Line (a,b))

    proof

      assume that

       A1: A is_line and

       A2: a <> b and

       A3: a in A and

       A4: b in A;

      consider p, q such that

       A5: p <> q and

       A6: A = ( Line (p,q)) by A1;

      consider xa be POINT of S such that

       A7: a = xa and

       A8: Collinear (p,q,xa) by A3, A6;

      consider xb be POINT of S such that

       A9: b = xb and

       A10: Collinear (p,q,xb) by A4, A6;

      a on_line (p,q) & b on_line (p,q) by A5, A7, A8, A9, A10;

      hence thesis by A2, A6, Thequiv2, GTARSKI1: 46;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:88

    

     Satz6p19: a <> b & A is_line & a in A & b in A & B is_line & a in B & b in B implies A = B

    proof

      assume that

       A1: a <> b and

       A2: A is_line and

       A3: a in A and

       A4: b in A and

       A5: B is_line and

       A6: a in B and

       A7: b in B;

      consider pa,qa be POINT of S such that pa <> qa and

       A8: A = ( Line (pa,qa)) by A2;

      consider pb,qb be POINT of S such that pb <> qb and

       A9: B = ( Line (pb,qb)) by A5;

      ( Line (pa,qa)) = ( Line (a,b)) & ( Line (pb,qb)) = ( Line (a,b)) by A1, A3, A4, A8, A2, A6, A7, A9, A5, Satz6p18;

      hence thesis by A8, A9;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:89

    A is_line & B is_line & A <> B & a in A & a in B & b in A & b in B implies a = b by Satz6p19;

    ::$Notion-Name

    theorem :: GTARSKI3:90

    (ex p, q st p <> q) implies ( Collinear (a,b,c) iff (ex A st A is_line & a in A & b in A & c in A))

    proof

      assume ex p, q st p <> q;

      then

      consider p, q such that

       A1: p <> q;

      

       A2: (ex A st A is_line & a in A & b in A & c in A) implies Collinear (a,b,c)

      proof

        assume ex A st A is_line & a in A & b in A & c in A;

        then

        consider A such that

         A3: A is_line and

         A4: a in A and

         A5: b in A and

         A6: c in A;

        per cases ;

          suppose a <> b;

          then c in ( Line (a,b)) by A3, A4, A5, A6, Satz6p18;

          then ex x st c = x & Collinear (a,b,x);

          hence thesis;

        end;

          suppose a = b;

          hence thesis by Satz3p1;

        end;

      end;

       Collinear (a,b,c) implies (ex A st A is_line & a in A & b in A & c in A)

      proof

        assume

         A8: Collinear (a,b,c);

        per cases ;

          suppose

           A9: a = b;

          per cases ;

            suppose

             A10: a = c;

            per cases by A1;

              suppose

               A11: a <> p;

              set A = ( Line (a,p));

              now

                thus A is_line by A11;

                 Collinear (a,p,a) by Satz3p1;

                hence a in A & b in A & c in A by A9, A10;

              end;

              hence ex A st A is_line & a in A & b in A & c in A;

            end;

              suppose

               A12: a <> q;

              set A = ( Line (a,q));

              now

                thus A is_line by A12;

                 Collinear (a,q,a) by Satz3p1;

                hence a in A & b in A & c in A by A9, A10;

              end;

              hence ex A st A is_line & a in A & b in A & c in A;

            end;

          end;

            suppose

             A13: a <> c;

            set A = ( Line (a,c));

            now

              thus A is_line by A13;

               Collinear (a,c,a) & Collinear (a,c,c) by Satz3p1;

              hence a in A & b in A & c in A by A9;

            end;

            hence ex A st A is_line & a in A & b in A & c in A;

          end;

        end;

          suppose

           A14: a <> b;

           Collinear (a,b,a) & Collinear (a,b,b) by Satz3p1;

          then

           A15: a in ( Line (a,b)) & b in ( Line (a,b)) & c in ( Line (a,b)) by A8;

          reconsider A = ( Line (a,b)) as Subset of S;

          A is_line by A14;

          hence ex A st A is_line & a in A & b in A & c in A by A15;

        end;

      end;

      hence thesis by A2;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:91

    

     Satz6p24: for S be satisfying_A8 TarskiGeometryStruct holds ex a,b,c be POINT of S st not Collinear (a,b,c)

    proof

      let S be satisfying_A8 TarskiGeometryStruct;

      consider a,b,c be POINT of S such that

       A1: not between (a,b,c) and

       A2: not between (b,c,a) and

       A3: not between (c,a,b) by GTARSKI2:def 7;

       not Collinear (a,b,c) by A1, A2, A3;

      hence thesis;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:92

    for S be non empty satisfying_Tarski-model TarskiGeometryStruct holds for a,b be POINT of S st S is satisfying_A8 & a <> b holds ex c be POINT of S st not Collinear (a,b,c)

    proof

      let S be non empty satisfying_Tarski-model TarskiGeometryStruct;

      let a,b be POINT of S;

      assume that

       A1: S is satisfying_A8 and

       A2: a <> b;

      assume

       A3: for c be POINT of S holds Collinear (a,b,c);

      consider a9,b9,c9 be POINT of S such that

       A4: not Collinear (a9,b9,c9) by A1, Satz6p24;

      

       A5: a9 <> b9 by A4, Satz3p1;

      set A = ( Line (a,b));

       Collinear (a,b,a9) & Collinear (a,b,b9) by A3;

      then A is_line & a9 in A & b9 in A by A2;

      then

       A6: ( Line (a9,b9)) = A by A5, Satz6p18;

       Collinear (a,b,c9) by A3;

      then c9 in ( Line (a9,b9)) by A6;

      then ex x be POINT of S st c9 = x & Collinear (a9,b9,x);

      hence contradiction by A4;

    end;

    theorem :: GTARSKI3:93

    

     Satz6p28Lem01: for S be satisfying_Tarski-model TarskiGeometryStruct holds for p,a,b be POINT of S st p out (a,b) & (p,a) <= (p,b) holds between (p,a,b) by Satz6p13;

    theorem :: GTARSKI3:94

    

     Satz6p28Lem02: for S be satisfying_Tarski-model TarskiGeometryStruct holds for a,b,c,d,e,f,g,h be 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

      let S be satisfying_Tarski-model TarskiGeometryStruct;

      let a,b,c,d,e,f,g,h be Element of S;

      (a,b) <= (c,d) or (c,d) <= (a,b) by Satz5p10;

      hence thesis by Satz5p6;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:95

    for S be satisfying_Tarski-model TarskiGeometryStruct holds for a,b,c,a1,b1,c1 be 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

      let S be satisfying_Tarski-model TarskiGeometryStruct;

      let a,b,c,a1,b1,c1 be Element of S;

      assume that

       A1: b out (a,c) and

       A2: b1 out (a1,c1) and

       A3: (b,a) equiv (b1,a1) and

       A4: (b,c) equiv (b1,c1) and

       A5: not (a,c) equiv (a1,c1);

      now

        thus b out (c,a) by A1;

        thus b1 out (c1,a1) by A2;

        (b,a) equiv (a1,b1) & (b,c) equiv (c1,b1) & not (a,c) equiv (c1,a1) by Satz2p5, A3, A4, A5;

        hence not (c,a) equiv (c1,a1) & (a,b) equiv (a1,b1) & (c,b) equiv (c1,b1) by Satz2p4;

        hence not ( between (c,a,b) & between (c1,a1,b1)) & not ( between (a,c,b) & between (a1,c1,b1)) by Satz4p3, A5;

        thus ((b,a) <= (b,c) or (b1,c1) <= (b1,a1)) & ((b,c) <= (b,a) or (b1,a1) <= (b1,c1)) by A3, Satz6p28Lem02, A4;

      end;

      hence contradiction by Satz6p28Lem01, A1, A2, Satz3p2;

    end;

    begin

    definition

      let S be TarskiGeometryStruct;

      let a,b,m be POINT of S;

      :: GTARSKI3:def12

      pred Middle a,m,b means

      : DEFM: between (a,m,b) & (m,a) equiv (m,b);

    end

    reserve S for satisfying_CongruenceIdentity satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct,

a,b,m for POINT of S;

    ::$Notion-Name

    theorem :: GTARSKI3:96

     Middle (a,m,b) implies Middle (b,m,a) by Satz3p2, Satz2p2;

    reserve S for satisfying_CongruenceIdentity satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_SegmentConstruction satisfying_BetweennessIdentity TarskiGeometryStruct,

a,b,m for POINT of S;

    ::$Notion-Name

    theorem :: GTARSKI3:97

    

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

    ::$Notion-Name

    theorem :: GTARSKI3:98

    

     Satz7p4existence: for p be POINT of S holds ex p9 be POINT of S st Middle (p,a,p9)

    proof

      let p be POINT of S;

      per cases ;

        suppose p <> a;

        consider x be POINT of S such that

         A1: between (p,a,x) & (a,x) equiv (p,a) by GTARSKI1:def 8;

        (a,x) equiv (a,p) by A1, Satz2p5;

        then (a,p) equiv (a,x) by Satz2p2;

        hence thesis by A1, DEFM;

      end;

        suppose p = a;

        hence thesis by Satz7p3;

      end;

    end;

    reserve S for satisfying_CongruenceIdentity satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_SegmentConstruction satisfying_SAS TarskiGeometryStruct,

a for POINT of S;

    ::$Notion-Name

    theorem :: GTARSKI3:99

    

     Satz7p4uniqueness: for p,p1,p2 be POINT of S st Middle (p,a,p1) & Middle (p,a,p2) holds p1 = p2

    proof

      let p,p1,p2 be POINT of S;

      assume

       A1: Middle (p,a,p1) & Middle (p,a,p2);

      per cases ;

        suppose

         A2: p <> a;

        (a,p1) equiv (a,p) & (a,p2) equiv (a,p) by A1, Satz2p2;

        hence thesis by A1, A2, Satz2p12;

      end;

        suppose p = a;

        then a = p1 & a = p2 by A1, Satz2p2, GTARSKI1:def 7;

        hence thesis;

      end;

    end;

    definition

      let S be satisfying_CongruenceIdentity satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_SAS TarskiGeometryStruct;

      let a,p be POINT of S;

      :: GTARSKI3:def13

      func reflection (a,p) -> POINT of S means

      : DEFR: Middle (p,a,it );

      existence by Satz7p4existence;

      uniqueness by Satz7p4uniqueness;

    end

    reserve S for satisfying_CongruenceIdentity satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_SAS TarskiGeometryStruct,

a,p,p9 for POINT of S;

    ::$Notion-Name

    theorem :: GTARSKI3:100

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

    reserve S for satisfying_CongruenceIdentity satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_SAS satisfying_Pasch TarskiGeometryStruct,

a,p,p9 for POINT of S;

    ::$Notion-Name

    theorem :: GTARSKI3:101

    

     Satz7p7: ( reflection (a,( reflection (a,p)))) = p

    proof

       Middle (p,a,( reflection (a,p))) by DEFR;

      then Middle (( reflection (a,p)),a,p) by Satz3p2, Satz2p2;

      hence thesis by DEFR;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:102

    ex p st ( reflection (a,p)) = p9

    proof

      set p = ( reflection (a,p9));

      take p;

      thus thesis by Satz7p7;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:103

    

     Satz7p9: ( reflection (a,p)) = ( reflection (a,p9)) implies p = p9

    proof

      assume ( reflection (a,p)) = ( reflection (a,p9));

      then ( reflection (a,( reflection (a,p)))) = p9 by Satz7p7;

      hence thesis by Satz7p7;

    end;

    reserve S for satisfying_CongruenceIdentity satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_SAS TarskiGeometryStruct,

a,p for POINT of S;

    ::$Notion-Name

    theorem :: GTARSKI3:104

    

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

    proof

      hereby

        assume ( reflection (a,p)) = p;

        then Middle (p,a,p) by DEFR;

        hence p = a by GTARSKI1:def 10;

      end;

      assume p = a;

      then Middle (p,a,p) by Satz3p1, Satz2p1;

      hence thesis by DEFR;

    end;

    reserve S for satisfying_Tarski-model TarskiGeometryStruct,

a,b,c,d,m,p,p9,q,r,s for POINT of S;

    ::$Notion-Name

    theorem :: GTARSKI3:105

    

     Satz7p13: (p,q) equiv (( reflection (a,p)),( reflection (a,q)))

    proof

      reconsider p9 = ( reflection (a,p)), q9 = ( reflection (a,q)) as POINT of S;

      per cases ;

        suppose

         A1: p = a;

         Middle (q,a,( reflection (a,q))) by DEFR;

        hence thesis by A1, Satz7p10;

      end;

        suppose

         A2: p <> a;

        

         A3: Middle (p,a,p9) by DEFR;

        

         A4: Middle (q,a,q9) by DEFR;

        consider x be POINT of S such that

         A5: between (p9,p,x) and

         A6: (p,x) equiv (q,a) by GTARSKI1:def 8;

        consider y be POINT of S such that

         A7: between (q9,q,y) and

         A8: (q,y) equiv (p,a) by GTARSKI1:def 8;

        consider x9 be POINT of S such that

         A9: between (x,p9,x9) and

         A10: (p9,x9) equiv (q,a) by GTARSKI1:def 8;

        consider y9 be POINT of S such that

         A11: between (y,q9,y9) and

         A12: (q9,y9) equiv (p,a) by GTARSKI1:def 8;

        

         A13: between5 (x,p,a,p9,x9) & between5 (y,q,a,q9,y9)

        proof

          

           A14: between (x9,p9,x) by A9, Satz3p2;

           between (p9,a,p) by A3, Satz3p2;

          then between5 (x9,p9,a,p,x) by A5, A14, Satz3p11p3pb, Satz3p11p4pb;

          hence between5 (x,p,a,p9,x9) by Satz3p2;

          

           A15: between (y9,q9,y) by A11, Satz3p2;

           between (q9,a,q) by A4, Satz3p2;

          then between5 (y9,q9,a,q,y) by A7, A15, Satz3p11p3pb, Satz3p11p4pb;

          hence between5 (y,q,a,q9,y9) by Satz3p2;

        end;

        

         A16: (a,x) equiv (a,y)

        proof

          

           A17: (p,a) equiv (q,y) by A8, Satz2p2;

          (x,p) equiv (q,a) by A6, Satz2p4;

          then

           A18: (x,p) equiv (a,q) by Satz2p5;

           between (x,p,a) & between (a,q,y) by A13, Satz3p2;

          then (x,a) equiv (a,y) by A17, A18, Satz2p11;

          hence thesis by Satz2p4;

        end;

        

         A19: (a,y) equiv (a,x9)

        proof

          (q,a) equiv (p9,x9) by A10, Satz2p2;

          then (a,q) equiv (p9,x9) by Satz2p4;

          then

           A20: (a,q) equiv (x9,p9) by Satz2p5;

          (q,y) equiv (a,p) by A8, Satz2p5;

          then (q,y) equiv (a,p9) by A3, Satz2p3;

          then

           A21: (q,y) equiv (p9,a) by Satz2p5;

           between (a,q,y) & between (x9,p9,a) by A13, Satz3p2;

          then (a,y) equiv (x9,a) by A20, A21, Satz2p11;

          hence thesis by Satz2p5;

        end;

        

         A22: (a,x9) equiv (a,y9)

        proof

          (q,a) equiv (a,q9) by A4, Satz2p4;

          then (p9,x9) equiv (a,q9) by A10, Satz2p3;

          then

           A23: (x9,p9) equiv (a,q9) by Satz2p4;

          (p,a) equiv (a,p9) by A3, Satz2p4;

          then (q9,y9) equiv (a,p9) by A12, Satz2p3;

          then (a,p9) equiv (q9,y9) by Satz2p2;

          then

           A24: (p9,a) equiv (q9,y9) by Satz2p4;

           between (x9,p9,a) & between (a,q9,y9) by A13, Satz3p2;

          then (x9,a) equiv (a,y9) by A23, A24, Satz2p11;

          hence thesis by Satz2p4;

        end;

        

         A25: (x,a,x9,y9) AFS (y9,a,y,x)

        proof

          now

            thus between (x,a,x9) by A13;

            thus between (y9,a,y) by A13, Satz3p2;

            (a,x) equiv (a,x9) by A16, A19, Satz2p3;

            then

             A26: (a,x) equiv (a,y9) by A22, Satz2p3;

            hence (a,y9) equiv (a,x) by Satz2p2;

            (a,x) equiv (y9,a) by A26, Satz2p5;

            hence (x,a) equiv (y9,a) by Satz2p4;

            thus (a,x9) equiv (a,y) by A19, Satz2p2;

            thus (x,y9) equiv (y9,x) by Satz2p1, Satz2p5;

          end;

          hence thesis;

        end;

        

         A27: S is satisfying_SST_A5;

        x <> a by A13, A2, GTARSKI1:def 10;

        then

         A28: (x9,y9) equiv (y,x) by A27, A25;

        

         A29: (y,q,a,x) IFS (y9,q9,a,x9)

        proof

          now

            thus between (y,q,a) & between (y9,q9,a) by A13, Satz3p2;

            (a,y) equiv (a,y9) by A19, A22, Satz2p3;

            then (a,y) equiv (y9,a) by Satz2p5;

            hence (y,a) equiv (y9,a) by Satz2p4;

            (a,q) equiv (q9,a) by A4, Satz2p5;

            hence (q,a) equiv (q9,a) by Satz2p4;

            (y,x) equiv (x9,y9) by A28, Satz2p2;

            hence (y,x) equiv (y9,x9) by Satz2p5;

            thus (a,x) equiv (a,x9) by A16, A19, Satz2p3;

          end;

          hence thesis;

        end;

        (x,p,a,q) IFS (x9,p9,a,q9)

        proof

          now

            thus between (x,p,a) & between (x9,p9,a) by A13, Satz3p2;

            (a,x) equiv (a,x9) by A16, A19, Satz2p3;

            then (a,x) equiv (x9,a) by Satz2p5;

            hence (x,a) equiv (x9,a) by Satz2p4;

            (a,p) equiv (p9,a) by A3, Satz2p5;

            hence (p,a) equiv (p9,a) by Satz2p4;

            (q,x) equiv (x9,q9) by A29, Satz4p2, Satz2p5;

            hence (x,q) equiv (x9,q9) by Satz2p4;

            thus (a,q) equiv (a,q9) by A4;

          end;

          hence thesis;

        end;

        hence thesis by Satz4p2;

      end;

    end;

    

     Lemma7p15a: between (p,q,r) implies between (( reflection (a,p)),( reflection (a,q)),( reflection (a,r)))

    proof

      assume

       A1: between (p,q,r);

      (p,q,r) cong (( reflection (a,p)),( reflection (a,q)),( reflection (a,r))) by Satz7p13;

      hence between (( reflection (a,p)),( reflection (a,q)),( reflection (a,r))) by A1, Satz4p6;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:106

    

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

    proof

      now

        assume

         C1: between (( reflection (a,p)),( reflection (a,q)),( reflection (a,r)));

        ( reflection (a,( reflection (a,p)))) = p & ( reflection (a,( reflection (a,q)))) = q & ( reflection (a,( reflection (a,r)))) = r by Satz7p7;

        hence between (p,q,r) by C1, Lemma7p15a;

      end;

      hence thesis by Lemma7p15a;

    end;

    

     Lemma7p16a: (p,q) equiv (r,s) implies (( reflection (a,p)),( reflection (a,q))) equiv (( reflection (a,r)),( reflection (a,s)))

    proof

      assume

       A1: (p,q) equiv (r,s);

      

       A2: (r,s) equiv (( reflection (a,r)),( reflection (a,s))) by Satz7p13;

      (p,q) equiv (( reflection (a,p)),( reflection (a,q))) by Satz7p13;

      then (r,s) equiv (( reflection (a,p)),( reflection (a,q))) by A1, GTARSKI1:def 6;

      hence thesis by A2, GTARSKI1:def 6;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:107

    

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

    proof

      now

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

        ( reflection (a,( reflection (a,p)))) = p & ( reflection (a,( reflection (a,q)))) = q & ( reflection (a,( reflection (a,r)))) = r & ( reflection (a,( reflection (a,s)))) = s by Satz7p7;

        hence thesis by Lemma7p16a;

      end;

      hence thesis by Lemma7p16a;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:108

    

     Satz7p17: Middle (p,a,p9) & Middle (p,b,p9) implies a = b

    proof

      assume that

       A1: Middle (p,a,p9) and

       A2: Middle (p,b,p9);

      now

        thus between (p,b,p9) by A2;

        ( reflection (a,p)) = p9 by A1, DEFR;

        then (b,p9) equiv (( reflection (a,b)),( reflection (a,( reflection (a,p))))) by Satz7p13;

        then (b,p9) equiv (( reflection (a,b)),p) by Satz7p7;

        then (b,p) equiv (( reflection (a,b)),p) by A2, Satz2p3;

        hence (p,b) equiv (( reflection (a,b)),p) by Satz2p4;

        hence (p,b) equiv (p,( reflection (a,b))) by Satz2p5;

        (b,p) equiv (( reflection (a,b)),( reflection (a,p))) by Satz7p13;

        then (b,p) equiv (( reflection (a,b)),p9) by A1, DEFR;

        then (b,p9) equiv (( reflection (a,b)),p9) by A2, GTARSKI1:def 6;

        then (p9,b) equiv (( reflection (a,b)),p9) by Satz2p4;

        hence (p9,b) equiv (p9,( reflection (a,b))) by Satz2p5;

      end;

      then ( reflection (a,b)) = b by Satz4p19;

      hence thesis by Satz7p10;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:109

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

    proof

      assume

       A1: ( reflection (a,p)) = ( reflection (b,p));

       Middle (p,a,( reflection (a,p))) & Middle (p,b,( reflection (b,p))) by DEFR;

      hence thesis by A1, Satz7p17;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:110

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

    proof

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

      proof

        assume

         A1: ( reflection (b,( reflection (a,p)))) = ( reflection (a,( reflection (b,p))));

        set p9 = ( reflection (a,p));

        

         A2: Middle (p,a,p9) by DEFR;

         Middle (( reflection (b,p)),a,( reflection (b,p9))) by A1, DEFR;

        then Middle (( reflection (b,( reflection (b,p)))),( reflection (b,a)),( reflection (b,( reflection (b,p9))))) by Satz7p15, Satz7p16;

        then Middle (p,( reflection (b,a)),( reflection (b,( reflection (b,p9))))) by Satz7p7;

        then Middle (p,( reflection (b,a)),p9) by Satz7p7;

        hence thesis by A2, Satz7p17, Satz7p10;

      end;

      hence thesis;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:111

    

     Satz7p20: Collinear (a,m,b) & (m,a) equiv (m,b) implies a = b or Middle (a,m,b)

    proof

      assume that

       A1: Collinear (a,m,b) and

       A2: (m,a) equiv (m,b);

      assume

       A3: a <> b;

      per cases by A1;

        suppose between (a,m,b);

        hence thesis by A2;

      end;

        suppose between (m,b,a);

        then

         A4: between (a,b,m) by Satz3p2;

        

         A5: between (b,b,m) by Satz3p1, Satz3p2;

        (m,a) equiv (b,m) by A2, Satz2p5;

        then

         A6: (a,m) equiv (b,m) by Satz2p4;

        (b,m) equiv (b,m) by Satz2p1;

        hence thesis by A3, A4, A5, A6, Satz4p3, GTARSKI1:def 7;

      end;

        suppose

         A7: between (b,a,m);

        

         A8: between (a,a,m) by Satz3p1, Satz3p2;

        (m,a) equiv (b,m) by A2, Satz2p5;

        then (a,m) equiv (b,m) by Satz2p4;

        then

         A9: (b,m) equiv (a,m) by Satz2p2;

        (a,m) equiv (a,m) by Satz2p1;

        hence thesis by A3, A7, A8, A9, Satz4p3, GTARSKI1:def 7;

      end;

    end;

    reserve S for non empty satisfying_Tarski-model TarskiGeometryStruct,

a,b,c,d,p for POINT of S;

    ::$Notion-Name

    theorem :: GTARSKI3:112

     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) implies Middle (a,p,c) & Middle (b,p,d)

    proof

      assume that

       A1: not Collinear (a,b,c) and

       A2: b <> d and

       A3: (a,b) equiv (c,d) and

       A4: (b,c) equiv (d,a) and

       A5: Collinear (a,p,c) and

       A6: Collinear (b,p,d);

      

       A7: Collinear (b,d,p) by A6, Satz3p2;

      then

      consider p9 be POINT of S such that

       A8: (b,d,p) cong (d,b,p9) by GTARSKI1:def 5, Satz4p14;

      

       A9: Collinear (d,b,p9) by A7, A8, Satz4p13;

      now

        thus Collinear (b,d,p) by A6, Satz3p2;

        thus (b,d,p) cong (d,b,p9) by A8;

        (a,b) equiv (d,c) by A3, Satz2p5;

        hence (b,a) equiv (d,c) by Satz2p4;

        thus (d,a) equiv (b,c) by A4, Satz2p2;

      end;

      then

       A10: (b,d,p,a) FS (d,b,p9,c);

      then (p,a) equiv (c,p9) by A2, Satz4p16, Satz2p5;

      then

       A11: (a,p) equiv (c,p9) by Satz2p4;

      

       A12: (a,c) equiv (c,a) by GTARSKI1:def 5;

      now

        thus Collinear (b,d,p) by A6, Satz3p2;

        thus (b,d,p) cong (d,b,p9) by A8;

        thus (b,c) equiv (d,a) by A4;

        (a,b) equiv (d,c) by A3, Satz2p5;

        then (b,a) equiv (d,c) by Satz2p4;

        hence (d,c) equiv (b,a) by Satz2p2;

      end;

      then (b,d,p,c) FS (d,b,p9,a);

      then (p,c) equiv (p9,a) by A2, Satz4p16;

      then

       A13: Collinear (c,p9,a) by A5, Satz4p13, A11, A12, GTARSKI1:def 3;

      

       A14: a <> c by A1, Satz3p1;

      

       A15: ( Line (a,c)) <> ( Line (b,d))

      proof

        assume ( Line (a,c)) = ( Line (b,d));

        then b in ( Line (a,c)) by Satz6p17;

        then ex x be POINT of S st b = x & Collinear (a,c,x);

        hence contradiction by A1, Satz3p2;

      end;

      now

        thus ( Line (a,c)) <> ( Line (b,d)) by A15;

        thus ( Line (a,c)) is_line by A14;

        thus ( Line (b,d)) is_line by A2;

         Collinear (a,c,p9) by A13;

        hence p9 in ( Line (a,c));

         Collinear (b,d,p9) by A9, Satz3p2;

        hence p9 in ( Line (b,d));

         Collinear (a,c,p) by A5, Satz3p2;

        hence p in ( Line (a,c));

         Collinear (b,d,p) by A6, Satz3p2;

        hence p in ( Line (b,d));

      end;

      then

       A16: p9 = p by Satz6p19;

      now

        thus Middle (a,p,c) by A14, Satz7p20, A10, A2, Satz4p16, A16, A5;

        (b,p) equiv (p,d) by A16, A8, Satz2p5;

        hence Middle (b,p,d) by A2, Satz7p20, A6, Satz2p4;

      end;

      hence thesis;

    end;

    reserve a1,a2,b1,b2,m1,m2 for POINT of S;

    ::$Notion-Name

    theorem :: GTARSKI3:113

    

     Satz7p22part1: 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) implies between (m1,c,m2)

    proof

      assume that

       A1: between (a1,c,a2) and

       A2: between (b1,c,b2) and

       A3: (c,a1) equiv (c,b1) and

       A4: (c,a2) equiv (c,b2) and

       A5: Middle (a1,m1,b1) and

       A6: Middle (a2,m2,b2) and

       A7: (c,a1) <= (c,a2);

      per cases ;

        suppose

         A8: a2 = c;

        a1 = c

        proof

          consider x be POINT of S such that

           A9: between (c,a1,x) and

           A10: (c,x) equiv (c,c) by A7, A8, Satz5p5;

          c = x by A10, GTARSKI1:def 7;

          hence thesis by A9, GTARSKI1:def 10;

        end;

        then Middle (a1,m1,a1) & Middle (a2,m2,a2) by A5, A6, A8, A3, A4, Satz2p2, GTARSKI1:def 7;

        then m1 = a1 & m2 = a2 by GTARSKI1:def 10;

        hence thesis by A8, Satz3p1;

      end;

        suppose

         A11: a2 <> c;

        set a = ( reflection (c,a2)), b = ( reflection (c,b2)), m = ( reflection (c,m2));

        now

          thus (c,a1) equiv (c,a1) by Satz2p1;

          (c,a2) equiv (( reflection (c,c)),( reflection (c,a2))) by Satz7p13;

          hence (c,a2) equiv (c,a) by Satz7p10;

        end;

        then

         A12: (c,a1) <= (c,a) by A7, Satz5p6;

        per cases ;

          suppose

           A13: a1 = c;

          then a1 = b1 by A3, Satz2p2, GTARSKI1:def 7;

          then m1 = a1 by A5, GTARSKI1:def 10;

          hence thesis by A13, Satz3p1, Satz3p2;

        end;

          suppose

           A14: a1 <> c;

          

           A15: between (c,a1,a)

          proof

            c out (a1,a)

            proof

              now

                thus c <> a1 by A14;

                thus c <> a

                proof

                  assume c = a;

                  then ( reflection (c,a2)) = ( reflection (c,c)) by Satz7p10;

                  hence contradiction by A11, Satz7p9;

                end;

                thus between (c,a1,a) or between (c,a,a1)

                proof

                  

                   A16: Middle (a2,c,a) by DEFR;

                  

                   A17: between (a2,c,a1) by A1, Satz3p2;

                  per cases by A11, A16, Satz5p1;

                    suppose between (a2,a,a1);

                    hence thesis by A16, Satz3p6p1;

                  end;

                    suppose between (a2,a1,a);

                    hence thesis by A17, Satz3p6p1;

                  end;

                end;

              end;

              hence thesis;

            end;

            hence thesis by A12, Satz6p13;

          end;

          

           A18: between (c,b1,b)

          proof

            per cases ;

              suppose c = b1;

              hence thesis by A14, A3, GTARSKI1:def 7;

            end;

              suppose

               A19: c <> b1;

              

               A20: (c,b1) <= (c,b2) by A3, A4, A7, Satz5p6;

              (c,b2) equiv (( reflection (c,c)),( reflection (c,b2))) by Satz7p13;

              then (c,b2) equiv (c,b) & (c,b1) equiv (c,b1) by Satz2p1, Satz7p10;

              then

               A21: (c,b1) <= (c,b) by A20, Satz5p6;

              

               A22: b2 <> c by A11, A4, GTARSKI1:def 7;

              c out (b1,b)

              proof

                now

                  thus c <> b1 by A19;

                  thus c <> b

                  proof

                    assume c = b;

                    then ( reflection (c,b2)) = ( reflection (c,c)) by Satz7p10;

                    hence contradiction by A22, Satz7p9;

                  end;

                  thus between (c,b1,b) or between (c,b,b1)

                  proof

                    

                     A23: Middle (b2,c,b) by DEFR;

                    

                     A24: between (b2,c,b1) by A2, Satz3p2;

                    then between (b2,b,b1) or between (b2,b1,b) by A22, A23, Satz5p1;

                    hence thesis by A23, A24, Satz3p6p1;

                  end;

                end;

                hence thesis;

              end;

              hence thesis by A21, Satz6p13;

            end;

          end;

           between (a,a1,c) & between (b,b1,c) & between (a,m,b) by A18, Satz3p2, A15, A6, Satz7p15;

          then

          consider q be POINT of S such that

           A25: between (m,q,c) and

           A26: between (a1,q,b1) by Satz3p17;

          

           A27: between (m,c,m2)

          proof

             Middle (m2,c,m) by DEFR;

            hence thesis by Satz3p2;

          end;

          q = m1

          proof

            (a,a1,c,m) IFS (b,b1,c,m)

            proof

              now

                thus between (a,a1,c) by A15, Satz3p2;

                thus between (b,b1,c) by A18, Satz3p2;

                (( reflection (c,c)),( reflection (c,a2))) equiv (( reflection (c,c)),( reflection (c,b2))) by A4, Satz7p16;

                then (c,( reflection (c,a2))) equiv (( reflection (c,c)),( reflection (c,b2))) by Satz7p10;

                then (c,a) equiv (c,b) by Satz7p10;

                then (c,a) equiv (b,c) by Satz2p5;

                hence (a,c) equiv (b,c) by Satz2p4;

                (c,a1) equiv (b1,c) by A3, Satz2p5;

                hence (a1,c) equiv (b1,c) by Satz2p4;

                (m2,a2) equiv (b2,m2) by A6, Satz2p5;

                then (a2,m2) equiv (b2,m2) by Satz2p4;

                hence (a,m) equiv (b,m) by Satz7p16;

                thus (c,m) equiv (c,m) by Satz2p1;

              end;

              hence thesis;

            end;

            then (a1,m) equiv (b1,m) by Satz4p2;

            then

             A28: (a1,m) equiv (m,b1) by Satz2p5;

            then

             A29: (m,a1) equiv (m,b1) by Satz2p4;

            (q,a1) equiv (q,b1)

            proof

              per cases ;

                suppose

                 A30: m <> c;

                 Collinear (c,m,q) by A25;

                hence thesis by A3, A29, A30, Satz4p17;

              end;

                suppose m = c;

                then q = m by A25, GTARSKI1:def 10;

                hence thesis by A28, Satz2p4;

              end;

            end;

            then Middle (a1,q,b1) by A26;

            hence thesis by A5, Satz7p17;

          end;

          hence thesis by A27, A25, Satz3p6p1;

        end;

      end;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:114

    

     Satz7p22part2: 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) implies between (m1,c,m2)

    proof

      assume that

       A1: between (a1,c,a2) and

       A2: between (b1,c,b2) and

       A3: (c,a1) equiv (c,b1) and

       A4: (c,a2) equiv (c,b2) and

       A5: Middle (a1,m1,b1) and

       A6: Middle (a2,m2,b2) and

       A7: (c,a2) <= (c,a1);

      per cases ;

        suppose

         A8: a1 = c;

        a2 = c

        proof

          consider x be POINT of S such that

           A9: between (c,a2,x) and

           A10: (c,x) equiv (c,c) by A7, A8, Satz5p5;

          c = x by A10, GTARSKI1:def 7;

          hence thesis by A9, GTARSKI1:def 10;

        end;

        then Middle (a1,m1,a1) & Middle (a2,m2,a2) by A5, A6, A8, A3, A4, Satz2p2, GTARSKI1:def 7;

        then m1 = a1 & m2 = a2 by GTARSKI1:def 10;

        hence thesis by A8, Satz3p1, Satz3p2;

      end;

        suppose

         A11: a1 <> c;

        set a = ( reflection (c,a1)), b = ( reflection (c,b1)), m = ( reflection (c,m1));

        now

          thus (c,a2) equiv (c,a2) by Satz2p1;

          (c,a1) equiv (( reflection (c,c)),( reflection (c,a1))) by Satz7p13;

          hence (c,a1) equiv (c,a) by Satz7p10;

        end;

        then

         A12: (c,a2) <= (c,a) by A7, Satz5p6;

        per cases ;

          suppose

           A13: a2 = c;

          then a2 = b2 by A4, Satz2p2, GTARSKI1:def 7;

          then m2 = a2 by A6, GTARSKI1:def 10;

          hence thesis by A13, Satz3p1;

        end;

          suppose

           A14: a2 <> c;

          

           A15: between (c,a2,a)

          proof

            c out (a2,a)

            proof

              now

                thus c <> a2 by A14;

                thus c <> a

                proof

                  assume c = a;

                  then ( reflection (c,a1)) = ( reflection (c,c)) by Satz7p10;

                  hence contradiction by A11, Satz7p9;

                end;

                thus between (c,a2,a) or between (c,a,a2)

                proof

                  

                   A16: Middle (a1,c,a) by DEFR;

                  then between (a1,a,a2) or between (a1,a2,a) by A1, A11, Satz5p1;

                  hence thesis by A1, A16, Satz3p6p1;

                end;

              end;

              hence thesis;

            end;

            hence thesis by A12, Satz6p13;

          end;

          

           A17: between (c,b2,b)

          proof

            per cases ;

              suppose c = b2;

              hence thesis by A14, A4, GTARSKI1:def 7;

            end;

              suppose

               A18: c <> b2;

              

               A19: (c,b2) <= (c,b1) by A3, A4, A7, Satz5p6;

              (c,b1) equiv (( reflection (c,c)),( reflection (c,b1))) by Satz7p13;

              then (c,b1) equiv (c,b) & (c,b2) equiv (c,b2) by Satz2p1, Satz7p10;

              then

               A20: (c,b2) <= (c,b) by A19, Satz5p6;

              

               A21: b1 <> c by A11, A3, GTARSKI1:def 7;

              c out (b2,b)

              proof

                now

                  thus c <> b2 by A18;

                  thus c <> b

                  proof

                    assume c = b;

                    then ( reflection (c,b1)) = ( reflection (c,c)) by Satz7p10;

                    hence contradiction by A21, Satz7p9;

                  end;

                  thus ( between (c,b2,b) or between (c,b,b2))

                  proof

                    

                     A22: Middle (b1,c,b) by DEFR;

                    per cases by A2, A21, Satz5p1;

                      suppose between (b1,b,b2);

                      hence thesis by A22, Satz3p6p1;

                    end;

                      suppose between (b1,b2,b);

                      hence thesis by A2, Satz3p6p1;

                    end;

                  end;

                end;

                hence thesis;

              end;

              hence thesis by A20, Satz6p13;

            end;

          end;

           between (a,a2,c) & between (b,b2,c) & between (a,m,b) by A5, Satz7p15, A15, Satz3p2, A17;

          then

          consider q be POINT of S such that

           A23: between (m,q,c) and

           A24: between (a2,q,b2) by Satz3p17;

          

           A25: between (m,c,m1)

          proof

             Middle (m1,c,m) by DEFR;

            hence thesis by Satz3p2;

          end;

          q = m2

          proof

            (a,a2,c,m) IFS (b,b2,c,m)

            proof

              now

                thus between (a,a2,c) by A15, Satz3p2;

                thus between (b,b2,c) by A17, Satz3p2;

                (( reflection (c,c)),( reflection (c,a1))) equiv (( reflection (c,c)),( reflection (c,b1))) by A3, Satz7p16;

                then (c,( reflection (c,a1))) equiv (( reflection (c,c)),( reflection (c,b1))) by Satz7p10;

                then (c,a) equiv (c,b) by Satz7p10;

                then (c,a) equiv (b,c) by Satz2p5;

                hence (a,c) equiv (b,c) by Satz2p4;

                (c,a2) equiv (b2,c) by A4, Satz2p5;

                hence (a2,c) equiv (b2,c) by Satz2p4;

                (m1,a1) equiv (b1,m1) by A5, Satz2p5;

                then (a1,m1) equiv (b1,m1) by Satz2p4;

                hence (a,m) equiv (b,m) by Satz7p16;

                thus (c,m) equiv (c,m) by Satz2p1;

              end;

              hence thesis;

            end;

            then (a2,m) equiv (b2,m) by Satz4p2;

            then

             A26: (a2,m) equiv (m,b2) by Satz2p5;

            then

             A27: (m,a2) equiv (m,b2) by Satz2p4;

            (q,a2) equiv (q,b2)

            proof

              per cases ;

                suppose

                 A28: m <> c;

                 Collinear (c,m,q) by A23;

                hence thesis by A4, A27, A28, Satz4p17;

              end;

                suppose m = c;

                then q = m by A23, GTARSKI1:def 10;

                hence thesis by A26, Satz2p4;

              end;

            end;

            then Middle (a2,q,b2) by A24;

            hence thesis by A6, Satz7p17;

          end;

          then between (m2,c,m1) by A25, A23, Satz3p6p1;

          hence thesis by Satz3p2;

        end;

      end;

    end;

    ::$Notion-Name

    theorem :: GTARSKI3:115

    

     Satz7p22: 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) implies between (m1,c,m2)

    proof

      assume that

       A1: between (a1,c,a2) and

       A2: between (b1,c,b2) and

       A3: (c,a1) equiv (c,b1) and

       A4: (c,a2) equiv (c,b2) and

       A5: Middle (a1,m1,b1) and

       A6: Middle (a2,m2,b2);

      per cases by Satz5p10;

        suppose (c,a1) <= (c,a2);

        hence thesis by A1, A2, A3, A4, A5, A6, Satz7p22part1;

      end;

        suppose (c,a2) <= (c,a1);

        hence thesis by A1, A2, A3, A4, A5, A6, Satz7p22part2;

      end;

    end;

    definition

      let S be TarskiGeometryStruct;

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

      :: GTARSKI3:def14

      pred Krippenfigur a1,m1,b1,c,b2,m2,a2 means 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);

    end

    ::$Notion-Name

    theorem :: GTARSKI3:116

     Krippenfigur (a1,m1,b1,c,b2,m2,a2) implies between (m1,c,m2) by Satz7p22;

    registration

      cluster non empty for satisfying_Lower_Dimension_Axiom satisfying_Tarski-model TarskiGeometryStruct;

      existence by GTARSKI2:def 2;

    end

    reserve S for non empty satisfying_Lower_Dimension_Axiom satisfying_Tarski-model TarskiGeometryStruct,

a,b,c,p,q,r for POINT of S;

    ::$Unknown

    theorem :: GTARSKI3:117

    (c,a) equiv (c,b) implies ex x be POINT of S st Middle (a,x,b)

    proof

      assume

       A1: (c,a) equiv (c,b);

      per cases ;

        suppose Collinear (a,b,c);

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

        per cases by A1, Satz7p20;

          suppose

           A2: a = b;

          take a;

          thus thesis by A2, Satz3p1, Satz2p1;

        end;

          suppose Middle (a,c,b);

          hence thesis;

        end;

      end;

        suppose

         A3: not Collinear (a,b,c);

        consider p such that

         A4: between (c,a,p) and

         A5: a <> p by Satz3p14;

        consider q such that

         A6: between (c,b,q) and

         A7: (b,q) equiv (a,p) by GTARSKI1:def 8;

         between (p,a,c) & between (q,b,c) by A4, A6, Satz3p2;

        then

        consider r such that

         A8: between (a,r,q) and

         A9: between (b,r,p) by GTARSKI1:def 11;

        consider x be POINT of S such that

         A10: between (a,x,b) and

         A11: between (r,x,c) by A4, A9, GTARSKI1:def 11;

        take x;

        (x,a) equiv (x,b)

        proof

          

           A12: (r,a) equiv (r,b)

          proof

            

             A13: (c,a,p,b) AFS (c,b,q,a) by A4, A6, A1, A7, GTARSKI1:def 5, Satz2p2;

            c <> a by A3, Satz3p1;

            then

             A15: (p,b) equiv (a,q) by Satz2p5, A13, Axiom5AFS;

            thesis

            proof

              consider r9 be POINT of S such that

               A19: between (a,r9,q) and

               A20: (b,r,p) cong (a,r9,q) by A15, Satz2p4, A9, Satz4p5;

               A21:

              now

                (b,q) equiv (p,a) by A7, Satz2p5;

                then (q,b) equiv (p,a) by Satz2p4;

                hence (b,r,p,a) IFS (a,r9,q,b) by A9, A19, A20, Satz2p2, GTARSKI1:def 5;

                thus (b,r,p,q) IFS (a,r9,q,p) by A9, A19, A20, GTARSKI1:def 5, A7;

              end;

              then (r,a) equiv (b,r9) by Satz2p5, Satz4p2;

              then

               A23: (a,r,q) cong (b,r9,p) by A21, Satz2p4, Satz2p2, Satz4p2;

              now

                thus Collinear (a,r,q) by A8;

                hence Collinear (b,r9,p) by A23, Satz4p13;

              end;

              then Collinear (a,q,r) & Collinear (b,p,r9) by Satz3p2;

              then

               A24: r in ( Line (a,q)) & r9 in ( Line (b,p));

              

               A25: r9 in ( Line (a,q)) & r in ( Line (b,p))

              proof

                 Collinear (a,q,r9) by A19, Satz3p2;

                hence r9 in ( Line (a,q));

                 Collinear (b,p,r) by A9, Satz3p2;

                hence r in ( Line (b,p));

              end;

              

               A26: a = q iff b = p by A15, Satz2p2, GTARSKI1:def 7;

              r = r9

              proof

                per cases ;

                  suppose

                   A27: a = q or b = p;

                  then

                   A28: a = r by A8, A26, GTARSKI1:def 10;

                   between (a,r9,a) by A19, A27, A15, Satz2p2, GTARSKI1:def 7;

                  hence thesis by A28, GTARSKI1:def 10;

                end;

                  suppose

                   A29: a <> q & b <> p;

                  assume

                   A30: r <> r9;

                  reconsider A = ( Line (a,q)), B = ( Line (b,p)) as Subset of S;

                  

                   A31: A is_line & B is_line by A29;

                  then

                   A32: A = B by A30, A24, A25, Satz6p19;

                  

                   A33: a <> b by A3, Satz3p1;

                  

                   A34: A = ( Line (a,b))

                  proof

                    b in A & a in A & A is_line by A29, A32, Satz6p17;

                    hence thesis by A33, Satz6p18;

                  end;

                  

                   A35: ( Line (a,p)) = A

                  proof

                    

                     A36: a in A by Satz6p17;

                    p in B by Satz6p17;

                    then p in A & A is_line by A31, A30, A24, A25, Satz6p19;

                    hence ( Line (a,p)) = A by A36, A5, Satz6p18;

                  end;

                  c in A

                  proof

                     Collinear (a,p,c) by A4;

                    hence thesis by A35;

                  end;

                  then ex y be POINT of S st c = y & Collinear (a,b,y) by A34;

                  hence contradiction by A3;

                end;

              end;

              hence thesis by A21, Satz4p2;

            end;

            hence thesis;

          end;

          per cases ;

            suppose r = c;

            then r = x by A11, GTARSKI1:def 10;

            hence thesis by A12;

          end;

            suppose

             A37: r <> c;

             Collinear (c,r,x) & (c,a) equiv (c,b) & (r,a) equiv (r,b) by A11, A1, A12;

            hence thesis by A37, Satz4p17;

          end;

        end;

        hence thesis by A10;

      end;

    end;

    begin

    definition

      let S be TarskiGeometryStruct;

      :: GTARSKI3:def15

      attr S is (RE) means for a,b be POINT of S holds (a,b) equiv (b,a);

      :: GTARSKI3:def16

      attr S is (TE) means for a,b,p,q,r,s be POINT of S st (a,b) equiv (p,q) & (a,b) equiv (r,s) holds (p,q) equiv (r,s);

      :: GTARSKI3:def17

      attr S is (IE) means for a,b,c be POINT of S st (a,b) equiv (c,c) holds a = b;

      :: GTARSKI3:def18

      attr S is (SC) means for a,b,c,q be POINT of S holds ex x be POINT of S st between (q,a,x) & (a,x) equiv (b,c);

      :: GTARSKI3:def19

      attr S is (FS) means for a,b,c,d,a9,b9,c9,d9 be 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);

      :: GTARSKI3:def20

      attr S is (IB) means for a,b be POINT of S st between (a,b,a) holds a = b;

      :: GTARSKI3:def21

      attr S is (Pa) means for a,b,c,p,q be POINT of S st between (a,p,c) & between (b,q,c) holds ex x be POINT of S st between (p,x,b) & between (q,x,a);

      :: GTARSKI3:def22

      attr S is (Lo2) means ex a,b,c be POINT of S st not between (a,b,c) & not between (b,c,a) & not between (c,a,b);

      :: GTARSKI3:def23

      attr S is (Up2) means for a,b,c,p,q be POINT of S st p <> q & (a,p) equiv (a,q) & (b,p) equiv (b,q) & (c,p) equiv (c,q) holds between (a,b,c) or between (b,c,a) or between (c,a,b);

      :: GTARSKI3:def24

      attr S is (Eu) means for a,b,c,d,t be POINT of S st between (a,d,t) & between (b,d,c) & a <> d holds ex x,y be POINT of S st between (a,b,x) & between (a,c,y) & between (x,t,y);

      :: GTARSKI3:def25

      attr S is (Co) means for X,Y be set st (ex a be POINT of S st (for x,y be POINT of S st x in X & y in Y holds between (a,x,y))) holds (ex b be POINT of S st (for x,y be POINT of S st x in X & y in Y holds between (x,b,y)));

      :: GTARSKI3:def26

      attr S is (FS') means for a,b,c,d,a9,b9,c9,d9 be 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);

    end

    reserve S for TarskiGeometryStruct;

    theorem :: GTARSKI3:118

    S is satisfying_CongruenceSymmetry iff S is (RE);

    theorem :: GTARSKI3:119

    S is satisfying_CongruenceEquivalenceRelation iff S is (TE);

    theorem :: GTARSKI3:120

    S is satisfying_CongruenceIdentity iff S is (IE);

    theorem :: GTARSKI3:121

    S is satisfying_SegmentConstruction iff S is (SC);

    theorem :: GTARSKI3:122

    S is satisfying_BetweennessIdentity iff S is (IB);

    theorem :: GTARSKI3:123

    S is satisfying_Pasch iff S is (Pa);

    theorem :: GTARSKI3:124

    S is satisfying_Lower_Dimension_Axiom iff S is (Lo2);

    theorem :: GTARSKI3:125

    S is satisfying_Upper_Dimension_Axiom iff S is (Up2);

    theorem :: GTARSKI3:126

    S is satisfying_Euclid_Axiom iff S is (Eu);

    theorem :: GTARSKI3:127

    for S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct holds S is satisfying_SAS iff S is (FS)

    proof

      let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation TarskiGeometryStruct;

      hereby

        assume S is satisfying_SAS;

        then S is satisfying_SST_A5;

        hence S is (FS);

      end;

      assume S is (FS);

      then S is satisfying_SST_A5;

      hence S is satisfying_SAS;

    end;

    theorem :: GTARSKI3:128

    

     ThMak1: for S be non empty TarskiGeometryStruct holds S is satisfying_Continuity_Axiom iff S is (Co)

    proof

      let S be non empty TarskiGeometryStruct;

      hereby

        assume

         A1: S is satisfying_Continuity_Axiom;

        now

          let X,Y be set;

          reconsider X9 = (X /\ the carrier of S), Y9 = (Y /\ the carrier of S) as Subset of S by XBOOLE_1: 17;

          assume ex a be POINT of S st (for x,y be POINT of S st x in X & y in Y holds between (a,x,y));

          then

          consider a be POINT of S such that

           A3: (for x,y be POINT of S st x in X & y in Y holds between (a,x,y));

          for x,y be POINT of S st x in X9 & y in Y9 holds between (a,x,y)

          proof

            let x,y be POINT of S;

            assume x in X9 & y in Y9;

            then x in X & y in Y by XBOOLE_0:def 4;

            hence thesis by A3;

          end;

          then

          consider b be POINT of S such that

           A4: for x,y be POINT of S st x in X9 & y in Y9 holds between (x,b,y) by A1;

          for x,y be POINT of S st x in X & y in Y holds between (x,b,y)

          proof

            let x,y be POINT of S;

            assume x in X & y in Y;

            then x in X9 & y in Y9 by XBOOLE_0:def 4;

            hence thesis by A4;

          end;

          hence ex b be POINT of S st (for x,y be POINT of S st x in X & y in Y holds between (x,b,y));

        end;

        hence S is (Co);

      end;

      assume S is (Co);

      hence S is satisfying_Continuity_Axiom;

    end;

    registration

      cluster (RE) -> satisfying_CongruenceSymmetry for TarskiGeometryStruct;

      coherence ;

      cluster (TE) -> satisfying_CongruenceEquivalenceRelation for TarskiGeometryStruct;

      coherence ;

      cluster (IE) -> satisfying_CongruenceIdentity for TarskiGeometryStruct;

      coherence ;

      cluster (SC) -> satisfying_SegmentConstruction for TarskiGeometryStruct;

      coherence ;

      cluster (IB) -> satisfying_BetweennessIdentity for TarskiGeometryStruct;

      coherence ;

      cluster (Pa) -> satisfying_Pasch for TarskiGeometryStruct;

      coherence ;

      cluster (Lo2) -> satisfying_Lower_Dimension_Axiom for TarskiGeometryStruct;

      coherence ;

      cluster (Up2) -> satisfying_Upper_Dimension_Axiom for TarskiGeometryStruct;

      coherence ;

      cluster (Eu) -> satisfying_Euclid_Axiom for TarskiGeometryStruct;

      coherence ;

      cluster (Co) -> satisfying_Continuity_Axiom for TarskiGeometryStruct;

      coherence ;

    end

    registration

      cluster satisfying_CongruenceSymmetry -> (RE) for TarskiGeometryStruct;

      coherence ;

      cluster satisfying_CongruenceEquivalenceRelation -> (TE) for TarskiGeometryStruct;

      coherence ;

      cluster satisfying_CongruenceIdentity -> (IE) for TarskiGeometryStruct;

      coherence ;

      cluster satisfying_SegmentConstruction -> (SC) for TarskiGeometryStruct;

      coherence ;

      cluster satisfying_BetweennessIdentity -> (IB) for TarskiGeometryStruct;

      coherence ;

      cluster satisfying_Pasch -> (Pa) for TarskiGeometryStruct;

      coherence ;

      cluster satisfying_Lower_Dimension_Axiom -> (Lo2) for TarskiGeometryStruct;

      coherence ;

      cluster satisfying_Upper_Dimension_Axiom -> (Up2) for TarskiGeometryStruct;

      coherence ;

      cluster satisfying_Euclid_Axiom -> (Eu) for TarskiGeometryStruct;

      coherence ;

      cluster satisfying_Continuity_Axiom -> (Co) for non empty TarskiGeometryStruct;

      coherence by ThMak1;

    end

    registration

      cluster (RE) (TE) for TarskiGeometryStruct;

      existence

      proof

         TarskiEuclid2Space is satisfying_CongruenceEquivalenceRelation;

        hence thesis;

      end;

    end

    theorem :: GTARSKI3:129

    

     ThMak2: for S be (RE) (TE) TarskiGeometryStruct holds S is satisfying_SAS iff S is (FS)

    proof

      let S be (RE) (TE) TarskiGeometryStruct;

      hereby

        assume S is satisfying_SAS;

        then S is satisfying_SST_A5;

        hence S is (FS);

      end;

      assume S is (FS);

      then S is satisfying_SST_A5;

      hence S is satisfying_SAS;

    end;

    registration

      cluster (FS) -> satisfying_SAS for (RE) (TE) TarskiGeometryStruct;

      coherence by ThMak2;

    end

    registration

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

      existence

      proof

         TarskiEuclid2Space is (FS) by ThMak2;

        hence thesis;

      end;

    end

    reserve S for TarskiGeometryStruct;

    ::$Notion-Name

    theorem :: GTARSKI3:130

    

     ThMak3: for S be TarskiGeometryStruct st S is (RE) & S is (TE) holds (S is (FS) iff S is (FS'))

    proof

      let S be TarskiGeometryStruct;

      assume that

       A1: S is (RE) and

       A2: S is (TE);

      hereby

        assume

         A3: S is (FS);

        thus S is (FS')

        proof

          let a,b,c,d,a9,b9,c9,d9 be POINT of S;

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

          then (c,d) equiv (c9,d9) & (c,d) equiv (d,c) by A1, A3;

          hence (d,c) equiv (c9,d9) by A2;

        end;

      end;

      assume

       A4: S is (FS');

      let a,b,c,d,a9,b9,c9,d9 be POINT of S;

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

      then (d,c) equiv (c9,d9) & (d,c) equiv (c,d) by A1, A4;

      hence (c,d) equiv (c9,d9) by A2;

    end;

    theorem :: GTARSKI3:131

    for S be (RE) (TE) TarskiGeometryStruct holds S is (FS) iff S is (FS') by ThMak3;

    registration

      cluster (FS') -> (FS) for (RE) (TE) TarskiGeometryStruct;

      coherence by ThMak3;

    end

    registration

      cluster (TE) (SC) for TarskiGeometryStruct;

      existence

      proof

         TarskiEuclid2Space is (SC);

        hence thesis;

      end;

    end

    registration

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

      existence

      proof

         TarskiEuclid2Space is (FS) by ThMak2;

        then TarskiEuclid2Space is (FS') by ThMak3;

        hence thesis;

      end;

    end

    registration

      cluster (SC) for (RE) (TE) (FS') TarskiGeometryStruct;

      existence

      proof

         TarskiEuclid2Space is (FS) by ThMak2;

        then TarskiEuclid2Space is (RE) (TE) (FS') by ThMak3;

        hence thesis;

      end;

    end

    theorem :: GTARSKI3:132

    for S be (TE) (SC) TarskiGeometryStruct holds for a,b be POINT of S holds (a,b) equiv (a,b) by Satz2p1bis;

    theorem :: GTARSKI3:133

    for S be (IE) (SC) TarskiGeometryStruct holds for a,b be POINT of S holds between (a,b,b) by Satz3p1;

    theorem :: GTARSKI3:134

    for S be (TE) (SC) TarskiGeometryStruct holds for a,b,c,d be POINT of S st (a,b) equiv (c,d) holds (c,d) equiv (a,b) by Satz2p2bis;

    theorem :: GTARSKI3:135

    

     ThMak4: for S be (TE) (SC) (FS') TarskiGeometryStruct holds (for a,b,c,d,e,f be 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

      let S be (TE) (SC) (FS') TarskiGeometryStruct;

      let a,b,c,d,e,f be POINT of S;

      assume

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

      

       A2: (a,f) equiv (a,f) by Satz2p1bis;

      S is (FS');

      hence thesis by A1, A2;

    end;

    definition

      let S be TarskiGeometryStruct;

      :: GTARSKI3:def27

      attr S is (RE') means for a,b,c,d be POINT of S st a <> b & between (b,a,c) holds (d,c) equiv (c,d);

    end

    theorem :: GTARSKI3:136

    

     ThMak5: for S be (TE) (SC) (FS') TarskiGeometryStruct holds S is (RE')

    proof

      let S be (TE) (SC) (FS') TarskiGeometryStruct;

      let a,b,c,d be POINT of S;

      assume

       A1: a <> b & between (b,a,c);

      (a,c) equiv (a,c) & (b,a) equiv (b,a) & (b,d) equiv (b,d) by Satz2p1bis;

      hence thesis by A1, ThMak4;

    end;

    registration

      cluster (TE) (SC) (FS') -> (RE') for TarskiGeometryStruct;

      coherence by ThMak5;

    end

    registration

      cluster (RE') for (IE) TarskiGeometryStruct;

      existence

      proof

         TarskiEuclid2Space is (FS) by ThMak2;

        then TarskiEuclid2Space is (RE) (TE) (FS') by ThMak3;

        hence thesis;

      end;

    end

    registration

      cluster (SC) for (RE') (IE) TarskiGeometryStruct;

      existence

      proof

         TarskiEuclid2Space is (FS) by ThMak2;

        then TarskiEuclid2Space is (RE) (TE) (FS') by ThMak3;

        hence thesis;

      end;

    end

    registration

      cluster trivial for (IE) non empty TarskiGeometryStruct;

      existence

      proof

         TrivialTarskiSpace is (IE);

        hence thesis;

      end;

    end

    registration

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

      existence

      proof

         TrivialTarskiSpace is (IE);

        hence thesis;

      end;

    end

    theorem :: GTARSKI3:137

    for S be trivial (IE) (SC) non empty TarskiGeometryStruct holds S is (RE)

    proof

      let S be trivial (IE) (SC) non empty TarskiGeometryStruct;

      let a,b be POINT of S;

      a = b by ZFMISC_1:def 10;

      hence thesis by Satz2p8;

    end;

    registration

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

      existence

      proof

        now

           TrivialTarskiSpace is (FS) by ThMak2;

          hence TrivialTarskiSpace is (RE) (TE) (FS') by ThMak3;

          thus TrivialTarskiSpace is non empty;

        end;

        hence thesis;

      end;

    end

    theorem :: GTARSKI3:138

    

     ThMak6: for S be (RE') (TE) (IE) (SC) non empty TarskiGeometryStruct holds S is (RE)

    proof

      let S be (RE') (TE) (IE) (SC) non empty TarskiGeometryStruct;

      let a,b be POINT of S;

      per cases ;

        suppose a = b;

        hence thesis by Satz2p8;

      end;

        suppose

         A1: a <> b;

         between (b,a,a) & S is (RE') by Satz3p1;

        hence thesis by A1, Satz2p2bis;

      end;

    end;

    registration

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

      existence

      proof

        now

           TrivialTarskiSpace is (FS) by ThMak2;

          hence TrivialTarskiSpace is (RE) (TE) (FS') by ThMak3;

          thus TrivialTarskiSpace is non empty;

        end;

        hence thesis;

      end;

    end

    theorem :: GTARSKI3:139

    for S be (TE) (IE) (SC) (FS') non empty TarskiGeometryStruct holds S is (RE) by ThMak6;

    theorem :: GTARSKI3:140

    

     ThMak7: for S be (TE) (IE) (SC) (FS') non empty TarskiGeometryStruct holds S is (FS)

    proof

      let S be (TE) (IE) (SC) (FS') non empty TarskiGeometryStruct;

      S is (RE) by ThMak6;

      hence thesis;

    end;

    begin

    ::$Notion-Name

    registration

      cluster (RE) (TE) (FS) -> (FS') for TarskiGeometryStruct;

      coherence by ThMak3;

    end

    registration

      cluster (TE) (IE) (SC) (FS') -> (FS) for non empty TarskiGeometryStruct;

      coherence by ThMak7;

    end

    registration

      cluster (TE) (IE) (SC) (FS') -> (RE) for non empty TarskiGeometryStruct;

      coherence by ThMak6;

    end

    registration

      cluster (TE) (IE) (SC) (FS') -> satisfying_SAS for non empty TarskiGeometryStruct;

      coherence ;

    end

    registration

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

      existence

      proof

         TarskiEuclid2Space is (FS) & TarskiEuclid2Space is (Co) by GTARSKI2:def 2, ThMak2;

        hence thesis by GTARSKI2:def 2;

      end;

    end

    definition

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

    end

    definition

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

    end

    theorem :: GTARSKI3:141

    for TP be Makarios_CE2 holds TP is Makarios_CE'2;

    theorem :: GTARSKI3:142

    for TP be Makarios_CE'2 holds TP is Makarios_CE2;

    theorem :: GTARSKI3:143

    for TP be 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;

    theorem :: GTARSKI3:144

    for TP be 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;