gtarski4.miz



    begin

    reserve S for non empty satisfying_Tarski-model TarskiGeometryStruct,

a,b,c,d,c9,x,y,z,p,q,q9 for POINT of S;

    definition

      let S be non empty satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct;

      let a,b be POINT of S;

      :: original: Line

      redefine

      func Line (a,b);

      commutativity by GTARSKI3: 83;

    end

    

     LemmaA1: Collinear (a,b,c) implies c in ( Line (a,b))

    proof

      assume Collinear (a,b,c);

      then c in { x where x be POINT of S : Collinear (a,b,x) };

      hence thesis by GTARSKI3:def 10;

    end;

    

     LemmaA2: x in ( Line (a,p)) implies Collinear (x,a,p)

    proof

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

      then x in { y where y be POINT of S : Collinear (a,p,y) } by GTARSKI3:def 10;

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

      hence thesis by GTARSKI3: 45;

    end;

    theorem :: GTARSKI4:1

    

     Prelim01: for S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity TarskiGeometryStruct holds for a,b,c,d be POINT of S st (a,b) equiv (c,d) holds (a,b) equiv (d,c) & (b,a) equiv (c,d) & (b,a) equiv (d,c) & (c,d) equiv (a,b) & (d,c) equiv (a,b) & (c,d) equiv (b,a) & (d,c) equiv (b,a)

    proof

      let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity TarskiGeometryStruct;

      let c1,c2,c3,c4 be POINT of S;

      assume

       A1: (c1,c2) equiv (c3,c4);

      assume

       A2: not ((c1,c2) equiv (c4,c3) & (c2,c1) equiv (c3,c4) & (c2,c1) equiv (c4,c3) & (c3,c4) equiv (c1,c2) & (c4,c3) equiv (c1,c2) & (c3,c4) equiv (c2,c1) & (c4,c3) equiv (c2,c1));

      

       A3: (c1,c2) equiv (c2,c1) by GTARSKI1:def 5;

      then

       A4: (c3,c4) equiv (c2,c1) by A1, GTARSKI1:def 6;

      (c1,c2) equiv (c1,c2) by GTARSKI3: 1;

      then

       A5: (c3,c4) equiv (c1,c2) by A1, GTARSKI1:def 6;

      (c3,c4) equiv (c4,c3) by GTARSKI1:def 5;

      hence contradiction by A1, A2, A3, A4, A5, GTARSKI1:def 6;

    end;

    theorem :: GTARSKI4:2

    

     Prelim02: for S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity TarskiGeometryStruct holds for p,q,a,b,c,d be POINT of S st ((p,q) equiv (a,b) or (p,q) equiv (b,a) or (q,p) equiv (a,b) or (q,p) equiv (b,a)) & ((p,q) equiv (c,d) or (p,q) equiv (d,c) or (q,p) equiv (c,d) or (q,p) equiv (d,c)) holds (a,b) equiv (d,c) & (b,a) equiv (c,d) & (b,a) equiv (d,c) & (c,d) equiv (a,b) & (d,c) equiv (a,b) & (c,d) equiv (b,a) & (d,c) equiv (b,a)

    proof

      let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity TarskiGeometryStruct;

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

      assume ((p,q) equiv (a,b) or (p,q) equiv (b,a) or (q,p) equiv (a,b) or (q,p) equiv (b,a)) & ((p,q) equiv (c,d) or (p,q) equiv (d,c) or (q,p) equiv (c,d) or (q,p) equiv (d,c));

      then (p,q) equiv (a,b) & (p,q) equiv (c,d) by Prelim01;

      then (a,b) equiv (c,d) by GTARSKI1:def 6;

      hence thesis by Prelim01;

    end;

    theorem :: GTARSKI4:3

    

     Prelim03: for S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity TarskiGeometryStruct holds for p,q,a,b,c,d be POINT of S st ((p,q) equiv (a,b) or (p,q) equiv (b,a) or (q,p) equiv (a,b) or (q,p) equiv (b,a) or (a,b) equiv (p,q) or (b,a) equiv (p,q) or (a,b) equiv (q,p) or (b,a) equiv (q,p)) & ((p,q) equiv (c,d) or (p,q) equiv (d,c) or (q,p) equiv (c,d) or (q,p) equiv (d,c) or (c,d) equiv (p,q) or (d,c) equiv (p,q) or (c,d) equiv (q,p) or (d,c) equiv (q,p)) holds (a,b) equiv (d,c) & (b,a) equiv (c,d) & (b,a) equiv (d,c) & (c,d) equiv (a,b) & (d,c) equiv (a,b) & (c,d) equiv (b,a) & (d,c) equiv (b,a) & (a,b) equiv (c,d)

    proof

      let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity TarskiGeometryStruct;

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

      assume ((p,q) equiv (a,b) or (p,q) equiv (b,a) or (q,p) equiv (a,b) or (q,p) equiv (b,a) or (a,b) equiv (p,q) or (b,a) equiv (p,q) or (a,b) equiv (q,p) or (b,a) equiv (q,p)) & ((p,q) equiv (c,d) or (p,q) equiv (d,c) or (q,p) equiv (c,d) or (q,p) equiv (d,c) or (c,d) equiv (p,q) or (d,c) equiv (p,q) or (c,d) equiv (q,p) or (d,c) equiv (q,p));

      then (p,q) equiv (a,b) & (p,q) equiv (c,d) by Prelim01;

      hence thesis by Prelim02;

    end;

    theorem :: GTARSKI4:4

    

     Prelim05: for S be satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct holds for a,b be POINT of S holds Collinear (a,b,b) & Collinear (b,b,a) & Collinear (b,a,b)

    proof

      let S be satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct;

      let a,b be POINT of S;

       between (a,b,b) & between (b,b,a) by GTARSKI3: 13, GTARSKI3: 15;

      hence thesis by GTARSKI1:def 17;

    end;

    theorem :: GTARSKI4:5

    

     Prelim07: for S be non empty satisfying_Tarski-model TarskiGeometryStruct holds for p,q,r be POINT of S st p <> q & p <> r & ( Collinear (p,q,r) or Collinear (q,r,p) or Collinear (r,p,q) or Collinear (p,r,q) or Collinear (q,p,r) or Collinear (r,q,p)) holds ( Line (p,q)) = ( Line (p,r)) & ( Line (p,q)) = ( Line (r,p)) & ( Line (q,p)) = ( Line (p,r)) & ( Line (q,p)) = ( Line (r,p))

    proof

      let S be non empty satisfying_Tarski-model TarskiGeometryStruct;

      let p,q,r be POINT of S;

      assume that

       A1: p <> q and

       A2: p <> r and

       A3: Collinear (p,q,r) or Collinear (q,r,p) or Collinear (r,p,q) or Collinear (p,r,q) or Collinear (q,p,r) or Collinear (r,q,p);

       Collinear (p,q,r) by A3, GTARSKI3: 45;

      then r on_line (p,q) by A1, GTARSKI3: 84;

      hence thesis by A1, A2, GTARSKI1: 39, GTARSKI3: 85;

    end;

    theorem :: GTARSKI4:6

    

     Prelim08: for S be TarskiGeometryStruct holds for a,b,c be POINT of S st ( Middle (a,b,c) or between (a,b,c)) holds Collinear (a,b,c)

    proof

      let S be TarskiGeometryStruct;

      let a,b,c be POINT of S;

      assume Middle (a,b,c) or between (a,b,c);

      then between (a,b,c) by GTARSKI3:def 12;

      hence thesis by GTARSKI1:def 17;

    end;

    theorem :: GTARSKI4:7

    

     Prelim08a: for S be satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct holds for a,b,c be POINT of S st ( Middle (a,b,c) or between (a,b,c)) holds Collinear (a,b,c) & Collinear (b,c,a) & Collinear (c,a,b) & Collinear (c,b,a) & Collinear (b,a,c) & Collinear (a,c,b)

    proof

      let S be satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct;

      let a,b,c be POINT of S;

      assume Middle (a,b,c) or between (a,b,c);

      then Collinear (a,b,c) by Prelim08;

      hence thesis by GTARSKI3: 45;

    end;

    theorem :: GTARSKI4:8

    

     Prelim08b: for S be non empty satisfying_Tarski-model TarskiGeometryStruct holds for a,b,c,d be POINT of S st a <> b & Collinear (a,b,c) & Collinear (a,b,d) holds Collinear (a,c,d)

    proof

      let S be non empty satisfying_Tarski-model TarskiGeometryStruct;

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

      assume that

       A1: a <> b and

       A2: Collinear (a,b,c) and

       A3: Collinear (a,b,d);

      per cases ;

        suppose a = c;

        hence thesis by Prelim05;

      end;

        suppose a <> c;

        then

         A4: ( Line (a,b)) = ( Line (a,c)) by A1, A2, Prelim07;

        d in { y where y be POINT of S : Collinear (a,b,y) } by A3;

        then d in ( Line (a,c)) by A4, GTARSKI3:def 10;

        then Collinear (d,a,c) by LemmaA2;

        hence thesis by GTARSKI3: 45;

      end;

    end;

    theorem :: GTARSKI4:9

    

     Prelim09: for S be non empty satisfying_Tarski-model TarskiGeometryStruct holds for a,b be POINT of S st Middle (a,a,b) or Middle (a,b,b) or Middle (a,b,a) holds a = b

    proof

      let S be non empty satisfying_Tarski-model TarskiGeometryStruct;

      let a,b be POINT of S;

      assume Middle (a,a,b) or Middle (a,b,b) or Middle (a,b,a);

      then (a,a) equiv (a,b) or (b,a) equiv (b,b) or Middle (a,b,a) by GTARSKI3:def 12;

      hence thesis by GTARSKI1:def 7, GTARSKI3: 3, GTARSKI3: 97;

    end;

    theorem :: GTARSKI4:10

    

     Prelim10: ( Middle (a,b,c) or Middle (c,b,a)) & (a <> b or b <> c) implies (( Line (b,a)) = ( Line (b,c)) & ( Line (a,b)) = ( Line (b,c)) & ( Line (a,b)) = ( Line (c,b)) & ( Line (b,a)) = ( Line (c,b)))

    proof

      assume that

       A1: ( Middle (a,b,c) or Middle (c,b,a)) and

       A2: a <> b or b <> c;

      

       A3: Middle (a,b,c) by A1, GTARSKI3: 96;

      then between (a,b,c) by GTARSKI3:def 12;

      then

       a4: Collinear (a,b,c) by GTARSKI1:def 17;

      per cases by A2;

        suppose

         A5: a <> b;

        then b <> c by A3, GTARSKI1:def 7, GTARSKI3:def 12;

        hence thesis by a4, A5, GTARSKI3: 82, LemmaA1;

      end;

        suppose

         A6: b <> c;

        then a <> b by A1, Prelim09;

        hence thesis by a4, A6, GTARSKI3: 82, LemmaA1;

      end;

    end;

    theorem :: GTARSKI4:11

    

     Prelim11: a <> b & c <> c9 & (c in ( Line (a,b)) or c in ( Line (b,a))) & (c9 in ( Line (a,b)) or c9 in ( Line (b,a))) implies ( Line (c,c9)) = ( Line (a,b)) & ( Line (c,c9)) = ( Line (b,a)) & ( Line (c9,c)) = ( Line (b,a)) & ( Line (c9,c)) = ( Line (a,b))

    proof

      assume that

       A1: a <> b and

       A2: c <> c9 and

       A3: c in ( Line (a,b)) or c in ( Line (b,a)) and

       A4: c9 in ( Line (a,b)) or c9 in ( Line (b,a));

      ( Line (a,b)) is_line by A1, GTARSKI3:def 11;

      hence thesis by A3, A4, A2, GTARSKI3: 87;

    end;

    theorem :: GTARSKI4:12

    

     Prelim12: Middle (( reflection (p,c)),( reflection (p,b)),( reflection (p,( reflection (b,c)))))

    proof

       Middle (c,b,( reflection (b,c))) by GTARSKI3:def 13;

      then between (( reflection (p,c)),( reflection (p,b)),( reflection (p,( reflection (b,c))))) & (( reflection (p,b)),( reflection (p,c))) equiv (( reflection (p,b)),( reflection (p,( reflection (b,c))))) by GTARSKI3:def 12, GTARSKI3: 106, GTARSKI3: 107;

      hence thesis by GTARSKI3:def 12;

    end;

    begin

    definition

      let S be satisfying_CongruenceIdentity satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_SAS TarskiGeometryStruct;

      let a,b,c be POINT of S;

      :: GTARSKI4:def1

      pred right_angle a,b,c means (a,c) equiv (a,( reflection (b,c)));

    end

    reserve S for satisfying_Tarski-model TarskiGeometryStruct,

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

    ::$Notion-Name

    theorem :: GTARSKI4:13

    

     Satz8p2: right_angle (a,b,c) implies right_angle (c,b,a)

    proof

      assume right_angle (a,b,c);

      then

       A1: (c,a) equiv (a,( reflection (b,c))) by GTARSKI3: 6;

      (a,( reflection (b,c))) equiv (( reflection (b,a)),( reflection (b,( reflection (b,c))))) by GTARSKI3: 105;

      then (a,( reflection (b,c))) equiv (( reflection (b,a)),c) by GTARSKI3: 101;

      then (a,( reflection (b,c))) equiv (c,( reflection (b,a))) by GTARSKI3: 7;

      hence thesis by A1, GTARSKI3: 5;

    end;

    theorem :: GTARSKI4:14

    

     Lem01: ( reflection (a,a)) = a

    proof

       Middle (a,a,a) by GTARSKI3: 97;

      hence thesis by GTARSKI3: 100;

    end;

    ::$Notion-Name

    theorem :: GTARSKI4:15

    

     Satz8p3: right_angle (a,b,c) & a <> b & Collinear (b,a,a9) implies right_angle (a9,b,c)

    proof

      assume that

       A1: right_angle (a,b,c) and

       A2: a <> b and

       A3: Collinear (b,a,a9);

      now

        (b,c) equiv (( reflection (b,b)),( reflection (b,c))) by GTARSKI3: 105;

        hence (b,c) equiv (b,( reflection (b,c))) by Lem01;

      end;

      hence thesis by A1, A2, A3, GTARSKI3: 53;

    end;

    theorem :: GTARSKI4:16

     right_angle (a,b,c) implies right_angle (a,b,( reflection (b,c)))

    proof

      assume right_angle (a,b,c);

      then (a,( reflection (b,c))) equiv (a,c) by GTARSKI3: 4;

      hence thesis by GTARSKI3: 101;

    end;

    ::$Notion-Name

    theorem :: GTARSKI4:17

    

     Satz8p5: right_angle (a,b,b)

    proof

      (a,b) equiv (a,b) by GTARSKI3: 2;

      hence thesis by Lem01;

    end;

    ::$Notion-Name

    theorem :: GTARSKI4:18

    

     Satz8p6: right_angle (a,b,c) & right_angle (a9,b,c) & between (a,c,a9) implies b = c

    proof

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

      then c = ( reflection (b,c)) by GTARSKI3: 55;

      hence thesis by GTARSKI3: 104;

    end;

    ::$Notion-Name

    theorem :: GTARSKI4:19

    

     Satz8p7: right_angle (a,b,c) & right_angle (a,c,b) implies b = c

    proof

      assume that

       A1: right_angle (a,b,c) and

       A2: right_angle (a,c,b);

      assume

       A3: b <> c;

      set c9 = ( reflection (b,c)), a9 = ( reflection (c,a));

      now

        (a9,c) equiv (a9,c9)

        proof

          now

            now

              thus (a,c9) equiv (a,c) by A1, GTARSKI3: 4;

               right_angle (c,c,a) by Satz8p2, Satz8p5;

              hence (a,c) equiv (a9,c) by Prelim01;

            end;

            hence (a,c9) equiv (a9,c) by GTARSKI3: 5;

            now

              thus right_angle (b,c,a) by A2, Satz8p2;

              thus b <> c by A3;

               Middle (c,b,c9) by GTARSKI3:def 13;

              hence Collinear (c,b,c9) by Prelim08a;

            end;

            then right_angle (c9,c,a) by Satz8p3;

            then

             A4: right_angle (a,c,c9) by Satz8p2;

            (a,( reflection (c,c9))) equiv (( reflection (c,a)),( reflection (c,( reflection (c,c9))))) by GTARSKI3: 105;

            then (a,c9) equiv (a9,( reflection (c,( reflection (c,c9))))) by A4, GTARSKI3: 5;

            hence (a,c9) equiv (a9,c9) by GTARSKI3: 101;

          end;

          hence thesis by GTARSKI1:def 6;

        end;

        hence right_angle (a9,b,c);

         Middle (a,c,a9) by GTARSKI3:def 13;

        hence between (a,c,a9) by GTARSKI3:def 12;

      end;

      hence contradiction by A1, A3, Satz8p6;

    end;

    ::$Notion-Name

    theorem :: GTARSKI4:20

    

     Satz8p8: right_angle (a,b,a) implies a = b

    proof

      assume

       A1: right_angle (a,b,a);

       right_angle (a,a,b) by Satz8p2, Satz8p5;

      hence thesis by A1, Satz8p7;

    end;

    ::$Notion-Name

    theorem :: GTARSKI4:21

    

     Satz8p9: right_angle (a,b,c) & Collinear (a,b,c) implies a = b or c = b

    proof

      assume

       A1: right_angle (a,b,c) & Collinear (a,b,c);

      assume

       A2: a <> b;

       Collinear (b,a,c) by A1, GTARSKI3: 45;

      hence thesis by A1, A2, Satz8p3, Satz8p8;

    end;

    ::$Notion-Name

    theorem :: GTARSKI4:22

    

     Satz8p10: right_angle (a,b,c) & (a,b,c) cong (a9,b9,c9) implies right_angle (a9,b9,c9)

    proof

      assume that

       A1: right_angle (a,b,c) and

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

      per cases ;

        suppose b = c;

        then (a,b) equiv (a9,b9) & (a,b) equiv (a9,c9) & (b,b) equiv (b9,c9) by A2, GTARSKI1:def 3;

        then b9 = c9 by GTARSKI1:def 7, GTARSKI3: 4;

        hence thesis by Satz8p5;

      end;

        suppose

         A3: b <> c;

        set d = ( reflection (b,c)), d9 = ( reflection (b9,c9));

        

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

        now

           Middle (c,b,d) & Middle (c9,b9,d9) by GTARSKI3:def 13;

          hence between (c,b,d) & between (c9,b9,d9) by GTARSKI3:def 12;

          thus (b,a) equiv (b9,a9) & (c,b) equiv (c9,b9) & (c,a) equiv (c9,a9) by A4, Prelim01;

          (b,c) equiv (( reflection (b,b)),( reflection (b,c))) by GTARSKI3: 105;

          then

           A5: (b9,c9) equiv (( reflection (b,b)),( reflection (b,c))) by A4, GTARSKI1:def 6;

          (b9,c9) equiv (( reflection (b9,b9)),( reflection (b9,c9))) by GTARSKI3: 105;

          then (( reflection (b,b)),( reflection (b,c))) equiv (( reflection (b9,b9)),( reflection (b9,c9))) by A5, GTARSKI1:def 6;

          then (b,( reflection (b,c))) equiv (( reflection (b9,b9)),( reflection (b9,c9))) by GTARSKI3: 104;

          hence (b,d) equiv (b9,d9) by GTARSKI3: 104;

        end;

        then (c,b,d,a) AFS (c9,b9,d9,a9) by GTARSKI3:def 2;

        then

         A6: (a,d) equiv (d9,a9) by A3, GTARSKI3: 6, GTARSKI3: 10;

        (a,c) equiv (d9,a9) by A1, A6, Prelim03;

        hence thesis by A4, Prelim03;

      end;

    end;

    definition

      let S be non empty satisfying_Tarski-model TarskiGeometryStruct;

      let A,A9 be Subset of S;

      let x be POINT of S;

      :: GTARSKI4:def2

      pred are_orthogonal A,x,A9 means A is_line & A9 is_line & x in A & x in A9 & (for u,v be POINT of S st u in A & v in A9 holds right_angle (u,x,v));

    end

    definition

      let S be non empty satisfying_Tarski-model TarskiGeometryStruct;

      let A,A9 be Subset of S;

      :: GTARSKI4:def3

      pred are_orthogonal A,A9 means ex x be POINT of S st are_orthogonal (A,x,A9);

    end

    definition

      let S be non empty satisfying_Tarski-model TarskiGeometryStruct;

      let A be Subset of S;

      let x,c,d be POINT of S;

      :: GTARSKI4:def4

      pred are_lorthogonal A,x,c,d means c <> d & are_orthogonal (A,x,( Line (c,d)));

    end

    definition

      let S be non empty satisfying_Tarski-model TarskiGeometryStruct;

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

      :: GTARSKI4:def5

      pred are_orthogonal a,b,x,c,d means a <> b & c <> d & are_orthogonal (( Line (a,b)),x,( Line (c,d)));

    end

    definition

      let S be non empty satisfying_Tarski-model TarskiGeometryStruct;

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

      :: GTARSKI4:def6

      pred are_orthogonal a,b,c,d means a <> b & c <> d & are_orthogonal (( Line (a,b)),( Line (c,d)));

    end

    reserve S for non empty satisfying_Tarski-model TarskiGeometryStruct,

A,A9 for Subset of S,

x,y,z,a,b,c,c9,d,u,p,q,q9 for POINT of S;

    ::$Notion-Name

    theorem :: GTARSKI4:23

    

     Satz8p12: are_orthogonal (A,x,A9) iff are_orthogonal (A9,x,A) by Satz8p2;

    ::$Notion-Name

    theorem :: GTARSKI4:24

    

     Satz8p13: are_orthogonal (A,x,A9) iff A is_line & A9 is_line & x in A & x in A9 & (ex u,v be POINT of S st u in A & v in A9 & u <> x & v <> x & right_angle (u,x,v))

    proof

      hereby

        assume

         A1: are_orthogonal (A,x,A9);

        hence A is_line & A9 is_line & x in A & x in A9;

        consider p,q be POINT of S such that

         A2: p <> q and

         A3: A = ( Line (p,q)) by A1, GTARSKI3:def 11;

        consider p9,q9 be POINT of S such that

         A4: p9 <> q9 and

         A5: A9 = ( Line (p9,q9)) by A1, GTARSKI3:def 11;

        thus ex u,v be POINT of S st u in A & v in A9 & u <> x & v <> x & right_angle (u,x,v)

        proof

          per cases ;

            suppose

             A6: x = p;

            take q;

            

             A7: q in A by A3, GTARSKI3: 83;

            per cases ;

              suppose

               A8: x = p9;

              take q9;

              thus thesis by A8, A4, A6, A2, A1, A5, A7, GTARSKI3: 83;

            end;

              suppose

               A9: x <> p9;

              take p9;

              p9 in A9 by A5, GTARSKI3: 83;

              hence thesis by A9, A6, A2, A3, A1, GTARSKI3: 83;

            end;

          end;

            suppose

             A10: x <> p;

            take p;

            

             A11: p in A by A3, GTARSKI3: 83;

            per cases ;

              suppose

               A12: x = p9;

              take q9;

              q9 in A9 by A5, GTARSKI3: 83;

              hence thesis by A12, A4, A10, A3, GTARSKI3: 83, A1;

            end;

              suppose

               A13: x <> p9;

              take p9;

              thus thesis by A5, GTARSKI3: 83, A13, A11, A10, A1;

            end;

          end;

        end;

      end;

      assume that

       A14: A is_line and

       A15: A9 is_line and

       A16: x in A and

       A17: x in A9 and

       A18: ex u,v be POINT of S st u in A & v in A9 & u <> x & v <> x & right_angle (u,x,v);

      consider u9,v9 be POINT of S such that

       A19: u9 in A and

       A20: v9 in A9 and

       A21: u9 <> x and

       A22: v9 <> x and

       A23: right_angle (u9,x,v9) by A18;

      now

        let u,v be POINT of S;

        assume that

         A24: u in A and

         A25: v in A9;

         Collinear (x,u9,u) by A14, A16, A19, A24, A21, GTARSKI3: 90;

        then right_angle (u,x,v9) by A23, A21, Satz8p3;

        then

         A26: right_angle (v9,x,u) by Satz8p2;

         Collinear (x,v9,v) by A15, A17, A20, A25, A21, GTARSKI3: 90;

        then right_angle (v,x,u) by A22, A26, Satz8p3;

        hence right_angle (u,x,v) by Satz8p2;

      end;

      hence are_orthogonal (A,x,A9) by A14, A15, A16, A17;

    end;

    ::$Notion-Name

    theorem :: GTARSKI4:25

    

     Satz8p14p1: are_orthogonal (A,A9) implies A <> A9

    proof

      assume are_orthogonal (A,A9);

      then

      consider x be POINT of S such that

       A1: are_orthogonal (A,x,A9);

      

       A2: A is_line & A9 is_line & x in A & x in A9 & (ex u,v be POINT of S st u in A & v in A9 & u <> x & v <> x & right_angle (u,x,v)) by A1, Satz8p13;

      consider u,v be POINT of S such that

       A3: u in A and

       A4: v in A9 and

       A5: u <> x and

       A6: v <> x and

       A7: right_angle (u,x,v) by A1, Satz8p13;

      assume A = A9;

      then Collinear (u,x,v) by A2, A3, A4, GTARSKI3: 90;

      hence contradiction by A5, A6, A7, Satz8p9;

    end;

    ::$Notion-Name

    definition

      let S be non empty TarskiGeometryStruct;

      let A,B be Subset of S;

      let x be POINT of S;

      :: GTARSKI4:def7

      pred A,B Is x means A is_line & B is_line & A <> B & x in A & x in B;

    end

    ::$Notion-Name

    theorem :: GTARSKI4:26

    

     Satz8p14p2: are_orthogonal (A,x,A9) iff are_orthogonal (A,A9) & (A,A9) Is x

    proof

      hereby

        assume

         A1: are_orthogonal (A,x,A9);

        hence are_orthogonal (A,A9);

        hence (A,A9) Is x by A1, Satz8p14p1;

      end;

      assume

       A2: are_orthogonal (A,A9) & (A,A9) Is x;

      then ex y be POINT of S st are_orthogonal (A,y,A9);

      hence are_orthogonal (A,x,A9) by A2, GTARSKI3: 88;

    end;

    ::$Notion-Name

    theorem :: GTARSKI4:27

     are_orthogonal (A,x,A9) & are_orthogonal (A,y,A9) implies x = y

    proof

      assume that

       A1: are_orthogonal (A,x,A9) and

       A2: are_orthogonal (A,y,A9);

      A <> A9 by A1, Satz8p14p1, Satz8p14p2;

      hence thesis by A1, A2, GTARSKI3: 89;

    end;

    theorem :: GTARSKI4:28

    

     Satz8p15a: Collinear (a,b,x) & are_orthogonal (a,b,c,x) implies are_orthogonal (a,b,x,c,x)

    proof

      assume

       A2: Collinear (a,b,x);

      assume

       A3: are_orthogonal (a,b,c,x);

      then (( Line (a,b)),( Line (c,x))) Is x by A2, LemmaA1, GTARSKI3:def 11, GTARSKI3: 83, Satz8p14p1;

      hence are_orthogonal (a,b,x,c,x) by A3, Satz8p14p2;

    end;

    ::$Notion-Name

    theorem :: GTARSKI4:29

    

     Satz8p15: a <> b & Collinear (a,b,x) implies ( are_orthogonal (a,b,c,x) iff are_orthogonal (a,b,x,c,x))

    proof

      assume that

       A1: a <> b and

       A2: Collinear (a,b,x);

      thus are_orthogonal (a,b,c,x) implies are_orthogonal (a,b,x,c,x) by Satz8p15a, A2;

      assume are_orthogonal (a,b,x,c,x);

      then c <> x & are_orthogonal (( Line (a,b)),( Line (c,x)));

      hence thesis by A1;

    end;

    ::$Notion-Name

    theorem :: GTARSKI4:30

    a <> b & Collinear (a,b,x) & Collinear (a,b,u) & u <> x implies ( are_orthogonal (a,b,c,x) iff ( not Collinear (a,b,c) & right_angle (c,x,u)))

    proof

      assume that

       A1: a <> b and

       A2: Collinear (a,b,x) and

       A3: Collinear (a,b,u) and

       A4: u <> x;

      hereby

        assume

         A5: are_orthogonal (a,b,c,x);

        then are_orthogonal (a,b,x,c,x) by A2, Satz8p15;

        then

         A6: a <> b & c <> x & are_orthogonal (( Line (a,b)),x,( Line (c,x)));

        

         A7: u in ( Line (a,b)) & c in ( Line (c,x)) by A3, LemmaA1, GTARSKI3: 83;

        then right_angle (c,x,u) by A6, Satz8p2;

        then

         A8: not Collinear (c,x,u) by A4, A5, Satz8p9;

        

         A9: not c in { y where y be POINT of S : Collinear (u,x,y) }

        proof

          assume c in { y where y be POINT of S : Collinear (u,x,y) };

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

          hence contradiction by A8, GTARSKI3: 45;

        end;

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

        proof

          per cases ;

            suppose u = a;

            hence thesis by A4, A1, GTARSKI3: 82, A2, LemmaA1;

          end;

            suppose

             A11: u <> a;

            then ( Line (a,b)) = ( Line (a,u)) by A3, LemmaA1, A1, GTARSKI3: 82;

            hence thesis by A4, A11, GTARSKI3: 82, A2, LemmaA1;

          end;

        end;

        then not c in ( Line (a,b)) by A9, GTARSKI3:def 10;

        hence not Collinear (a,b,c) & right_angle (c,x,u) by A7, A6, Satz8p2, LemmaA1;

      end;

      assume

       A14: not Collinear (a,b,c) & right_angle (c,x,u);

      now

        thus ( Line (a,b)) is_line by A1, GTARSKI3:def 11;

        thus ( Line (c,x)) is_line by A14, A2, GTARSKI3:def 11;

        thus x in ( Line (a,b)) by A2, LemmaA1;

        thus x in ( Line (c,x)) by GTARSKI3: 83;

        thus ex u,v be POINT of S st u in ( Line (a,b)) & v in ( Line (c,x)) & u <> x & v <> x & right_angle (u,x,v)

        proof

          take u, c;

          thus u in ( Line (a,b)) by A3, LemmaA1;

          thus c in ( Line (c,x)) by GTARSKI3: 83;

          thus u <> x by A4;

          thus c <> x by A14, A2;

          thus right_angle (u,x,c) by A14, Satz8p2;

        end;

      end;

      then are_orthogonal (( Line (a,b)),( Line (c,x))) by Satz8p13;

      hence are_orthogonal (a,b,c,x) by A1, A14, A2;

    end;

    ::$Notion-Name

    definition

      let S be non empty satisfying_Tarski-model TarskiGeometryStruct;

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

      :: GTARSKI4:def8

      pred x is_foot a,b,c means Collinear (a,b,x) & are_orthogonal (a,b,c,x);

    end

    ::$Notion-Name

    theorem :: GTARSKI4:31

    

     Satz8p18Uniqueness: x is_foot (a,b,c) & y is_foot (a,b,c) implies x = y

    proof

      assume that

       A1: x is_foot (a,b,c) and

       A2: y is_foot (a,b,c);

      

       A3: Collinear (a,b,y) & are_orthogonal (a,b,c,y) by A2;

      

       A4: c in ( Line (c,x)) & c in ( Line (c,y)) by GTARSKI3: 83;

       are_orthogonal (a,b,x,c,x) & are_orthogonal (a,b,y,c,y) by A1, A3, Satz8p15;

      then are_orthogonal (( Line (a,b)),x,( Line (c,x))) & are_orthogonal (( Line (a,b)),y,( Line (c,y)));

      then right_angle (c,x,y) & right_angle (c,y,x) by A4, Satz8p2;

      hence thesis by Satz8p7;

    end;

    theorem :: GTARSKI4:32

    

     Satz8p18Lemma: not Collinear (a,b,c) & between (b,a,y) & a <> y & between (a,y,z) & (y,z) equiv (y,p) & y <> p & q9 = ( reflection (z,q)) & Middle (c,x,c9) & c <> y & between (q9,y,c9) & Middle (y,p,c) & between (p,y,q) & q <> q9 implies x <> y

    proof

      assume that

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

       A2: between (b,a,y) and

       A3: a <> y and

       A4: between (a,y,z) and

       A5: (y,z) equiv (y,p) and

       A6: y <> p and

       A7: q9 = ( reflection (z,q)) and

       A8: Middle (c,x,c9) and

       A9: c <> y and

       A10: between (q9,y,c9) and

       A11: Middle (y,p,c) and

       A12: between (p,y,q) and

       A13: q <> q9;

      assume

       A14: x = y;

      now

         Collinear (b,a,y) by A2, GTARSKI1:def 17;

        hence y in ( Line (a,b)) by LemmaA1;

        thus a <> y by A3;

        thus a <> b by A1, GTARSKI3: 46;

      end;

      then

       A15: ( Line (a,y)) = ( Line (a,b)) by GTARSKI3: 82;

      now

         Collinear (a,y,z) by A4, GTARSKI1:def 17;

        hence z in ( Line (y,a)) by LemmaA1;

        thus y <> a by A3;

        thus y <> z by A5, A6, GTARSKI1:def 7, GTARSKI3: 4;

      end;

      then

       A16: ( Line (y,z)) = ( Line (a,b)) by A15, GTARSKI3: 82;

      

       A17: ( Line (x,c)) = ( Line (x,c9)) by A8, A9, A14, Prelim10;

       Collinear (x,c9,q9) by A10, A14, GTARSKI1:def 17;

      then

       A18: q9 in ( Line (x,c)) by A17, LemmaA1;

       between (c,p,x) & between (p,x,q) & p <> x by A14, A6, A11, A12, GTARSKI3:def 12, GTARSKI3: 14;

      then between (c,x,q) by GTARSKI3: 19;

      then Collinear (c,x,q) by GTARSKI1:def 17;

      then q in ( Line (c,x)) by LemmaA1;

      then

       A19: ( Line (q,q9)) = ( Line (c,x)) by A13, A9, A14, A18, Prelim11;

       Middle (q,z,q9) by A7, GTARSKI3:def 13;

      then between (q,z,q9) by GTARSKI3:def 12;

      then Collinear (q,z,q9) by GTARSKI1:def 17;

      then Collinear (q,q9,z) by GTARSKI3: 45;

      then z in ( Line (c,x)) by A19, LemmaA1;

      then Collinear (z,c,x) by LemmaA2;

      then Collinear (y,z,c) by A14, GTARSKI3: 45;

      then c in ( Line (a,b)) by A16, LemmaA1;

      then Collinear (c,a,b) by LemmaA2;

      hence contradiction by A1, GTARSKI3: 45;

    end;

    reserve S for non empty satisfying_Lower_Dimension_Axiom satisfying_Tarski-model TarskiGeometryStruct,

a,b,c,p,q,x,y,z,t for POINT of S;

    ::$Notion-Name

    theorem :: GTARSKI4:33

    

     Satz8p18pExistence: not Collinear (a,b,c) implies ex x st x is_foot (a,b,c)

    proof

      assume

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

      consider y such that

       A2: between (b,a,y) and

       A3: (a,y) equiv (a,c) by GTARSKI1:def 8;

      consider p such that

       A4: Middle (y,p,c) by A3, GTARSKI3: 117;

      

       A5: right_angle (a,p,y) by A3, A4, GTARSKI3:def 13;

      consider z such that

       A6: between (a,y,z) and

       A7: (y,z) equiv (y,p) by GTARSKI1:def 8;

      consider q such that

       A8: between (p,y,q) and

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

      set q9 = ( reflection (z,q));

      consider c9 such that

       A10: between (q9,y,c9) and

       A11: (y,c9) equiv (y,c) by GTARSKI1:def 8;

      

       A12: a <> b by A1, GTARSKI3: 46;

      

       A13: a <> y

      proof

        assume a = y;

        then a = c by A3, GTARSKI1:def 7, GTARSKI3: 4;

        then Collinear (a,c,b) by GTARSKI3: 46;

        hence contradiction by A1, GTARSKI3: 45;

      end;

      now

        thus between (a,y,z) by A6;

        thus between (q,y,p) by A8, GTARSKI3: 14;

        (y,a) equiv (y,q) by A9, GTARSKI3: 3;

        then (a,y) equiv (y,q) by GTARSKI3: 6;

        hence (a,y) equiv (q,y) by GTARSKI3: 7;

        thus (y,z) equiv (y,p) by A7;

        thus (a,q) equiv (q,a) by GTARSKI3: 2, GTARSKI3: 6;

        thus (y,q) equiv (y,a) by A9;

      end;

      then

       A14: (a,y,z,q) AFS (q,y,p,a) by GTARSKI3:def 2;

      now

        (p,a) equiv (z,q) by A14, A13, GTARSKI3: 3, GTARSKI3: 10;

        then (a,p) equiv (z,q) by GTARSKI3: 6;

        hence (a,p) equiv (q,z) by GTARSKI3: 7;

        (y,a) equiv (y,q) by A9, GTARSKI3: 3;

        then (a,y) equiv (y,q) by GTARSKI3: 6;

        hence (a,y) equiv (q,y) by GTARSKI3: 7;

        (y,p) equiv (y,z) by A7, GTARSKI3: 4;

        then (p,y) equiv (y,z) by GTARSKI3: 6;

        hence (p,y) equiv (z,y) by GTARSKI3: 7;

      end;

      then (a,p,y) cong (q,z,y) by GTARSKI1:def 3;

      then right_angle (q,z,y) by A5, Satz8p10;

      then

       A15: right_angle (y,z,q) by Satz8p2;

      

       A16: (y,c) equiv (y,c9) by A11, GTARSKI3: 3;

      consider x such that

       A17: Middle (c,x,c9) by A11, GTARSKI3: 3, GTARSKI3: 117;

      

       A18: y <> p

      proof

        assume y = p;

        then (y,c) equiv (y,y) by A4, GTARSKI3: 4, GTARSKI3:def 12;

        then y = c by GTARSKI1:def 7;

        then Collinear (b,a,c) by A2, GTARSKI1:def 17;

        hence contradiction by A1, GTARSKI3: 45;

      end;

      now

         between (q,y,p) & between (y,p,c) by A4, A8, GTARSKI3: 14, GTARSKI3:def 12;

        hence between (q,y,c) by A18, GTARSKI3: 19;

        thus between (q9,y,c9) by A10;

        thus (y,q) equiv (y,q9) by A15;

        thus (y,c) equiv (y,c9) by A11, GTARSKI3: 3;

        thus Middle (q,z,q9) by GTARSKI3:def 13;

        thus Middle (c,x,c9) by A17;

      end;

      then Krippenfigur (q,z,q9,y,c9,x,c) by GTARSKI3:def 14;

      then between (z,y,x) by GTARSKI3: 116;

      then

       A19: Collinear (z,y,x) by GTARSKI1:def 17;

      

       A20: c <> y

      proof

        assume y = c;

        then Collinear (b,a,c) by A2, GTARSKI1:def 17;

        hence contradiction by A1, GTARSKI3: 45;

      end;

      

       A21: y <> z by A7, A18, GTARSKI1:def 7, GTARSKI3: 4;

      

       A22: q <> q9

      proof

        assume q = q9;

        then

         A23: Middle (q,z,q) by GTARSKI3:def 13;

        then

         A24: q = z by GTARSKI3: 97;

        

         A25: y <> q by A23, GTARSKI3: 97, A21;

         Collinear (b,a,y) by A2, GTARSKI1:def 17;

        then

         A26: ( Line (y,a)) = ( Line (a,b)) by A12, A13, GTARSKI3: 82, LemmaA1;

         Collinear (a,y,z) by A6, GTARSKI1:def 17;

        then

         A27: ( Line (y,q)) = ( Line (a,b)) by A13, A21, A26, GTARSKI3: 82, A24, LemmaA1;

         Collinear (y,q,p) by A8, GTARSKI1:def 17;

        then

         A28: ( Line (y,p)) = ( Line (a,b)) by A25, A18, GTARSKI3: 82, A27, LemmaA1;

         between (y,p,c) by A4, GTARSKI3:def 12;

        then Collinear (y,p,c) by GTARSKI1:def 17;

        then c in ( Line (a,b)) by A28, LemmaA1;

        then Collinear (c,a,b) by LemmaA2;

        hence contradiction by A1, GTARSKI3: 45;

      end;

      now

         Collinear (b,a,y) by A2, GTARSKI1:def 17;

        hence y in ( Line (a,b)) by LemmaA1;

        thus a <> y by A13;

        thus a <> b by A1, GTARSKI3: 46;

      end;

      then

       A29: ( Line (a,y)) = ( Line (a,b)) by GTARSKI3: 82;

      now

         Collinear (a,y,z) by A6, GTARSKI1:def 17;

        hence z in ( Line (y,a)) by LemmaA1;

        thus y <> a by A13;

        thus y <> z by A7, A18, GTARSKI1:def 7, GTARSKI3: 4;

      end;

      then

       A30: ( Line (y,z)) = ( Line (a,b)) by A29, GTARSKI3: 82;

      

       A31: c <> x

      proof

        assume c = x;

        then c9 = ( reflection (c,c)) by A17, GTARSKI3:def 13;

        then between (q9,y,c) by A10, GTARSKI3: 104;

        then

         a32: Collinear (y,c,q9) by GTARSKI1:def 17;

         between (y,p,c) by A4, GTARSKI3:def 12;

        then

         A33: Collinear (y,p,c) by GTARSKI1:def 17;

        

         A34: q <> y by A13, A9, GTARSKI3: 4, GTARSKI1:def 7;

        y <> p by A4, A20, Prelim09;

        then

         A35: ( Line (y,p)) = ( Line (y,c)) by A20, A33, GTARSKI3: 82, LemmaA1;

         Collinear (p,y,q) by A8, GTARSKI1:def 17;

        then ( Line (y,q)) = ( Line (y,c)) by A34, A20, GTARSKI3: 82, A35, LemmaA1;

        then

         A37: ( Line (q,q9)) = ( Line (y,c)) by A22, A34, GTARSKI3: 82, a32, LemmaA1;

         Middle (q,z,q9) by GTARSKI3:def 13;

        then between (q,z,q9) by GTARSKI3:def 12;

        then Collinear (q,z,q9) by GTARSKI1:def 17;

        then Collinear (q,q9,z) by GTARSKI3: 45;

        then z in ( Line (y,c)) by A37, LemmaA1;

        then Collinear (z,y,c) by LemmaA2;

        then c in ( Line (y,z)) by LemmaA1;

        then Collinear (c,a,b) by LemmaA2, A30;

        hence contradiction by A1, GTARSKI3: 45;

      end;

      take x;

      now

        now

          thus ( Line (y,z)) is_line by A21, GTARSKI3:def 11;

          thus ( Line (c,x)) is_line by A31, GTARSKI3:def 11;

          thus x in ( Line (y,z)) by LemmaA1, A19;

          thus x in ( Line (c,x)) by GTARSKI3: 83;

          thus ex u,v be POINT of S st u in ( Line (y,z)) & v in ( Line (c,x)) & u <> x & v <> x & right_angle (u,x,v)

          proof

            take y, c;

            thus y in ( Line (y,z)) by GTARSKI3: 83;

            thus c in ( Line (c,x)) by GTARSKI3: 83;

            thus y <> x by Satz8p18Lemma, A1, A2, A13, A7, A18, A17, A20, A10, A4, A8, A22, A6;

            thus c <> x by A31;

            thus right_angle (y,x,c) by A16, A17, GTARSKI3:def 13;

          end;

        end;

        then are_orthogonal (( Line (a,b)),( Line (c,x))) by A30, Satz8p13;

        hence are_orthogonal (a,b,c,x) by GTARSKI3: 46, A1, A31;

        x in ( Line (y,z)) by LemmaA1, A19;

        then Collinear (x,a,b) by LemmaA2, A30;

        hence Collinear (a,b,x) by GTARSKI3: 45;

      end;

      hence thesis;

    end;

    ::$Notion-Name

    theorem :: GTARSKI4:34

    

     Lemma8p20: right_angle (a,b,c) & Middle (( reflection (a,c)),p,( reflection (b,c))) implies right_angle (b,a,p) & (b <> c implies a <> p)

    proof

      assume that

       A1: right_angle (a,b,c) and

       A2: Middle (( reflection (a,c)),p,( reflection (b,c)));

      set d = ( reflection (b,c)), b9 = ( reflection (a,b)), c9 = ( reflection (a,c)), d9 = ( reflection (a,d)), p9 = ( reflection (a,p));

      

       A3: right_angle (b9,b,c)

      proof

        per cases ;

          suppose a = b;

          then ( reflection (a,b)) = b by GTARSKI3: 104;

          hence thesis by Satz8p2, Satz8p5;

        end;

          suppose

           A4: a <> b;

           Middle (b,a,b9) by GTARSKI3:def 13;

          then between (b,a,b9) by GTARSKI3:def 12;

          then Collinear (b,a,b9) by GTARSKI1:def 17;

          hence thesis by A1, A4, Satz8p3;

        end;

      end;

      

       A5: (b9,b) equiv (b,b9)

      proof

        (b9,b) equiv (( reflection (a,( reflection (a,b)))),( reflection (a,b))) by GTARSKI3: 105;

        hence thesis by GTARSKI3: 101;

      end;

      

       A6: (b9,c) equiv (b,c9)

      proof

        (b9,c) equiv (( reflection (a,b9)),( reflection (a,c))) by GTARSKI3: 105;

        hence thesis by GTARSKI3: 101;

      end;

      (b9,b,c) cong (b,b9,c9)

      proof

        (b,c) equiv (b9,c9) by GTARSKI3: 105;

        hence thesis by A5, A6, GTARSKI1:def 3;

      end;

      then

       A7: right_angle (b,b9,c9) by A3, Satz8p10;

      

       A8: ( reflection (b9,c9)) = d9 by Prelim12, GTARSKI3: 100;

      (c9,p,d,b) IFS (d9,p9,c,b)

      proof

        now

          thus between (c9,p,d) by A2, GTARSKI3:def 12;

           between (d,p,c9) by A2, GTARSKI3: 14, GTARSKI3:def 12;

          then between (( reflection (a,d)),( reflection (a,p)),( reflection (a,c9))) by GTARSKI3: 106;

          hence between (d9,p9,c) by GTARSKI3: 101;

          (( reflection (a,c)),( reflection (b,c))) equiv (( reflection (a,( reflection (a,c)))),( reflection (a,( reflection (b,c))))) by GTARSKI3: 105;

          then (( reflection (a,c)),( reflection (b,c))) equiv (c,( reflection (a,( reflection (b,c))))) by GTARSKI3: 101;

          hence (c9,d) equiv (d9,c) by GTARSKI3: 7;

          now

            thus (p,d) equiv (p9,d9) by GTARSKI3: 105;

            

             A9: (p,c9) equiv (p,d) by A2, GTARSKI3:def 12;

            (p,c9) equiv (( reflection (a,p)),( reflection (a,c9))) by GTARSKI3: 105;

            then

             A10: (p,c9) equiv (p9,c) by GTARSKI3: 101;

            (p,d) equiv (( reflection (a,p)),( reflection (a,d))) by GTARSKI3: 105;

            then (p,c9) equiv (( reflection (a,p)),( reflection (a,d))) by A9, GTARSKI3: 5;

            then (( reflection (a,p)),( reflection (a,d))) equiv (p,c9) by GTARSKI3: 4;

            hence (p9,d9) equiv (p9,c) by A10, GTARSKI3: 5;

          end;

          hence (p,d) equiv (p9,c) by GTARSKI3: 5;

          (c9,b) equiv (b,d9) by A8, A7, GTARSKI3: 6;

          hence (c9,b) equiv (d9,b) by GTARSKI3: 7;

           Middle (c,b,d) by GTARSKI3:def 13;

          then (b,d) equiv (b,c) by GTARSKI3: 4, GTARSKI3:def 12;

          then (d,b) equiv (b,c) by GTARSKI3: 6;

          hence (d,b) equiv (c,b) by GTARSKI3: 7;

        end;

        hence thesis by GTARSKI3:def 5;

      end;

      then (b,p) equiv (p9,b) by GTARSKI3: 6, GTARSKI3: 41;

      hence right_angle (b,a,p) by GTARSKI3: 7;

      thus b <> c implies a <> p

      proof

        assume

         A11: b <> c;

        assume

         A12: a = p;

        c = ( reflection (a,c9)) by GTARSKI3: 101

        .= d by A12, A2, GTARSKI3:def 13;

        then Middle (c,b,c) by GTARSKI3:def 13;

        hence thesis by GTARSKI3: 97, A11;

      end;

    end;

    theorem :: GTARSKI4:35

    

     Satz8p21p1: not Collinear (a,b,c) implies ex p, t st are_orthogonal (a,b,p,a) & Collinear (a,b,t) & between (c,t,p)

    proof

      assume

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

      then

       A2: a <> b by GTARSKI3: 46;

      consider x such that

       A3: x is_foot (a,b,c) by A1, Satz8p18pExistence;

       Collinear (a,b,x) & are_orthogonal (a,b,c,x) by A3;

      then are_orthogonal (a,b,x,c,x) by Satz8p15;

      then

       A4: a <> b & c <> x & are_orthogonal (( Line (a,b)),x,( Line (c,x)));

      

       A5: a in ( Line (a,b)) & c in ( Line (c,x)) by GTARSKI3: 83;

      then right_angle (a,x,c) by A4;

      then

       A6: (a,( reflection (x,c))) equiv (a,c) by GTARSKI3: 3;

       Middle (c,a,( reflection (a,c))) by GTARSKI3:def 13;

      then (a,c) equiv (a,( reflection (a,c))) by GTARSKI3:def 12;

      then

      consider p such that

       A7: Middle (( reflection (x,c)),p,( reflection (a,c))) by A6, GTARSKI3: 5, GTARSKI3: 117;

      

       A8: Middle (( reflection (a,c)),p,( reflection (x,c))) by A7, GTARSKI3: 96;

      

       A9: right_angle (a,x,c) by A5, A4;

      then

       A10: right_angle (x,a,p) & a <> p by A1, A3, A8, Lemma8p20;

      now

         Middle (c,x,( reflection (x,c))) by GTARSKI3:def 13;

        hence between (( reflection (x,c)),x,c) by GTARSKI3: 14, GTARSKI3:def 12;

         Middle (c,a,( reflection (a,c))) by GTARSKI3:def 13;

        hence between (( reflection (a,c)),a,c) by GTARSKI3: 14, GTARSKI3:def 12;

        thus between (( reflection (x,c)),p,( reflection (a,c))) by A7, GTARSKI3:def 12;

      end;

      then

      consider t such that

       A11: between (p,t,c) and

       A12: between (x,t,a) by GTARSKI3: 40;

       Collinear (x,t,a) by A12, GTARSKI1:def 17;

      then Collinear (x,a,t) by GTARSKI3: 45;

      then

       A13: t in ( Line (x,a)) by LemmaA1;

      per cases ;

        suppose

         A16: x <> a;

        then ( Line (a,b)) = ( Line (x,a)) by A2, A3, LemmaA1, GTARSKI3: 82;

        then

         a18: Collinear (t,a,b) by LemmaA2, A13;

        take p, t;

        now

          thus a <> b by A1, GTARSKI3: 46;

          thus p <> a by A9, A1, A3, A8, Lemma8p20;

          now

            thus ( Line (a,b)) is_line by A2, GTARSKI3:def 11;

            thus ( Line (p,a)) is_line by A10, GTARSKI3:def 11;

            thus a in ( Line (a,b)) by GTARSKI3: 83;

            thus a in ( Line (p,a)) by GTARSKI3: 83;

            thus ex u,v be POINT of S st u in ( Line (a,b)) & v in ( Line (p,a)) & u <> a & v <> a & right_angle (u,a,v)

            proof

              take x, p;

              thus x in ( Line (a,b)) by A3, LemmaA1;

              thus p in ( Line (p,a)) by GTARSKI3: 83;

              thus x <> a & p <> a by A16, A9, A1, A3, A8, Lemma8p20;

              thus right_angle (x,a,p) by A9, A8, Lemma8p20;

            end;

          end;

          hence are_orthogonal (( Line (a,b)),( Line (p,a))) by Satz8p13;

        end;

        hence thesis by a18, A11, GTARSKI3: 14, GTARSKI3: 45;

      end;

        suppose

         A19: x = a;

        then

         A20: a = t by A12, GTARSKI1:def 10;

         a21:

        now

          thus p <> a by A9, A1, A3, A8, Lemma8p20;

          thus c <> a

          proof

            assume c = a;

            then Collinear (a,c,b) by GTARSKI3: 46;

            hence contradiction by A1, GTARSKI3: 45;

          end;

           Collinear (p,a,c) by A20, A11, GTARSKI1:def 17;

          hence c in ( Line (a,p)) by LemmaA1;

        end;

        take p, t;

         Collinear (a,b,a) & are_orthogonal (a,b,c,a) by A3, A19;

        hence thesis by a21, A11, GTARSKI3: 14, GTARSKI3: 82, A19, A12, GTARSKI1:def 10;

      end;

    end;

    ::$Notion-Name

    theorem :: GTARSKI4:36

    

     Satz8p21: a <> b implies ex p, t st are_orthogonal (a,b,p,a) & Collinear (a,b,t) & between (c,t,p)

    proof

      assume

       A1: a <> b;

      per cases ;

        suppose not Collinear (a,b,c);

        hence thesis by Satz8p21p1;

      end;

        suppose

         A2: Collinear (a,b,c);

        consider c9 such that

         A3: not Collinear (a,b,c9) by A1, GTARSKI3: 92;

        ex p, t st are_orthogonal (a,b,p,a) & Collinear (a,b,t) & between (c9,t,p) by A3, Satz8p21p1;

        hence thesis by A2, GTARSKI3: 15;

      end;

    end;

    theorem :: GTARSKI4:37

    

     Th01: a <> b & a <> p & right_angle (b,a,p) & right_angle (a,b,q) implies not Collinear (p,a,q)

    proof

      assume that

       A1: a <> b and

       A2: a <> p and

       A3: right_angle (b,a,p) and

       A4: right_angle (a,b,q);

      assume

       A5: Collinear (p,a,q);

      now

        

         A6: right_angle (p,a,b) by A3, Satz8p2;

         right_angle (a,b,q) & a <> p & Collinear (a,p,q) by A2, A4, A5, GTARSKI3: 45;

        hence right_angle (q,a,b) by A6, Satz8p3;

        thus right_angle (q,b,a) by A4, Satz8p2;

      end;

      hence contradiction by A1, Satz8p7;

    end;

    

     LemmaA3: for S be non empty satisfying_Lower_Dimension_Axiom satisfying_Tarski-model TarskiGeometryStruct holds for a,b,p be POINT of S st a <> p holds ( reflection (a,p)) <> p

    proof

      let S be non empty satisfying_Lower_Dimension_Axiom satisfying_Tarski-model TarskiGeometryStruct;

      let a,b,p be POINT of S;

      assume

       A1: a <> p;

      assume

       A2: p = ( reflection (a,p));

       Middle (p,a,( reflection (a,p))) by GTARSKI3:def 13;

      hence contradiction by GTARSKI3: 97, A1, A2;

    end;

    theorem :: GTARSKI4:38

    

     Satz8p22lemma: for S be non empty satisfying_Lower_Dimension_Axiom satisfying_Tarski-model TarskiGeometryStruct holds for a,b,p,q,t be POINT of S st (a,p) <= (b,q) & are_orthogonal (a,b,q,b) & are_orthogonal (a,b,p,a) & Collinear (a,b,t) & between (q,t,p) holds ex x be POINT of S st Middle (a,x,b)

    proof

      let S be non empty satisfying_Lower_Dimension_Axiom satisfying_Tarski-model TarskiGeometryStruct;

      let a,b,p,q,t be POINT of S;

      assume that

       A1: (a,p) <= (b,q) and

       A2: are_orthogonal (a,b,q,b) and

       A3: are_orthogonal (a,b,p,a) and

       A4: Collinear (a,b,t) and

       A5: between (q,t,p);

      consider r be POINT of S such that

       A6: between (b,r,q) and

       A7: (a,p) equiv (b,r) by A1, GTARSKI3:def 7;

       between (p,t,q) by A5, GTARSKI3: 14;

      then

      consider x be POINT of S such that

       A8: between (t,x,b) and

       A9: between (r,x,p) by A6, GTARSKI1:def 11;

      

       A10: Collinear (a,b,x)

      proof

        per cases ;

          suppose b = t;

          then x = b by A8, GTARSKI1:def 10;

          then Collinear (b,x,a) by GTARSKI3: 46;

          hence thesis by GTARSKI3: 45;

        end;

          suppose b <> t;

          then

           A12: ( Line (t,b)) = ( Line (a,b)) by A2, GTARSKI3: 82, A4, LemmaA1;

           Collinear (t,x,b) by A8, GTARSKI1:def 17;

          then Collinear (t,b,x) by GTARSKI3: 45;

          then x in ( Line (a,b)) by A12, LemmaA1;

          then Collinear (x,a,b) by LemmaA2;

          hence thesis by GTARSKI3: 45;

        end;

      end;

      a <> b & q <> b & are_orthogonal (( Line (a,b)),( Line (q,b))) by A2;

      then

      consider x9 be POINT of S such that

       A13: are_orthogonal (( Line (a,b)),x9,( Line (q,b)));

      b in ( Line (a,b)) & b in ( Line (q,b)) by GTARSKI3: 83;

      then right_angle (b,x9,b) by A13;

      then b = ( reflection (x9,b)) by GTARSKI1:def 7, GTARSKI3: 4;

      then Middle (b,x9,b) by GTARSKI3: 100;

      then

       A14: x9 = b by GTARSKI3: 97;

      

       A15: a in ( Line (a,b)) & q in ( Line (q,b)) by GTARSKI3: 83;

      a <> b & p <> a & are_orthogonal (( Line (a,b)),( Line (p,a))) by A3;

      then

      consider y be POINT of S such that

       A16: are_orthogonal (( Line (a,b)),y,( Line (p,a)));

      

       A17: b in ( Line (a,b)) & p in ( Line (p,a)) by GTARSKI3: 83;

      then

       A18: right_angle (b,y,p) by A16;

      a in ( Line (a,b)) & a in ( Line (p,a)) by GTARSKI3: 83;

      then right_angle (a,y,a) by A16;

      then a = ( reflection (y,a)) by GTARSKI1:def 7, GTARSKI3: 4;

      then Middle (a,y,a) by GTARSKI3: 100;

      then

       A19: y = a by GTARSKI3: 97;

       right_angle (q,b,a) & q <> b & Collinear (b,q,r) by A13, Satz8p2, A2, A6, A14, A15, Prelim08a;

      then

       A20: right_angle (r,b,a) by Satz8p3;

      

       A21: not Collinear (b,a,p) & not Collinear (a,b,q) by A3, A15, A14, A13, A17, A16, A19, A2, Satz8p9;

      

       A22: r <> b by A3, A7, GTARSKI1: 5;

      now

        thus not Collinear (a,p,b) by A21, GTARSKI3: 45;

        thus p <> r

        proof

          assume

           A23: p = r;

          then p = x by A9, GTARSKI1: 8;

          then b = r by A20, A2, Satz8p9, A10, A23, Satz8p2;

          hence contradiction by A23, A17, A19, A2, A16, Satz8p8;

        end;

        thus (a,p) equiv (b,r) by A7;

        

         A24: x <> a

        proof

          assume x = a;

          then

           A25: Collinear (r,a,p) by A9, GTARSKI1:def 17;

           right_angle (a,b,r) by A20, Satz8p2;

          then not Collinear (p,a,r) by A3, A18, A19, Th01;

          hence contradiction by A25, GTARSKI3: 45;

        end;

        thus (p,b) equiv (r,a)

        proof

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

          consider r9 be POINT of S such that

           A26: between (p9,x,r9) and

           A27: (x,r9) equiv (x,r) by GTARSKI1:def 8;

          consider m be POINT of S such that

           A28: Middle (r9,m,r) by A27, GTARSKI3: 117;

          

           A29: Middle (r,m,r9) by A28, GTARSKI3: 96;

          

           A30: right_angle (x,a,p) by A17, A19, A10, A2, A16, Satz8p3;

          

           A31: p <> p9 by A3, LemmaA3;

           Collinear (p,a,p9) by GTARSKI3:def 13, Prelim08;

          then

           A32: ( Line (a,p)) = ( Line (p,p9)) by A31, A3, Prelim07;

          

           A33: not Collinear (x,p,p9)

          proof

            assume Collinear (x,p,p9);

            then Collinear (p,p9,x) by GTARSKI3: 45;

            then x in ( Line (a,p)) by A32, LemmaA1;

            hence contradiction by A30, A24, A3, Satz8p9, LemmaA2;

          end;

           between (p9,x,r9) & between (p,x,r) & (x,p9) equiv (x,p) & (x,r9) equiv (x,r) & Middle (p9,a,p) & Middle (r9,m,r) by A9, GTARSKI3: 14, A26, A28, A30, Prelim01, A27, GTARSKI3: 96, GTARSKI3:def 13;

          then

           A34: between (a,x,m) by GTARSKI3: 115;

          

           A35: x <> m

          proof

            assume

             A36: x = m;

             Collinear (x,r9,p9) by A26, Prelim08a;

            then

             A37: p9 in ( Line (x,r9)) by LemmaA1;

            

             A38: Collinear (x,r,r9) by A36, A28, Prelim08a;

            per cases ;

              suppose

               A39: x <> r;

              then x <> r9 by A27, GTARSKI1: 5, GTARSKI3: 4;

              then ( Line (x,r)) = ( Line (x,r9)) by A39, A38, Prelim07;

              then Collinear (p9,x,r) by A37, LemmaA2;

              then

               A40: Collinear (x,r,p9) by GTARSKI3: 45;

               Collinear (x,r,p) by A9, Prelim08a;

              hence contradiction by A33, A39, Prelim08b, A40;

            end;

              suppose x = r;

              hence contradiction by A20, A10, A2, A22, Satz8p2, Satz8p9;

            end;

          end;

           Collinear (a,x,m) by A34, GTARSKI1:def 17;

          then

           A41: m in ( Line (a,x)) by LemmaA1;

          then

           A43: m in ( Line (a,b)) by A24, A2, GTARSKI3: 82, A10, LemmaA1;

          

           A44: ( reflection (m,r)) = r9 by A28, GTARSKI3: 96, GTARSKI3: 100;

          now

            thus a <> b by A2;

            thus

             A45: r <> m by A43, LemmaA2, A20, A2, A22, Satz8p9;

            thus are_orthogonal (( Line (a,b)),( Line (r,m)))

            proof

              now

                thus ( Line (a,b)) is_line by A2, GTARSKI3:def 11;

                thus ( Line (r,m)) is_line by A45, GTARSKI3:def 11;

                thus m in ( Line (a,b)) by A10, LemmaA1, A41, A24, A2, GTARSKI3: 82;

                thus m in ( Line (r,m)) by GTARSKI3: 83;

                

                 b3: x in ( Line (a,b)) by A10, LemmaA1;

                

                 b4: r in ( Line (r,m)) by GTARSKI3: 83;

                 right_angle (x,m,r) by A44, GTARSKI3: 4, A27;

                hence ex u,v be POINT of S st u <> m & v <> m & u in ( Line (a,b)) & v in ( Line (r,m)) & right_angle (u,m,v) by A35, A45, b3, b4;

              end;

              hence thesis by Satz8p13;

            end;

          end;

          then

           A46: are_orthogonal (a,b,r,m);

           Collinear (m,a,b) by A43, LemmaA2;

          then

           A47: m is_foot (a,b,r) by A46, GTARSKI3: 45;

          now

            thus Collinear (a,b,b) by Prelim05;

            thus are_orthogonal (a,b,r,b)

            proof

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

              now

                thus A is_line by A2, GTARSKI3:def 11;

                thus A9 is_line by A22, GTARSKI3:def 11;

                thus b in A & b in A9 by GTARSKI3: 83;

                thus ex u,v be POINT of S st u in A & v in A9 & u <> b & v <> b & right_angle (u,b,v)

                proof

                  take a, r;

                  thus a in A by GTARSKI3: 83;

                  thus r in A9 by GTARSKI3: 83;

                  thus a <> b by A2;

                  thus r <> b by A3, A7, GTARSKI1: 5;

                  thus right_angle (a,b,r) by A20, Satz8p2;

                end;

              end;

              then are_orthogonal (A,A9) by Satz8p13;

              hence thesis by A3, A7, GTARSKI1: 5;

            end;

          end;

          then

           A48: b is_foot (a,b,r);

          then

           A49: m = b by A47, Satz8p18Uniqueness;

          

           A50: Middle (r,b,r9) by A29, A47, A48, Satz8p18Uniqueness;

          

           A51: Middle (p,a,p9) by GTARSKI3:def 13;

          now

            thus

             A52: Middle (p9,a,p) by GTARSKI3: 96, GTARSKI3:def 13;

            hence between (p9,a,p) by GTARSKI3:def 12;

            thus between (r,b,r9) by A50, GTARSKI3:def 12;

            

             A53: (a,p) equiv (a,p9) by A51, GTARSKI3:def 12;

            

             A54: (m,r9) equiv (m,r) by A28, GTARSKI3:def 12;

             between (p9,a,p) & between (r,m,r9) & (p9,a) equiv (r,m) & (a,p) equiv (m,r9) by A53, A29, GTARSKI3:def 12, A7, A54, A49, Prelim03, A52;

            hence (p9,p) equiv (r,r9) by GTARSKI3: 11;

            thus (a,p) equiv (b,r9) by A7, A54, A49, Prelim03;

            (p9,r) equiv (p9,r) by GTARSKI3: 1;

            hence (p9,r) equiv (r,p9) by Prelim01;

             between (p,x,r) & between (p9,x,r9) & (p,x) equiv (p9,x) & (x,r) equiv (x,r9) by A26, A30, A9, GTARSKI3: 14, Prelim01, A27;

            then (p,r) equiv (p9,r9) by GTARSKI3: 11;

            hence (p,r) equiv (r9,p9) by Prelim01;

          end;

          then (p9,a,p,r) IFS (r,b,r9,p9) by GTARSKI3:def 5;

          then (a,r) equiv (b,p9) by GTARSKI3: 41;

          hence thesis by A18, A19, Prelim03;

        end;

        thus Collinear (a,x,b) by A10, GTARSKI3: 45;

         Collinear (r,x,p) by A9, GTARSKI1:def 17;

        hence Collinear (p,x,r) by GTARSKI3: 45;

      end;

      then Middle (a,x,b) & Middle (p,x,r) by GTARSKI3: 112;

      hence thesis;

    end;

    ::$Notion-Name

    theorem :: GTARSKI4:39

    

     Satz8p22: for S be non empty satisfying_Lower_Dimension_Axiom satisfying_Tarski-model TarskiGeometryStruct holds for a,b be POINT of S holds ex x be POINT of S st Middle (a,x,b)

    proof

      let S be non empty satisfying_Lower_Dimension_Axiom satisfying_Tarski-model TarskiGeometryStruct;

      let a,b be POINT of S;

      set c = the POINT of S;

      per cases ;

        suppose a = b;

        hence thesis by GTARSKI3: 97;

      end;

        suppose

         A1: a <> b;

        then

        consider q,t be POINT of S such that

         A2: are_orthogonal (b,a,q,b) and Collinear (b,a,t) and between (c,t,q) by Satz8p21;

        

         A3: are_orthogonal (a,b,q,b) by A2;

        consider p,t9 be POINT of S such that

         A4: are_orthogonal (a,b,p,a) and

         A5: Collinear (a,b,t9) and

         A6: between (q,t9,p) by A1, Satz8p21;

        per cases by GTARSKI3: 64;

          suppose (a,p) <= (b,q);

          hence thesis by Satz8p22lemma, A3, A4, A5, A6;

        end;

          suppose

           A7: (b,q) <= (a,p);

           are_orthogonal (b,a,p,a) & are_orthogonal (b,a,q,b) & Collinear (b,a,t9) & between (p,t9,q) by A6, A4, A2, A5, GTARSKI3: 14, GTARSKI3: 45;

          then ex x be POINT of S st Middle (b,x,a) by Satz8p22lemma, A7;

          hence thesis by GTARSKI3: 96;

        end;

      end;

    end;

    definition

      let S be non empty satisfying_Lower_Dimension_Axiom satisfying_Tarski-model TarskiGeometryStruct;

      let a,b be POINT of S;

      :: GTARSKI4:def9

      func Midpoint (a,b) -> POINT of S means Middle (a,it ,b);

      existence by Satz8p22;

      uniqueness by GTARSKI3: 108;

    end

    ::$Notion-Name

    theorem :: GTARSKI4:40

    for S be non empty satisfying_Lower_Dimension_Axiom satisfying_Tarski-model TarskiGeometryStruct holds for a,b,p,q,r,t be POINT of S st are_orthogonal (p,a,a,b) & are_orthogonal (q,b,a,b) & Collinear (a,b,t) & between (p,t,q) & between (b,r,q) & (a,p) equiv (b,r) holds ex x be POINT of S st Middle (a,x,b) & Middle (p,x,r)

    proof

      let S be non empty satisfying_Lower_Dimension_Axiom satisfying_Tarski-model TarskiGeometryStruct;

      let a,b,p,q,r,t be POINT of S;

      assume that

       A1: are_orthogonal (p,a,a,b) and

       A2: are_orthogonal (q,b,a,b) and

       A3: Collinear (a,b,t) and

       A4: between (p,t,q) and

       A5: between (b,r,q) and

       A6: (a,p) equiv (b,r);

      

       A7: q <> b & a <> b & are_orthogonal (( Line (q,b)),( Line (a,b))) by A2;

      

       A7BIS: are_orthogonal (( Line (p,a)),( Line (a,b))) by A1;

      consider x be POINT of S such that

       A8: between (t,x,b) and

       A9: between (r,x,p) by A4, A5, GTARSKI1:def 11;

      

       A10: Collinear (a,b,x)

      proof

        per cases ;

          suppose b = t;

          then x = b by A8, GTARSKI1:def 10;

          then Collinear (b,x,a) by GTARSKI3: 46;

          hence thesis by GTARSKI3: 45;

        end;

          suppose b <> t;

          then

           A12: ( Line (t,b)) = ( Line (a,b)) by A2, GTARSKI3: 82, A3, LemmaA1;

           Collinear (t,x,b) by A8, GTARSKI1:def 17;

          then Collinear (t,b,x) by GTARSKI3: 45;

          then x in ( Line (a,b)) by A12, LemmaA1;

          then Collinear (x,a,b) by LemmaA2;

          hence thesis by GTARSKI3: 45;

        end;

      end;

      consider x9 be POINT of S such that

       A13: are_orthogonal (( Line (a,b)),x9,( Line (q,b))) by A7, Satz8p12;

      b in ( Line (a,b)) & b in ( Line (q,b)) by GTARSKI3: 83;

      then right_angle (b,x9,b) by A13;

      then b = ( reflection (x9,b)) by GTARSKI1:def 7, GTARSKI3: 4;

      then Middle (b,x9,b) by GTARSKI3: 100;

      then

       A14: x9 = b by GTARSKI3: 97;

      

       A15: a in ( Line (a,b)) & q in ( Line (q,b)) by GTARSKI3: 83;

      consider y be POINT of S such that

       A16: are_orthogonal (( Line (a,b)),y,( Line (p,a))) by A7BIS, Satz8p12;

      

       A17: b in ( Line (a,b)) & p in ( Line (p,a)) by GTARSKI3: 83;

      then

       A18: right_angle (b,y,p) by A16;

      a in ( Line (a,b)) & a in ( Line (p,a)) by GTARSKI3: 83;

      then right_angle (a,y,a) by A16;

      then a = ( reflection (y,a)) by GTARSKI1:def 7, GTARSKI3: 4;

      then Middle (a,y,a) by GTARSKI3: 100;

      then

       A19: y = a by GTARSKI3: 97;

       right_angle (q,b,a) & q <> b & Collinear (b,q,r) by A13, Satz8p2, A2, A5, A14, A15, Prelim08a;

      then

       A20: right_angle (r,b,a) by Satz8p3;

      

       A21: not Collinear (b,a,p) & not Collinear (a,b,q) by A15, A14, A13, A17, A16, A19, A2, Satz8p9, A1;

      

       A22: r <> b by A6, GTARSKI1: 5, A1;

      now

        thus not Collinear (a,p,b) by A21, GTARSKI3: 45;

        thus p <> r

        proof

          assume

           A23: p = r;

          then p = x by A9, GTARSKI1: 8;

          then b = r by A20, A2, Satz8p9, A10, A23, Satz8p2;

          hence contradiction by A23, A17, A19, A2, A16, Satz8p8;

        end;

        thus (a,p) equiv (b,r) by A6;

        

         A24: x <> a

        proof

          assume x = a;

          then

           A25: Collinear (r,a,p) by A9, GTARSKI1:def 17;

           right_angle (a,b,r) by A20, Satz8p2;

          then not Collinear (p,a,r) by A18, A19, Th01, A1;

          hence contradiction by A25, GTARSKI3: 45;

        end;

        thus (p,b) equiv (r,a)

        proof

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

          consider r9 be POINT of S such that

           A26: between (p9,x,r9) and

           A27: (x,r9) equiv (x,r) by GTARSKI1:def 8;

          consider m be POINT of S such that

           A28: Middle (r9,m,r) by A27, GTARSKI3: 117;

          

           A29: Middle (r,m,r9) by A28, GTARSKI3: 96;

          

           A30: right_angle (x,a,p) by A17, A19, A10, A2, A16, Satz8p3;

          

           A31: p <> p9 by A1, LemmaA3;

           Collinear (p,a,p9) by GTARSKI3:def 13, Prelim08;

          then

           A32: ( Line (a,p)) = ( Line (p,p9)) by A31, Prelim07, A1;

          

           A33: not Collinear (x,p,p9)

          proof

            assume Collinear (x,p,p9);

            then Collinear (p,p9,x) by GTARSKI3: 45;

            then x in ( Line (a,p)) by A32, LemmaA1;

            hence contradiction by A30, A24, Satz8p9, A1, LemmaA2;

          end;

           between (p9,x,r9) & between (p,x,r) & (x,p9) equiv (x,p) & (x,r9) equiv (x,r) & Middle (p9,a,p) & Middle (r9,m,r) by A9, GTARSKI3: 14, A26, A28, A30, Prelim01, A27, GTARSKI3: 96, GTARSKI3:def 13;

          then

           A34: between (a,x,m) by GTARSKI3: 115;

          

           A35: x <> m

          proof

            assume

             A36: x = m;

             Collinear (x,r9,p9) by A26, Prelim08a;

            then

             A37: p9 in ( Line (x,r9)) by LemmaA1;

            

             A38: Collinear (x,r,r9) by A36, A28, Prelim08a;

            per cases ;

              suppose

               A39: x <> r;

              then x <> r9 by A27, GTARSKI1: 5, GTARSKI3: 4;

              then ( Line (x,r)) = ( Line (x,r9)) by A39, A38, Prelim07;

              then Collinear (p9,x,r) by A37, LemmaA2;

              then

               A40: Collinear (x,r,p9) by GTARSKI3: 45;

               Collinear (x,r,p) by A9, Prelim08a;

              hence contradiction by A33, A40, A39, Prelim08b;

            end;

              suppose x = r;

              hence contradiction by A20, A10, A2, A22, Satz8p2, Satz8p9;

            end;

          end;

           Collinear (a,x,m) by A34, GTARSKI1:def 17;

          then

           A41: m in ( Line (a,x)) by LemmaA1;

          then

           A43: m in ( Line (a,b)) by A24, A2, GTARSKI3: 82, A10, LemmaA1;

          

           A44: ( reflection (m,r)) = r9 by A28, GTARSKI3: 96, GTARSKI3: 100;

          now

            thus a <> b by A2;

            thus

             A45: r <> m by A43, LemmaA2, A20, A2, A22, Satz8p9;

            thus are_orthogonal (( Line (a,b)),( Line (r,m)))

            proof

              now

                thus ( Line (a,b)) is_line by A2, GTARSKI3:def 11;

                thus ( Line (r,m)) is_line by A45, GTARSKI3:def 11;

                thus m in ( Line (a,b)) by A10, LemmaA1, A41, A24, A2, GTARSKI3: 82;

                thus m in ( Line (r,m)) by GTARSKI3: 83;

                

                 B3: x in ( Line (a,b)) by A10, LemmaA1;

                

                 B4: r in ( Line (r,m)) by GTARSKI3: 83;

                 right_angle (x,m,r) by A44, GTARSKI3: 4, A27;

                hence ex u,v be POINT of S st u <> m & v <> m & u in ( Line (a,b)) & v in ( Line (r,m)) & right_angle (u,m,v) by A35, A45, B3, B4;

              end;

              hence thesis by Satz8p13;

            end;

          end;

          then

           A46: are_orthogonal (a,b,r,m);

           Collinear (m,a,b) by A43, LemmaA2;

          then

           A47: m is_foot (a,b,r) by A46, GTARSKI3: 45;

          now

            thus Collinear (a,b,b) by Prelim05;

            thus are_orthogonal (a,b,r,b)

            proof

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

              now

                thus A is_line by A2, GTARSKI3:def 11;

                thus A9 is_line by A22, GTARSKI3:def 11;

                thus b in A & b in A9 by GTARSKI3: 83;

                thus ex u,v be POINT of S st u in A & v in A9 & u <> b & v <> b & right_angle (u,b,v)

                proof

                  take a, r;

                  thus a in A by GTARSKI3: 83;

                  thus r in A9 by GTARSKI3: 83;

                  thus a <> b by A2;

                  thus r <> b by A6, GTARSKI1: 5, A1;

                  thus right_angle (a,b,r) by A20, Satz8p2;

                end;

              end;

              then are_orthogonal (A,A9) by Satz8p13;

              hence thesis by A6, GTARSKI1: 5, A1;

            end;

          end;

          then

           A48: b is_foot (a,b,r);

          then

           A49: m = b by A47, Satz8p18Uniqueness;

          

           A50: Middle (r,b,r9) by A29, A47, A48, Satz8p18Uniqueness;

          now

            

             A51: Middle (p,a,p9) by GTARSKI3:def 13;

            thus

             A52: Middle (p9,a,p) by GTARSKI3: 96, GTARSKI3:def 13;

            hence between (p9,a,p) by GTARSKI3:def 12;

            thus between (r,b,r9) by A50, GTARSKI3:def 12;

            

             A53: (a,p) equiv (a,p9) by A51, GTARSKI3:def 12;

            

             A54: (m,r9) equiv (m,r) by A28, GTARSKI3:def 12;

             between (p9,a,p) & between (r,m,r9) & (p9,a) equiv (r,m) & (a,p) equiv (m,r9) by A53, A29, GTARSKI3:def 12, A6, A54, A49, Prelim03, A52;

            hence (p9,p) equiv (r,r9) by GTARSKI3: 11;

            thus (a,p) equiv (b,r9) by A6, A54, A49, Prelim03;

            (p9,r) equiv (p9,r) by GTARSKI3: 1;

            hence (p9,r) equiv (r,p9) by Prelim01;

             between (p,x,r) & between (p9,x,r9) & (p,x) equiv (p9,x) & (x,r) equiv (x,r9) by A26, A30, A9, GTARSKI3: 14, Prelim01, A27;

            then (p,r) equiv (p9,r9) by GTARSKI3: 11;

            hence (p,r) equiv (r9,p9) by Prelim01;

          end;

          then (p9,a,p,r) IFS (r,b,r9,p9) by GTARSKI3:def 5;

          then (a,r) equiv (b,p9) by GTARSKI3: 41;

          hence thesis by A18, A19, Prelim03;

        end;

        thus Collinear (a,x,b) by A10, GTARSKI3: 45;

         Collinear (r,x,p) by A9, GTARSKI1:def 17;

        hence Collinear (p,x,r) by GTARSKI3: 45;

      end;

      then Middle (a,x,b) & Middle (p,x,r) by GTARSKI3: 112;

      hence thesis;

    end;

    begin

    theorem :: GTARSKI4:41

    for a,b,c,d,x,p,q be POINT of S holds c in ( Line (a,b)) & d in ( Line (a,b)) & a <> b & c <> d implies ( Line (a,b)) = ( Line (c,d)) by Prelim11;

    theorem :: GTARSKI4:42

    for a,b,c,d,x,p,q be POINT of S holds c in ( Line (a,b)) & d in ( Line (a,b)) & c <> d & are_orthogonal (a,b,x,p,q) implies are_orthogonal (c,d,x,p,q) by Prelim11;

    theorem :: GTARSKI4:43

    for a,b,c,d,p,q be POINT of S holds p in ( Line (a,b)) & q in ( Line (a,b)) & a <> b & are_orthogonal (p,q,c,d) implies are_orthogonal (a,b,c,d) by Prelim11;

    theorem :: GTARSKI4:44

    for a,b,c,d be POINT of S holds a <> b & b <> c & c <> d & a <> c & a <> d & b <> d & are_orthogonal (b,a,a,c) & Collinear (a,c,d) implies are_orthogonal (b,a,a,d)

    proof

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

      assume

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

      then

       A3: d in ( Line (a,c)) by LemmaA1;

      a in ( Line (a,c)) by GTARSKI3: 83;

      hence thesis by A1, A3, Prelim11;

    end;

    theorem :: GTARSKI4:45

    for a,b,p,q be POINT of S holds are_orthogonal (a,b,p,q) implies are_orthogonal (a,b,q,p);

    theorem :: GTARSKI4:46

    

     ExtPerp5: for a,b,c,d,p,q be POINT of S holds p in ( Line (a,b)) & q in ( Line (a,b)) & p <> q & are_orthogonal (a,b,c,d) implies are_orthogonal (p,q,c,d) by Prelim11;

    theorem :: GTARSKI4:47

    for a,b,c,d,p,q be POINT of S holds Collinear (a,b,p) & Collinear (a,b,q) & p <> q & are_orthogonal (a,b,c,d) implies are_orthogonal (p,q,c,d)

    proof

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

      assume that

       A1: Collinear (a,b,p) and

       A2: Collinear (a,b,q) & p <> q & are_orthogonal (a,b,c,d);

      

       A3: p in ( Line (a,b)) by A1, LemmaA1;

      q in ( Line (a,b)) by A2, LemmaA1;

      hence thesis by ExtPerp5, A3, A2;

    end;

    theorem :: GTARSKI4:48

    for a,b,c,d,p,q be POINT of S holds p in ( Line (a,b)) & q in ( Line (a,b)) & p <> q & a <> b & are_orthogonal (c,d,p,q) implies are_orthogonal (c,d,a,b) by Prelim11;