translac.miz



    begin

    reserve AS for AffinSpace,

a,b,c,d,p,q,r,s,x for Element of AS;

    definition

      let AS;

      :: TRANSLAC:def1

      attr AS is Fanoian means for a, b, c, d st (a,b) // (c,d) & (a,c) // (b,d) & (a,d) // (b,c) holds LIN (a,b,c);

    end

    

     Lm1: LIN (a,b,c) & a <> b & a <> c & b <> c & not LIN (a,b,p) implies ex x st LIN (p,a,x) & p <> x & a <> x

    proof

      assume that

       A1: LIN (a,b,c) and

       A2: a <> b and

       A3: a <> c and

       A4: b <> c and

       A5: not LIN (a,b,p);

      (a,b) // (a,c) by A1, AFF_1:def 1;

      then (b,a) // (a,c) by AFF_1: 4;

      then

      consider x such that

       A6: (p,a) // (a,x) and

       A7: (p,b) // (c,x) by A2, DIRAF: 40;

       A8:

      now

        assume p = x;

        then (p,b) // (p,c) by A7, AFF_1: 4;

        then LIN (p,b,c) by AFF_1:def 1;

        then

         A9: LIN (b,c,p) by AFF_1: 6;

         LIN (b,c,a) & LIN (b,c,b) by A1, AFF_1: 6, AFF_1: 7;

        hence contradiction by A4, A5, A9, AFF_1: 8;

      end;

       A10:

      now

        assume a = x;

        then

         A11: (p,b) // (a,c) by A7, AFF_1: 4;

        (a,b) // (a,c) by A1, AFF_1:def 1;

        then (a,b) // (p,b) by A3, A11, AFF_1: 5;

        then (b,a) // (b,p) by AFF_1: 4;

        then LIN (b,a,p) by AFF_1:def 1;

        hence contradiction by A5, AFF_1: 6;

      end;

      (a,p) // (a,x) by A6, AFF_1: 4;

      then LIN (a,p,x) by AFF_1:def 1;

      then LIN (p,a,x) by AFF_1: 6;

      hence thesis by A8, A10;

    end;

    

     Lm2: LIN (a,b,c) & a <> b & a <> c & b <> c & not LIN (a,b,p) & LIN (a,b,q) implies ex x st LIN (p,q,x) & p <> x & q <> x

    proof

      assume that

       A1: LIN (a,b,c) and

       A2: a <> b and

       A3: a <> c and

       A4: b <> c and

       A5: not LIN (a,b,p) and

       A6: LIN (a,b,q);

       A7:

      now

        assume that

         A8: q = c and q <> a and q <> b;

         A9:

        now

          assume

           A10: LIN (q,a,p);

           LIN (c,a,b) & LIN (c,a,a) by A1, AFF_1: 6, AFF_1: 7;

          hence contradiction by A3, A5, A8, A10, AFF_1: 8;

        end;

         LIN (q,a,b) by A6, AFF_1: 6;

        hence thesis by A2, A3, A4, A8, A9, Lm1;

      end;

       A11:

      now

        assume that

         A12: q <> a and

         A13: q <> b and q <> c;

         A14:

        now

          assume LIN (q,a,p);

          then LIN (a,q,p) by AFF_1: 6;

          then

           A15: (a,q) // (a,p) by AFF_1:def 1;

           LIN (a,q,b) by A6, AFF_1: 6;

          then (a,q) // (a,b) by AFF_1:def 1;

          then (a,b) // (a,p) by A12, A15, AFF_1: 5;

          hence contradiction by A5, AFF_1:def 1;

        end;

         LIN (q,a,b) by A6, AFF_1: 6;

        hence thesis by A2, A12, A13, A14, Lm1;

      end;

      now

        assume that

         A16: q = b and q <> a and q <> c;

         LIN (q,a,c) & not LIN (q,a,p) by A1, A5, A16, AFF_1: 6;

        hence thesis by A2, A3, A4, A16, Lm1;

      end;

      hence thesis by A1, A2, A3, A4, A5, A7, A11, Lm1;

    end;

    

     Lm3: LIN (a,b,c) & a <> b & a <> c & b <> c & not LIN (a,b,p) & (p,q) // (a,b) implies ex x st LIN (p,q,x) & p <> x & q <> x

    proof

      assume that

       A1: LIN (a,b,c) and

       A2: a <> b and

       A3: a <> c and

       A4: b <> c and

       A5: not LIN (a,b,p) and

       A6: (p,q) // (a,b);

      

       A7: b <> q

      proof

        assume b = q;

        then (b,p) // (b,a) by A6, AFF_1: 4;

        then LIN (b,p,a) by AFF_1:def 1;

        hence contradiction by A5, AFF_1: 6;

      end;

      

       A8: a <> q

      proof

        assume a = q;

        then (a,p) // (a,b) by A6, AFF_1: 4;

        then LIN (a,p,b) by AFF_1:def 1;

        hence contradiction by A5, AFF_1: 6;

      end;

      

       A9: not LIN (a,b,q)

      proof

        assume

         A10: LIN (a,b,q);

        then (a,b) // (a,q) by AFF_1:def 1;

        then (p,q) // (a,q) by A2, A6, AFF_1: 5;

        then (q,p) // (q,a) by AFF_1: 4;

        then LIN (q,p,a) by AFF_1:def 1;

        then

         A11: LIN (q,a,p) by AFF_1: 6;

        

         A12: LIN (q,a,a) by AFF_1: 7;

         LIN (q,a,b) by A10, AFF_1: 6;

        hence contradiction by A5, A8, A11, A12, AFF_1: 8;

      end;

      consider r such that

       A13: (b,c) // (q,r) and

       A14: (b,q) // (c,r) by DIRAF: 40;

       LIN (b,a,c) by A1, AFF_1: 6;

      then (b,a) // (b,c) by AFF_1:def 1;

      then (b,a) // (q,r) by A4, A13, AFF_1: 5;

      then (a,b) // (q,r) by AFF_1: 4;

      then (p,q) // (q,r) by A2, A6, AFF_1: 5;

      then (q,p) // (q,r) by AFF_1: 4;

      then LIN (q,p,r) by AFF_1:def 1;

      then

       A15: LIN (p,q,r) by AFF_1: 6;

      

       A16: not LIN (a,c,p)

      proof

        assume

         A17: LIN (a,c,p);

         LIN (a,c,b) & LIN (a,c,a) by A1, AFF_1: 6, AFF_1: 7;

        hence contradiction by A3, A5, A17, AFF_1: 8;

      end;

       A18:

      now

        consider s such that

         A19: (b,a) // (q,s) and

         A20: (b,q) // (a,s) by DIRAF: 40;

        

         A21: q <> s

        proof

          assume q = s;

          then (q,b) // (q,a) by A20, AFF_1: 4;

          then LIN (q,b,a) by AFF_1:def 1;

          hence contradiction by A9, AFF_1: 6;

        end;

        assume

         A22: p = r;

         A23:

        now

          assume p = s;

          then (a,p) // (c,p) by A7, A14, A22, A20, AFF_1: 5;

          then (p,a) // (p,c) by AFF_1: 4;

          then LIN (p,a,c) by AFF_1:def 1;

          hence contradiction by A16, AFF_1: 6;

        end;

        (a,b) // (q,s) by A19, AFF_1: 4;

        then (p,q) // (q,s) by A2, A6, AFF_1: 5;

        then (q,p) // (q,s) by AFF_1: 4;

        then LIN (q,p,s) by AFF_1:def 1;

        then LIN (p,q,s) by AFF_1: 6;

        hence thesis by A23, A21;

      end;

      q <> r

      proof

        assume q = r;

        then (q,b) // (q,c) by A14, AFF_1: 4;

        then LIN (q,b,c) by AFF_1:def 1;

        then

         A24: LIN (b,c,q) by AFF_1: 6;

         LIN (b,c,a) & LIN (b,c,b) by A1, AFF_1: 6, AFF_1: 7;

        hence contradiction by A4, A9, A24, AFF_1: 8;

      end;

      hence thesis by A15, A18;

    end;

    theorem :: TRANSLAC:1

    

     Th1: (ex a, b, c st LIN (a,b,c) & a <> b & a <> c & b <> c) implies for p, q holds ex r st LIN (p,q,r) & p <> r & q <> r

    proof

      given a, b, c such that

       A1: LIN (a,b,c) and

       A2: a <> b and

       A3: a <> c and

       A4: b <> c;

      let p, q;

       A5:

      now

        assume that

         A6: LIN (a,b,p) and

         A7: LIN (a,b,q);

        

         A8: LIN (a,b,b) by AFF_1: 7;

        

         A9: LIN (a,b,a) by AFF_1: 7;

        now

          assume

           A10: p = c or q = c;

          now

            assume p <> a or q <> b;

             A11:

            now

              assume that

               A12: p = c and

               A13: p <> a;

              q = b implies thesis by A1, A2, A9, A8, A12, A13, AFF_1: 8;

              hence thesis by A1, A2, A4, A7, A8, A12, AFF_1: 8;

            end;

            now

              assume that

               A14: q = c and q <> b;

              p = b implies thesis by A1, A2, A3, A9, A8, A14, AFF_1: 8;

              hence thesis by A1, A2, A4, A6, A8, A14, AFF_1: 8;

            end;

            hence thesis by A3, A4, A10, A11;

          end;

          hence thesis by A1, A3, A4;

        end;

        hence thesis by A1, A2, A6, A7, AFF_1: 8;

      end;

       A15:

      now

        assume that

         A16: not LIN (a,b,p) and not LIN (a,b,q);

        now

          consider p9 be Element of AS such that

           A17: (a,b) // (p,p9) and

           A18: p <> p9 by DIRAF: 40;

          assume

           A19: not (p,q) // (a,b);

          

           A20: not LIN (p,p9,q)

          proof

            assume LIN (p,p9,q);

            then (p,p9) // (p,q) by AFF_1:def 1;

            hence contradiction by A19, A17, A18, AFF_1: 5;

          end;

          (p,p9) // (a,b) by A17, AFF_1: 4;

          then ex p99 be Element of AS st LIN (p,p9,p99) & p <> p99 & p9 <> p99 by A1, A2, A3, A4, A16, Lm3;

          then

          consider r such that

           A21: LIN (q,p,r) and

           A22: q <> r & p <> r by A18, A20, Lm1;

           LIN (p,q,r) by A21, AFF_1: 6;

          hence thesis by A22;

        end;

        hence thesis by A1, A2, A3, A4, A16, Lm3;

      end;

      now

        assume ( not LIN (a,b,q)) & LIN (a,b,p);

        then

        consider x such that

         A23: LIN (q,p,x) and

         A24: q <> x & p <> x by A1, A2, A3, A4, Lm2;

         LIN (p,q,x) by A23, AFF_1: 6;

        hence thesis by A24;

      end;

      hence thesis by A1, A2, A3, A4, A5, A15, Lm2;

    end;

    reserve AFP for AffinPlane,

a,a9,b,b9,c,c9,d,p,p9,q,q9,r,x,x9,y,y9,z for Element of AFP,

A,C,P for Subset of AFP,

f,g,h,f1,f2 for Permutation of the carrier of AFP;

    theorem :: TRANSLAC:2

    

     Th2: AFP is Fanoian & (a,b) // (c,d) & (a,c) // (b,d) & not LIN (a,b,c) implies ex p st LIN (b,c,p) & LIN (a,d,p)

    proof

      assume (for a, b, c, d st (a,b) // (c,d) & (a,c) // (b,d) & (a,d) // (b,c) holds LIN (a,b,c)) & (a,b) // (c,d) & (a,c) // (b,d) & not LIN (a,b,c);

      then not (a,d) // (b,c);

      then ex p st LIN (a,d,p) & LIN (b,c,p) by AFF_1: 60;

      hence thesis;

    end;

    

     Lm4: not LIN (a,b,x) & (a,b) // (x,y) & x <> y implies not LIN (x,y,a) & not LIN (b,a,y) & not LIN (y,x,b)

    proof

      assume that

       A1: not LIN (a,b,x) and

       A2: (a,b) // (x,y) and

       A3: x <> y;

      thus not LIN (x,y,a)

      proof

        

         A4: LIN (x,y,x) by AFF_1: 7;

        assume

         A5: LIN (x,y,a);

        (x,y) // (a,b) by A2, AFF_1: 4;

        then LIN (x,y,b) by A3, A5, AFF_1: 9;

        hence contradiction by A1, A3, A5, A4, AFF_1: 8;

      end;

      thus not LIN (b,a,y)

      proof

        assume

         A6: LIN (b,a,y);

        (b,a) // (y,x) & b <> a by A1, A2, AFF_1: 4, AFF_1: 7;

        then LIN (b,a,x) by A6, AFF_1: 9;

        hence contradiction by A1, AFF_1: 6;

      end;

      thus not LIN (y,x,b)

      proof

        

         A7: LIN (y,x,x) by AFF_1: 7;

        assume

         A8: LIN (y,x,b);

        (y,x) // (b,a) by A2, AFF_1: 4;

        then LIN (y,x,a) by A3, A8, AFF_1: 9;

        hence contradiction by A1, A3, A8, A7, AFF_1: 8;

      end;

    end;

    

     Lm5: not LIN (a,b,x) & (a,b) // (x,y) & (a,x) // (b,y) implies not LIN (x,y,a) & not LIN (b,a,y) & not LIN (y,x,b)

    proof

      assume that

       A1: not LIN (a,b,x) and

       A2: (a,b) // (x,y) and

       A3: (a,x) // (b,y);

      x <> y

      proof

        assume x = y;

        then (x,a) // (x,b) by A3, AFF_1: 4;

        then LIN (x,a,b) by AFF_1:def 1;

        hence contradiction by A1, AFF_1: 6;

      end;

      hence thesis by A1, A2, Lm4;

    end;

    theorem :: TRANSLAC:3

    

     Th3: f is translation & not LIN (a,(f . a),x) & (a,(f . a)) // (x,y) & (a,x) // ((f . a),y) implies y = (f . x)

    proof

      assume

       A1: f is translation;

      then

       A2: f is dilatation by TRANSGEO:def 11;

      then

       A3: (a,x) // ((f . a),(f . x)) by TRANSGEO: 68;

      assume

       A4: ( not LIN (a,(f . a),x)) & (a,(f . a)) // (x,y) & (a,x) // ((f . a),y);

      (a,(f . a)) // (x,(f . x)) by A1, A2, TRANSGEO: 82;

      hence thesis by A4, A3, TRANSGEO: 80;

    end;

    theorem :: TRANSLAC:4

    

     Th4: AFP is translational iff for a, a9, b, c, b9, c9 st not LIN (a,a9,b) & not LIN (a,a9,c) & (a,a9) // (b,b9) & (a,a9) // (c,c9) & (a,b) // (a9,b9) & (a,c) // (a9,c9) holds (b,c) // (b9,c9)

    proof

      thus AFP is translational implies for a, a9, b, c, b9, c9 st not LIN (a,a9,b) & not LIN (a,a9,c) & (a,a9) // (b,b9) & (a,a9) // (c,c9) & (a,b) // (a9,b9) & (a,c) // (a9,c9) holds (b,c) // (b9,c9)

      proof

        assume

         A1: AFP is translational;

        let a, a9, b, c, b9, c9;

        assume that

         A2: not LIN (a,a9,b) and

         A3: not LIN (a,a9,c) and

         A4: (a,a9) // (b,b9) and

         A5: (a,a9) // (c,c9) and

         A6: (a,b) // (a9,b9) and

         A7: (a,c) // (a9,c9);

        set A = ( Line (a,a9)), P = ( Line (b,b9)), C = ( Line (c,c9));

        

         A8: a in A & a9 in A by AFF_1: 15;

        

         A9: c <> c9

        proof

          assume c = c9;

          then (c,a) // (c,a9) by A7, AFF_1: 4;

          then LIN (c,a,a9) by AFF_1:def 1;

          hence contradiction by A3, AFF_1: 6;

        end;

        then

         A10: C is being_line by AFF_1:def 3;

        

         A11: b <> b9

        proof

          assume b = b9;

          then (b,a) // (b,a9) by A6, AFF_1: 4;

          then LIN (b,a,a9) by AFF_1:def 1;

          hence contradiction by A2, AFF_1: 6;

        end;

        then

         A12: P is being_line by AFF_1:def 3;

        

         A13: a <> a9 by A2, AFF_1: 7;

        then

         A14: A is being_line by AFF_1:def 3;

        

         A15: c in C by AFF_1: 15;

        then

         A16: A <> C by A3, A8, A14, AFF_1: 21;

        

         A17: A // P by A4, A13, A11, AFF_1: 37;

        

         A18: b9 in P & c9 in C by AFF_1: 15;

        

         A19: A // C by A5, A13, A9, AFF_1: 37;

        

         A20: b in P by AFF_1: 15;

        then A <> P by A2, A8, A14, AFF_1: 21;

        hence thesis by A1, A6, A7, A8, A20, A15, A18, A14, A12, A10, A17, A19, A16, AFF_2:def 11;

      end;

      assume

       A21: for a, a9, b, c, b9, c9 st not LIN (a,a9,b) & not LIN (a,a9,c) & (a,a9) // (b,b9) & (a,a9) // (c,c9) & (a,b) // (a9,b9) & (a,c) // (a9,c9) holds (b,c) // (b9,c9);

      now

        let A, P, C, a, b, c, a9, b9, c9;

        assume that

         A22: A // P and

         A23: A // C and

         A24: a in A and

         A25: a9 in A and

         A26: b in P and

         A27: b9 in P and

         A28: c in C and

         A29: c9 in C and

         A30: A is being_line and

         A31: P is being_line and

         A32: C is being_line and

         A33: A <> P and

         A34: A <> C and

         A35: (a,b) // (a9,b9) and

         A36: (a,c) // (a9,c9);

        

         A37: (a,a9) // (b,b9) & (a,a9) // (c,c9) by A22, A23, A24, A25, A26, A27, A28, A29, AFF_1: 39;

         A38:

        now

          assume

           A39: a <> a9;

          

           A40: not LIN (a,a9,c)

          proof

            assume LIN (a,a9,c);

            then c in A by A24, A25, A30, A39, AFF_1: 25;

            hence contradiction by A23, A28, A34, AFF_1: 45;

          end;

           not LIN (a,a9,b)

          proof

            assume LIN (a,a9,b);

            then b in A by A24, A25, A30, A39, AFF_1: 25;

            hence contradiction by A22, A26, A33, AFF_1: 45;

          end;

          hence (b,c) // (b9,c9) by A21, A35, A36, A37, A40;

        end;

        now

          assume

           A41: a = a9;

          then LIN (a,c,c9) by A36, AFF_1:def 1;

          then LIN (c,c9,a) by AFF_1: 6;

          then

           A42: c = c9 or a in C by A28, A29, A32, AFF_1: 25;

           LIN (a,b,b9) by A35, A41, AFF_1:def 1;

          then LIN (b,b9,a) by AFF_1: 6;

          then b = b9 or a in P by A26, A27, A31, AFF_1: 25;

          hence (b,c) // (b9,c9) by A22, A23, A24, A33, A34, A42, AFF_1: 2, AFF_1: 45;

        end;

        hence (b,c) // (b9,c9) by A38;

      end;

      hence thesis by AFF_2:def 11;

    end;

    theorem :: TRANSLAC:5

    

     Th5: ex f st f is translation & (f . a) = a

    proof

      take ( id the carrier of AFP);

      thus thesis by TRANSGEO: 81;

    end;

    

     Lm6: a <> b implies ex y st ( not LIN (a,b,x) & (a,b) // (x,y) & (a,x) // (b,y) or ( LIN (a,b,x) & ex p, q st not LIN (a,b,p) & (a,b) // (p,q) & (a,p) // (b,q) & (p,q) // (x,y) & (p,x) // (q,y)))

    proof

      assume

       A1: a <> b;

       A2:

      now

        assume

         A3: LIN (a,b,x);

        consider p such that

         A4: not LIN (a,b,p) by A1, AFF_1: 13;

        consider q such that

         A5: (a,b) // (p,q) & (a,p) // (b,q) by DIRAF: 40;

        ex y st (p,q) // (x,y) & (p,x) // (q,y) by DIRAF: 40;

        hence thesis by A3, A4, A5;

      end;

      now

        

         A6: ex y st (a,b) // (x,y) & (a,x) // (b,y) by DIRAF: 40;

        assume not LIN (a,b,x);

        hence thesis by A6;

      end;

      hence thesis by A2;

    end;

    

     Lm7: a <> b implies ex x st not LIN (a,b,x) & (a,b) // (x,y) & (a,x) // (b,y) or LIN (a,b,x) & ex p, q st not LIN (a,b,p) & (a,b) // (p,q) & (a,p) // (b,q) & (p,q) // (x,y) & (p,x) // (q,y)

    proof

      assume

       A1: a <> b;

       A2:

      now

        assume

         A3: LIN (a,b,y);

        consider p such that

         A4: not LIN (a,b,p) by A1, AFF_1: 13;

        consider q such that

         A5: (a,b) // (p,q) and

         A6: (a,p) // (b,q) by DIRAF: 40;

         A7:

        now

          assume p = q;

          then (p,a) // (p,b) by A6, AFF_1: 4;

          then LIN (p,a,b) by AFF_1:def 1;

          hence contradiction by A4, AFF_1: 6;

        end;

        consider x such that

         A8: (q,p) // (y,x) and

         A9: (q,y) // (p,x) by DIRAF: 40;

        

         A10: (p,x) // (q,y) by A9, AFF_1: 4;

        

         A11: (p,q) // (x,y) by A8, AFF_1: 4;

        then (a,b) // (x,y) or p = q by A5, AFF_1: 5;

        then (a,b) // (y,x) by A7, AFF_1: 4;

        then LIN (a,b,x) by A1, A3, AFF_1: 9;

        hence thesis by A4, A5, A6, A11, A10;

      end;

      now

        consider x such that

         A12: (b,a) // (y,x) & (b,y) // (a,x) by DIRAF: 40;

        

         A13: (a,b) // (x,y) & (a,x) // (b,y) by A12, AFF_1: 4;

        assume not LIN (a,b,y);

        then not LIN (b,a,y) by AFF_1: 6;

        then not LIN (a,b,x) by A12, Lm5;

        hence thesis by A13;

      end;

      hence thesis by A2;

    end;

    

     Lm8: AFP is translational & a <> b & LIN (a,b,x) & (a,b) // (p,q) & (a,b) // (p9,q9) & (a,p) // (b,q) & (a,p9) // (b,q9) & (p,q) // (x,y) & (p9,q9) // (x,y9) & (p,x) // (q,y) & (p9,x) // (q9,y9) & not LIN (a,b,p) & not LIN (a,b,p9) & not LIN (p,q,p9) implies y = y9

    proof

      assume that

       A1: AFP is translational and

       A2: a <> b and

       A3: LIN (a,b,x) and

       A4: (a,b) // (p,q) and

       A5: (a,b) // (p9,q9) and

       A6: (a,p) // (b,q) and

       A7: (a,p9) // (b,q9) and

       A8: (p,q) // (x,y) and

       A9: (p9,q9) // (x,y9) and

       A10: (p,x) // (q,y) and

       A11: (p9,x) // (q9,y9) and

       A12: not LIN (a,b,p) and

       A13: not LIN (a,b,p9) and

       A14: not LIN (p,q,p9);

      

       A15: p <> q

      proof

        assume p = q;

        then (p,a) // (p,b) by A6, AFF_1: 4;

        then LIN (p,a,b) by AFF_1:def 1;

        hence contradiction by A12, AFF_1: 6;

      end;

      

       A16: not LIN (p,q,x)

      proof

        assume

         A17: LIN (p,q,x);

        then (p,q) // (p,x) by AFF_1:def 1;

        then

         A18: (p,x) // (a,b) by A4, A15, AFF_1: 5;

        (a,b) // (a,x) by A3, AFF_1:def 1;

        then (p,x) // (a,x) by A2, A18, AFF_1: 5;

        then (x,p) // (x,a) by AFF_1: 4;

        then

         A19: LIN (x,p,a) by AFF_1:def 1;

        

         A20: LIN (x,p,x) & LIN (a,x,b) by A3, AFF_1: 6, AFF_1: 7;

        

         A21: LIN (x,p,p) by AFF_1: 7;

        x <> a by A4, A6, A12, A17, Lm5;

        then LIN (x,p,b) by A19, A20, AFF_1: 11;

        hence contradiction by A3, A12, A19, A21, AFF_1: 8;

      end;

      

       A22: (p,q) // (p9,q9) by A2, A4, A5, AFF_1: 5;

      then

       A23: (p9,q9) // (x,y) by A8, A15, AFF_1: 5;

      

       A24: p9 <> q9

      proof

        assume p9 = q9;

        then (p9,a) // (p9,b) by A7, AFF_1: 4;

        then LIN (p9,a,b) by AFF_1:def 1;

        hence contradiction by A13, AFF_1: 6;

      end;

      

       A25: not LIN (p9,q9,x)

      proof

        assume

         A26: LIN (p9,q9,x);

        then (p9,q9) // (p9,x) by AFF_1:def 1;

        then

         A27: (p9,x) // (a,b) by A5, A24, AFF_1: 5;

        (a,b) // (a,x) by A3, AFF_1:def 1;

        then (p9,x) // (a,x) by A2, A27, AFF_1: 5;

        then (x,p9) // (x,a) by AFF_1: 4;

        then

         A28: LIN (x,p9,a) by AFF_1:def 1;

        

         A29: LIN (x,p9,x) & LIN (a,x,b) by A3, AFF_1: 6, AFF_1: 7;

        

         A30: LIN (x,p9,p9) by AFF_1: 7;

        x <> a by A5, A7, A13, A26, Lm5;

        then LIN (x,p9,b) by A28, A29, AFF_1: 11;

        hence contradiction by A3, A13, A28, A30, AFF_1: 8;

      end;

      (p,p9) // (q,q9) by A1, A4, A5, A6, A7, A12, A13, Th4;

      then (p9,x) // (q9,y) by A1, A8, A10, A14, A22, A16, Th4;

      hence thesis by A9, A11, A25, A23, TRANSGEO: 80;

    end;

    theorem :: TRANSLAC:6

    

     Th6: (for p, q, r st p <> q & LIN (p,q,r) holds r = p or r = q) & (a,b) // (p,q) & (a,p) // (b,q) & not LIN (a,b,p) implies (a,q) // (b,p)

    proof

      assume that

       A1: for p, q, r st p <> q & LIN (p,q,r) holds r = p or r = q and

       A2: (a,b) // (p,q) and

       A3: (a,p) // (b,q) and

       A4: not LIN (a,b,p);

      consider z such that

       A5: (q,p) // (a,z) and

       A6: (q,a) // (p,z) by DIRAF: 40;

      

       A7: p <> q

      proof

        assume p = q;

        then (p,a) // (p,b) by A3, AFF_1: 4;

        then LIN (p,a,b) by AFF_1:def 1;

        hence contradiction by A4, AFF_1: 6;

      end;

      

       A8: not LIN (a,p,q)

      proof

        

         A9: LIN (p,q,p) by AFF_1: 7;

        assume LIN (a,p,q);

        then

         A10: LIN (p,q,a) by AFF_1: 6;

        (p,q) // (a,b) by A2, AFF_1: 4;

        then LIN (p,q,b) by A7, A10, AFF_1: 9;

        hence contradiction by A4, A7, A10, A9, AFF_1: 8;

      end;

       A11:

      now

        assume a = z;

        then (a,p) // (a,q) by A6, AFF_1: 4;

        hence contradiction by A8, AFF_1:def 1;

      end;

      (p,q) // (a,z) by A5, AFF_1: 4;

      then (a,b) // (a,z) by A2, A7, AFF_1: 5;

      then

       A12: LIN (a,b,z) by AFF_1:def 1;

      a <> b by A4, AFF_1: 7;

      then a = z or b = z by A1, A12;

      hence thesis by A6, A11, AFF_1: 4;

    end;

    

     Lm9: AFP is translational & a <> b & LIN (a,b,x) & (a,b) // (p,q) & (a,b) // (p9,q9) & (a,p) // (b,q) & (a,p9) // (b,q9) & (p,q) // (x,y) & (p9,q9) // (x,y9) & (p,x) // (q,y) & (p9,x) // (q9,y9) & not LIN (a,b,p) & not LIN (a,b,p9) implies y = y9

    proof

      assume that

       A1: AFP is translational and

       A2: a <> b and

       A3: LIN (a,b,x) and

       A4: (a,b) // (p,q) and

       A5: (a,b) // (p9,q9) and

       A6: (a,p) // (b,q) and

       A7: (a,p9) // (b,q9) and

       A8: (p,q) // (x,y) and

       A9: (p9,q9) // (x,y9) and

       A10: (p,x) // (q,y) and

       A11: (p9,x) // (q9,y9) and

       A12: not LIN (a,b,p) and

       A13: not LIN (a,b,p9);

      

       A14: p <> q

      proof

        assume p = q;

        then (p,a) // (p,b) by A6, AFF_1: 4;

        then LIN (p,a,b) by AFF_1:def 1;

        hence contradiction by A12, AFF_1: 6;

      end;

      then (a,b) // (x,y) by A4, A8, AFF_1: 5;

      then

       A15: LIN (a,b,y) by A2, A3, AFF_1: 9;

      

       A16: not LIN (p,q,x)

      proof

        assume LIN (p,q,x);

        then (p,q) // (p,x) by AFF_1:def 1;

        then (a,b) // (p,x) by A4, A14, AFF_1: 5;

        then (a,b) // (x,p) by AFF_1: 4;

        hence contradiction by A2, A3, A12, AFF_1: 9;

      end;

       A17:

      now

        assume x = y;

        then (x,p) // (x,q) by A10, AFF_1: 4;

        then LIN (x,p,q) by AFF_1:def 1;

        hence contradiction by A16, AFF_1: 6;

      end;

      

       A18: p9 <> q9

      proof

        assume p9 = q9;

        then (p9,a) // (p9,b) by A7, AFF_1: 4;

        then LIN (p9,a,b) by AFF_1:def 1;

        hence contradiction by A13, AFF_1: 6;

      end;

      

       A19: not LIN (q,p,b)

      proof

        

         A20: LIN (q,p,p) by AFF_1: 7;

        assume

         A21: LIN (q,p,b);

        (q,p) // (b,a) by A4, AFF_1: 4;

        then LIN (q,p,a) by A14, A21, AFF_1: 9;

        hence contradiction by A12, A14, A21, A20, AFF_1: 8;

      end;

      now

        assume

         A22: LIN (p,q,p9);

        (p,q) // (p9,q9) by A2, A4, A5, AFF_1: 5;

        then

         A23: LIN (p,q,q9) by A14, A22, AFF_1: 9;

         A24:

        now

          assume

           A25: for x st LIN (a,p,x) holds x = a or x = p;

          then

           A26: for p, q, r st p <> q & LIN (p,q,r) holds r = p or r = q by Th1;

           A27:

          now

            assume

             A28: q = p9;

             A29:

            now

              (a,q) // (b,p) by A4, A6, A12, A26, Th6;

              then

               A30: (q,a) // (p,b) by AFF_1: 4;

              

               A31: (q,p) // (a,b) by A4, AFF_1: 4;

              assume

               A32: a = x;

              then

               A33: (q,a) // (p,y9) & not LIN (q,p,a) by A11, A14, A18, A16, A23, A25, A28, Th1, AFF_1: 6;

              b = y & (q,p) // (a,y9) by A2, A9, A14, A18, A17, A15, A23, A25, A28, A32, Th1;

              hence thesis by A31, A30, A33, TRANSGEO: 80;

            end;

            now

              

               A34: (q,p) // (b,a) & (q,b) // (p,a) by A4, A6, AFF_1: 4;

              assume

               A35: b = x;

              then

               A36: (q,b) // (p,y9) by A11, A14, A18, A23, A25, A28, Th1;

              a = y & (q,p) // (b,y9) by A2, A9, A14, A18, A17, A15, A23, A25, A28, A35, Th1;

              hence thesis by A19, A34, A36, TRANSGEO: 80;

            end;

            hence thesis by A2, A3, A25, A29, Th1;

          end;

          now

            assume

             A37: p = p9;

            then q = q9 by A14, A18, A23, A25, Th1;

            hence thesis by A8, A9, A10, A11, A16, A37, TRANSGEO: 80;

          end;

          hence thesis by A14, A22, A25, A27, Th1;

        end;

        now

          given p99 be Element of AFP such that

           A38: LIN (a,p,p99) and

           A39: p99 <> a and

           A40: p99 <> p;

          

           A41: not LIN (p,q,p99)

          proof

            assume LIN (p,q,p99);

            then

             A42: LIN (p,p99,q) by AFF_1: 6;

             LIN (p,p99,p) & LIN (p,p99,a) by A38, AFF_1: 6, AFF_1: 7;

            then LIN (p,q,a) by A40, A42, AFF_1: 8;

            hence contradiction by A4, A6, A12, Lm5;

          end;

          

           A43: not LIN (p9,q9,p99)

          proof

            (p,q) // (p9,q9) by A2, A4, A5, AFF_1: 5;

            then

             A44: LIN (p,q,q9) by A14, A22, AFF_1: 9;

            assume LIN (p9,q9,p99);

            hence contradiction by A18, A22, A41, A44, AFF_1: 11;

          end;

          consider q99 be Element of AFP such that

           A45: (a,b) // (p99,q99) & (a,p99) // (b,q99) by DIRAF: 40;

          consider y99 be Element of AFP such that

           A46: (p99,q99) // (x,y99) & (p99,x) // (q99,y99) by DIRAF: 40;

          

           A47: not LIN (a,b,p99)

          proof

            assume LIN (a,b,p99);

            then

             A48: LIN (a,p99,b) by AFF_1: 6;

             LIN (a,p99,a) & LIN (a,p99,p) by A38, AFF_1: 6, AFF_1: 7;

            hence contradiction by A12, A39, A48, AFF_1: 8;

          end;

          then y = y99 by A1, A2, A3, A4, A6, A8, A10, A12, A45, A46, A41, Lm8;

          hence thesis by A1, A2, A3, A5, A7, A9, A11, A13, A45, A46, A43, A47, Lm8;

        end;

        hence thesis by A24;

      end;

      hence thesis by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, Lm8;

    end;

    

     Lm10: a <> b & LIN (a,b,x) & (a,b) // (p,q) & (a,p) // (b,q) & (p,q) // (x,y) & not LIN (a,b,p) implies p <> q & LIN (a,b,y)

    proof

      assume that

       A1: a <> b & LIN (a,b,x) and

       A2: (a,b) // (p,q) and

       A3: (a,p) // (b,q) and

       A4: (p,q) // (x,y) and

       A5: not LIN (a,b,p);

      thus p <> q

      proof

        assume p = q;

        then (p,a) // (p,b) by A3, AFF_1: 4;

        then LIN (p,a,b) by AFF_1:def 1;

        hence contradiction by A5, AFF_1: 6;

      end;

      then (a,b) // (x,y) by A2, A4, AFF_1: 5;

      hence thesis by A1, AFF_1: 9;

    end;

    

     Lm11: AFP is translational & a <> b & LIN (a,b,x) & (a,b) // (p,q) & (a,b) // (p9,q9) & (a,p) // (b,q) & (a,p9) // (b,q9) & (p,q) // (x,y) & (p,x) // (q,y) & (p9,q9) // (x9,y) & (p9,x9) // (q9,y) & not LIN (a,b,p) & not LIN (a,b,p9) implies x = x9

    proof

      assume that

       A1: AFP is translational and

       A2: a <> b and

       A3: LIN (a,b,x) and

       A4: (a,b) // (p,q) and

       A5: (a,b) // (p9,q9) and

       A6: (a,p) // (b,q) and

       A7: (a,p9) // (b,q9) and

       A8: (p,q) // (x,y) and

       A9: (p,x) // (q,y) and

       A10: (p9,q9) // (x9,y) & (p9,x9) // (q9,y) and

       A11: not LIN (a,b,p) and

       A12: not LIN (a,b,p9);

      

       A13: (b,a) // (q,p) & (b,a) // (q9,p9) by A4, A5, AFF_1: 4;

      

       A14: (b,q) // (a,p) & (b,q9) // (a,p9) by A6, A7, AFF_1: 4;

      

       A15: (q9,p9) // (y,x9) & (q9,y) // (p9,x9) by A10, AFF_1: 4;

       LIN (a,b,y) by A2, A3, A4, A6, A8, A11, Lm10;

      then

       A16: LIN (b,a,y) by AFF_1: 6;

      

       A17: (q,p) // (y,x) & (q,y) // (p,x) by A8, A9, AFF_1: 4;

      ( not LIN (b,a,q)) & not LIN (b,a,q9) by A4, A5, A6, A7, A11, A12, Lm5;

      hence thesis by A1, A2, A16, A13, A14, A17, A15, Lm9;

    end;

    

     Lm12: AFP is translational & a <> b implies ex f st f is translation & (f . a) = b

    proof

      defpred X[ Element of AFP, Element of AFP] means ( not LIN (a,b,$1) & (a,b) // ($1,$2) & (a,$1) // (b,$2)) or ( LIN (a,b,$1) & (ex p, q st not LIN (a,b,p) & (a,b) // (p,q) & (a,p) // (b,q) & (p,q) // ($1,$2) & (p,$1) // (q,$2)));

      assume that

       A1: AFP is translational and

       A2: a <> b;

      

       A3: ex y st X[x, y] by A2, Lm6;

      

       A4: for x, y, x9 holds X[x, y] & X[x9, y] implies x = x9

      proof

        let x, y, x9;

        assume that

         A5: not LIN (a,b,x) & (a,b) // (x,y) & (a,x) // (b,y) or ( LIN (a,b,x) & ex p, q st not LIN (a,b,p) & (a,b) // (p,q) & (a,p) // (b,q) & (p,q) // (x,y) & (p,x) // (q,y)) and

         A6: not LIN (a,b,x9) & (a,b) // (x9,y) & (a,x9) // (b,y) or ( LIN (a,b,x9) & ex p, q st not LIN (a,b,p) & (a,b) // (p,q) & (a,p) // (b,q) & (p,q) // (x9,y) & (p,x9) // (q,y));

         A7:

        now

          assume

           A8: LIN (a,b,y);

          

           A9: not ( not LIN (a,b,x9) & (a,b) // (x9,y) & (a,x9) // (b,y))

          proof

            assume that

             A10: not LIN (a,b,x9) and

             A11: (a,b) // (x9,y) and (a,x9) // (b,y);

            (a,b) // (y,x9) by A11, AFF_1: 4;

            hence contradiction by A2, A8, A10, AFF_1: 9;

          end;

           not ( not LIN (a,b,x) & (a,b) // (x,y) & (a,x) // (b,y))

          proof

            assume that

             A12: not LIN (a,b,x) and

             A13: (a,b) // (x,y) and (a,x) // (b,y);

            (a,b) // (y,x) by A13, AFF_1: 4;

            hence contradiction by A2, A8, A12, AFF_1: 9;

          end;

          hence thesis by A1, A2, A5, A6, A9, Lm11;

        end;

        now

          assume

           A14: not LIN (a,b,y);

          then

           A15: (b,y) // (a,x9) by A2, A6, Lm10, AFF_1: 4;

          

           A16: (b,y) // (a,x) & (b,a) // (y,x9) by A2, A5, A6, A14, Lm10, AFF_1: 4;

          ( not LIN (b,a,y)) & (b,a) // (y,x) by A2, A5, A14, Lm5, Lm10, AFF_1: 4;

          hence thesis by A16, A15, TRANSGEO: 80;

        end;

        hence thesis by A7;

      end;

      

       A17: ex x st X[x, y] by A2, Lm7;

      

       A18: X[x, y] & X[x, y9] implies y = y9 by A1, A2, Lm9, TRANSGEO: 80;

      ex f st for x, y holds (f . x) = y iff X[x, y] from TRANSGEO:sch 1( A3, A17, A4, A18);

      then

      consider f such that

       A19: for x, y holds (f . x) = y iff not LIN (a,b,x) & (a,b) // (x,y) & (a,x) // (b,y) or LIN (a,b,x) & ex p, q st not LIN (a,b,p) & (a,b) // (p,q) & (a,p) // (b,q) & (p,q) // (x,y) & (p,x) // (q,y);

      

       A20: (a,b) // (x,(f . x))

      proof

        set y = (f . x);

        now

          assume

           A21: LIN (a,b,x);

          then

          consider p, q such that

           A22: not LIN (a,b,p) and

           A23: (a,b) // (p,q) and

           A24: (a,p) // (b,q) and

           A25: (p,q) // (x,y) and (p,x) // (q,y) by A19;

          p <> q by A2, A21, A22, A23, A24, A25, Lm10;

          hence thesis by A23, A25, AFF_1: 5;

        end;

        hence thesis by A19;

      end;

      for x, y holds (x,y) // ((f . x),(f . y))

      proof

        let x, y;

         A26:

        now

          

           A27: ex x9 st (y,(f . y)) // (x,x9) & (y,x) // ((f . y),x9) by DIRAF: 40;

          assume that

           A28: LIN (a,b,x) and

           A29: not LIN (a,b,y);

          (a,b) // (y,(f . y)) & (a,y) // (b,(f . y)) by A19, A29;

          then (y,x) // ((f . y),(f . x)) by A19, A28, A29, A27;

          hence thesis by AFF_1: 4;

        end;

         A30:

        now

          

           A31: ex y9 st (x,(f . x)) // (y,y9) & (x,y) // ((f . x),y9) by DIRAF: 40;

          assume that

           A32: not LIN (a,b,x) and

           A33: LIN (a,b,y);

          (a,b) // (x,(f . x)) & (a,x) // (b,(f . x)) by A19, A32;

          hence thesis by A19, A32, A33, A31;

        end;

         A34:

        now

          assume

           A35: LIN (a,b,x) & LIN (a,b,y);

          then LIN (a,b,(f . x)) & LIN (a,b,(f . y)) by A2, A20, AFF_1: 9;

          then

           A36: (a,b) // ((f . x),(f . y)) by AFF_1: 10;

          (a,b) // (x,y) by A35, AFF_1: 10;

          hence thesis by A2, A36, AFF_1: 5;

        end;

        now

          assume

           A37: ( not LIN (a,b,x)) & not LIN (a,b,y);

          then

           A38: (a,b) // (x,(f . x)) & (a,b) // (y,(f . y)) by A19;

          (a,x) // (b,(f . x)) & (a,y) // (b,(f . y)) by A19, A37;

          hence thesis by A1, A37, A38, Th4;

        end;

        hence thesis by A34, A26, A30;

      end;

      then

       A39: f is dilatation by TRANSGEO: 68;

      

       A40: (f . a) = b

      proof

        

         A41: LIN (a,b,a) by AFF_1: 7;

        consider p such that

         A42: not LIN (a,b,p) by A2, AFF_1: 13;

        consider q such that

         A43: (a,b) // (p,q) & (a,p) // (b,q) by DIRAF: 40;

        (p,a) // (q,b) & (p,q) // (a,b) by A43, AFF_1: 4;

        hence thesis by A19, A42, A43, A41;

      end;

      (x,(f . x)) // (y,(f . y))

      proof

        (a,b) // (x,(f . x)) & (a,b) // (y,(f . y)) by A20;

        hence thesis by A2, AFF_1: 5;

      end;

      then f is translation by A39, TRANSGEO: 82;

      hence thesis by A40;

    end;

    theorem :: TRANSLAC:7

    

     Th7: AFP is translational implies ex f st f is translation & (f . a) = b

    proof

      assume

       A1: AFP is translational;

      a = b implies thesis by Th5;

      hence thesis by A1, Lm12;

    end;

    theorem :: TRANSLAC:8

    (for a, b holds ex f st f is translation & (f . a) = b) implies AFP is translational

    proof

      assume

       A1: for a, b holds ex f st f is translation & (f . a) = b;

      now

        let a, a9, b, c, b9, c9;

        consider f such that

         A2: f is translation and

         A3: (f . a) = a9 by A1;

        

         A4: f is dilatation by A2, TRANSGEO:def 11;

        assume ( not LIN (a,a9,b)) & not LIN (a,a9,c) & (a,a9) // (b,b9) & (a,a9) // (c,c9) & (a,b) // (a9,b9) & (a,c) // (a9,c9);

        then b9 = (f . b) & c9 = (f . c) by A2, A3, Th3;

        hence (b,c) // (b9,c9) by A4, TRANSGEO: 68;

      end;

      hence thesis by Th4;

    end;

    theorem :: TRANSLAC:9

    

     Th9: f is translation & g is translation & not LIN (a,(f . a),(g . a)) implies (f * g) = (g * f)

    proof

      assume that

       A1: f is translation and

       A2: g is translation;

      

       A3: g is dilatation by A2, TRANSGEO:def 11;

      then

       A4: (a,(f . a)) // ((g . a),(g . (f . a))) by TRANSGEO: 68;

      assume

       A5: not LIN (a,(f . a),(g . a));

      (a,(g . a)) // ((f . a),(g . (f . a))) by A2, A3, TRANSGEO: 82;

      then (f . (g . a)) = (g . (f . a)) by A1, A5, A4, Th3;

      then ((f * g) . a) = (g . (f . a)) by FUNCT_2: 15;

      then

       A6: ((f * g) . a) = ((g * f) . a) by FUNCT_2: 15;

      (f * g) is translation & (g * f) is translation by A1, A2, TRANSGEO: 86;

      hence thesis by A6, TRANSGEO: 84;

    end;

    theorem :: TRANSLAC:10

    

     Th10: AFP is translational & f is translation & g is translation implies (f * g) = (g * f)

    proof

      assume that

       A1: AFP is translational and

       A2: f is translation and

       A3: g is translation;

      

       A4: g is dilatation by A3, TRANSGEO:def 11;

      now

        set a = the Element of AFP;

        assume that

         A5: f <> ( id the carrier of AFP) and

         A6: g <> ( id the carrier of AFP);

        

         A7: a <> (f . a) by A2, A5, TRANSGEO:def 11;

        

         A8: a <> (g . a) by A3, A6, TRANSGEO:def 11;

        now

          consider b such that

           A9: not LIN (a,(f . a),b) by A7, AFF_1: 13;

          consider h such that

           A10: h is translation and

           A11: (h . a) = b by A1, Th7;

          

           A12: (h * g) is translation by A3, A10, TRANSGEO: 86;

          assume

           A13: LIN (a,(f . a),(g . a));

           not LIN (a,(f . a),(h . (g . a)))

          proof

            

             A14: not LIN (a,(g . a),b)

            proof

              assume

               A15: LIN (a,(g . a),b);

               LIN (a,(g . a),(f . a)) & LIN (a,(g . a),a) by A13, AFF_1: 6, AFF_1: 7;

              hence contradiction by A8, A9, A15, AFF_1: 8;

            end;

            then ((g * h) . a) = ((h * g) . a) by A3, A10, A11, Th9;

            then ((g * h) . a) = (h . (g . a)) by FUNCT_2: 15;

            then

             A16: (g . b) = (h . (g . a)) by A11, FUNCT_2: 15;

            assume

             A17: LIN (a,(f . a),(h . (g . a)));

            (a,(g . a)) // (b,(g . b)) & (a,b) // ((g . a),(g . b)) by A3, A4, TRANSGEO: 68, TRANSGEO: 82;

            then LIN (a,(f . a),a) & not LIN ((g . a),a,(h . (g . a))) by A14, A16, Lm5, AFF_1: 7;

            hence contradiction by A7, A13, A17, AFF_1: 8;

          end;

          then

           A18: not LIN (a,(f . a),((h * g) . a)) by FUNCT_2: 15;

          (h * (f * g)) = ((h * f) * g) by RELAT_1: 36

          .= ((f * h) * g) by A2, A9, A10, A11, Th9

          .= (f * (h * g)) by RELAT_1: 36

          .= ((h * g) * f) by A2, A12, A18, Th9

          .= (h * (g * f)) by RELAT_1: 36;

          hence thesis by TRANSGEO: 5;

        end;

        hence thesis by A2, A3, Th9;

      end;

      hence thesis by TRANSGEO: 4;

    end;

    theorem :: TRANSLAC:11

    

     Th11: f is translation & g is translation & (p,(f . p)) // (p,(g . p)) implies (p,(f . p)) // (p,((f * g) . p))

    proof

      assume that

       A1: f is translation and

       A2: g is translation and

       A3: (p,(f . p)) // (p,(g . p));

      

       A4: f is dilatation by A1, TRANSGEO:def 11;

       A5:

      now

        assume g <> ( id the carrier of AFP);

        then

         A6: (g . p) <> p by A2, TRANSGEO:def 11;

        (p,(g . p)) // ((f . p),(f . (g . p))) by A4, TRANSGEO: 68;

        then (p,(f . p)) // ((f . p),(f . (g . p))) by A3, A6, AFF_1: 5;

        then ((f . p),p) // ((f . p),(f . (g . p))) by AFF_1: 4;

        then LIN ((f . p),p,(f . (g . p))) by AFF_1:def 1;

        then LIN (p,(f . p),(f . (g . p))) by AFF_1: 6;

        then (p,(f . p)) // (p,(f . (g . p))) by AFF_1:def 1;

        hence thesis by FUNCT_2: 15;

      end;

      now

        assume g = ( id the carrier of AFP);

        then (f * g) = f by FUNCT_2: 17;

        hence thesis by AFF_1: 2;

      end;

      hence thesis by A5;

    end;

    theorem :: TRANSLAC:12

    AFP is Fanoian & AFP is translational & f is translation implies ex g st g is translation & (g * g) = f

    proof

      assume that

       A1: AFP is Fanoian and

       A2: AFP is translational and

       A3: f is translation;

       A4:

      now

        set a = the Element of AFP;

        set b = (f . a);

        assume f <> ( id the carrier of AFP);

        then a <> b by A3, TRANSGEO:def 11;

        then

        consider c such that

         A5: not LIN (a,b,c) by AFF_1: 13;

        consider d such that

         A6: (c,b) // (a,d) and

         A7: (c,a) // (b,d) by DIRAF: 40;

         not LIN (c,b,a) by A5, AFF_1: 6;

        then

        consider p such that

         A8: LIN (b,a,p) and

         A9: LIN (c,d,p) by A1, A6, A7, Th2;

        consider f1 be Permutation of the carrier of AFP such that

         A10: f1 is translation and

         A11: (f1 . p) = a by A2, Th7;

        consider f2 be Permutation of the carrier of AFP such that

         A12: f2 is translation and

         A13: (f2 . p) = b by A2, Th7;

        

         A14: (f1 * f2) is translation by A10, A12, TRANSGEO: 86;

        

         A15: LIN (p,c,d) by A9, AFF_1: 6;

        then

         A16: (p,c) // (p,d) by AFF_1:def 1;

         A17:

        now

          assume (p,c) // (p,a);

          then LIN (p,c,a) by AFF_1:def 1;

          then

           A18: LIN (p,a,c) by AFF_1: 6;

           LIN (p,a,a) & LIN (p,a,b) by A8, AFF_1: 6, AFF_1: 7;

          then p = a by A5, A18, AFF_1: 8;

          then (a,c) // (c,b) or a = d by A6, A16, AFF_1: 5;

          then (c,a) // (c,b) or a = d by AFF_1: 4;

          then LIN (c,a,b) or a = d by AFF_1:def 1;

          then (a,c) // (a,b) by A5, A7, AFF_1: 4, AFF_1: 6;

          then LIN (a,c,b) by AFF_1:def 1;

          hence contradiction by A5, AFF_1: 6;

        end;

        consider f3 be Permutation of the carrier of AFP such that

         A19: f3 is translation and

         A20: (f3 . p) = c by A2, Th7;

        (f3 " ) is translation by A19, TRANSGEO: 85;

        then

         A21: (f1 * (f3 " )) is translation by A10, TRANSGEO: 86;

         LIN (p,a,b) by A8, AFF_1: 6;

        then (p,(f1 . p)) // (p,(f2 . p)) by A11, A13, AFF_1:def 1;

        then

         A22: (p,a) // (p,((f1 * f2) . p)) by A10, A11, A12, Th11;

        consider f4 be Permutation of the carrier of AFP such that

         A23: f4 is translation and

         A24: (f4 . p) = d by A2, Th7;

        (f4 . ((f2 " ) . b)) = (f4 . p) by A13, TRANSGEO: 2;

        then

         A25: ((f4 * (f2 " )) . b) = d by A24, FUNCT_2: 15;

        consider h such that

         A26: h is translation and

         A27: (h . c) = a by A2, Th7;

         not LIN (c,a,b) by A5, AFF_1: 6;

        then

         A28: (h . b) = d by A6, A7, A26, A27, Th3;

        (f1 . ((f3 " ) . c)) = (f1 . p) by A20, TRANSGEO: 2;

        then ((f1 * (f3 " )) . c) = a by A11, FUNCT_2: 15;

        then

         A29: (f1 * (f3 " )) = h by A26, A27, A21, TRANSGEO: 84;

        

         A30: (f2 " ) is translation by A12, TRANSGEO: 85;

        then (f4 * (f2 " )) is translation by A23, TRANSGEO: 86;

        then (f1 * (f3 " )) = (f4 * (f2 " )) by A26, A28, A29, A25, TRANSGEO: 84;

        then (f1 * ((f3 " ) * f3)) = ((f4 * (f2 " )) * f3) by RELAT_1: 36;

        then (f1 * ( id the carrier of AFP)) = ((f4 * (f2 " )) * f3) by FUNCT_2: 61;

        

        then f1 = ((f4 * (f2 " )) * f3) by FUNCT_2: 17

        .= (f4 * ((f2 " ) * f3)) by RELAT_1: 36

        .= (f4 * (f3 * (f2 " ))) by A2, A19, A30, Th10

        .= ((f4 * f3) * (f2 " )) by RELAT_1: 36;

        

        then

         A31: (f1 * f2) = ((f4 * f3) * ((f2 " ) * f2)) by RELAT_1: 36

        .= ((f4 * f3) * ( id the carrier of AFP)) by FUNCT_2: 61

        .= (f4 * f3) by FUNCT_2: 17;

        (p,(f3 . p)) // (p,(f4 . p)) by A20, A24, A15, AFF_1:def 1;

        then (p,c) // (p,((f3 * f4) . p)) by A19, A20, A23, Th11;

        then (p,c) // (p,((f1 * f2) . p)) by A2, A19, A23, A31, Th10;

        then p = ((f1 * f2) . p) by A22, A17, AFF_1: 5;

        then ((f1 " ) * (f1 * f2)) = ((f1 " ) * ( id the carrier of AFP)) by A14, TRANSGEO:def 11;

        then (((f1 " ) * f1) * f2) = ((f1 " ) * ( id the carrier of AFP)) by RELAT_1: 36;

        then (( id the carrier of AFP) * f2) = ((f1 " ) * ( id the carrier of AFP)) by FUNCT_2: 61;

        then f2 = ((f1 " ) * ( id the carrier of AFP)) by FUNCT_2: 17;

        

        then

         A32: ((f2 * f2) . a) = ((f2 * (f1 " )) . a) by FUNCT_2: 17

        .= (f2 . ((f1 " ) . a)) by FUNCT_2: 15

        .= b by A11, A13, TRANSGEO: 2;

        (f2 * f2) is translation by A12, TRANSGEO: 86;

        hence thesis by A3, A12, A32, TRANSGEO: 84;

      end;

      now

        set g = ( id the carrier of AFP);

        

         A33: g is translation & (g * g) = ( id the carrier of AFP) by FUNCT_2: 17, TRANSGEO: 81;

        assume f = ( id the carrier of AFP);

        hence thesis by A33;

      end;

      hence thesis by A4;

    end;

    theorem :: TRANSLAC:13

    

     Th13: AFP is Fanoian & f is translation & (f * f) = ( id the carrier of AFP) implies f = ( id the carrier of AFP)

    proof

      set a = the Element of AFP;

      assume that

       A1: AFP is Fanoian and

       A2: f is translation and

       A3: (f * f) = ( id the carrier of AFP);

      assume f <> ( id the carrier of AFP);

      then a <> (f . a) by A2, TRANSGEO:def 11;

      then

      consider b such that

       A4: not LIN (a,(f . a),b) by AFF_1: 13;

      

       A5: f is dilatation by A2, TRANSGEO:def 11;

      then

       A6: (a,b) // ((f . a),(f . b)) by TRANSGEO: 68;

      ((f . b),a) // ((f . (f . b)),(f . a)) by A5, TRANSGEO: 68;

      then ((f . b),a) // (((f * f) . b),(f . a)) by FUNCT_2: 15;

      then ((f . b),a) // (b,(f . a)) by A3;

      then

       A7: (a,(f . b)) // ((f . a),b) by AFF_1: 4;

      (a,(f . a)) // (b,(f . b)) by A2, A5, TRANSGEO: 82;

      hence contradiction by A1, A4, A6, A7;

    end;

    theorem :: TRANSLAC:14

    AFP is translational & AFP is Fanoian & f1 is translation & f2 is translation & g = (f1 * f1) & g = (f2 * f2) implies f1 = f2

    proof

      assume that

       A1: AFP is translational and

       A2: AFP is Fanoian and

       A3: f1 is translation and

       A4: f2 is translation and

       A5: g = (f1 * f1) & g = (f2 * f2);

      set h = ((f2 " ) * f1);

      

       A6: (f2 " ) is translation by A4, TRANSGEO: 85;

      (h * h) = ((f2 " ) * (f1 * ((f2 " ) * f1))) by RELAT_1: 36

      .= ((f2 " ) * ((f1 * (f2 " )) * f1)) by RELAT_1: 36

      .= ((f2 " ) * (((f2 " ) * f1) * f1)) by A1, A3, A6, Th10

      .= ((f2 " ) * ((f2 " ) * (f1 * f1))) by RELAT_1: 36

      .= (((f2 " ) * (f2 " )) * (f1 * f1)) by RELAT_1: 36

      .= ((g " ) * g) by A5, FUNCT_1: 44

      .= ( id the carrier of AFP) by FUNCT_2: 61;

      then ((f2 " ) * f1) = ( id the carrier of AFP) by A2, A3, A6, Th13, TRANSGEO: 86;

      then ((f2 " ) * f1) = ((f2 " ) * f2) by FUNCT_2: 61;

      hence thesis by TRANSGEO: 5;

    end;