afvect01.miz

    begin

    reserve AFV for WeakAffVect;

    reserve a,a9,b,b9,c,d,p,p9,q,q9,r,r9 for Element of AFV;

    registration

      let A be non empty set, C be Relation of [:A, A:];

      cluster AffinStruct (# A, C #) -> non empty;

      coherence ;

    end



     Lm1: (a,b) '||' (b,c) & a <> c implies (a,b) // (b,c)

    proof

      assume that

       A1: (a,b) '||' (b,c) and

       A2: a <> c;

       not (a,b) // (c,b) by A2, AFVECT0: 4, AFVECT0: 7;

      hence thesis by A1, DIRAF:def 4;

    end;



     Lm2: (a,b) // (b,a) iff ex p, q st (a,b) '||' (p,q) & (a,p) '||' (p,b) & (a,q) '||' (q,b)

    proof

       A1:

      now

        given p, q such that

         A2: (a,b) '||' (p,q) and

         A3: (a,p) '||' (p,b) and

         A4: (a,q) '||' (q,b);

        now

           A5:

          now

            assume

             A6: MDist (p,q);

            (a,b) // (p,q) or (a,b) // (q,p) by A2, DIRAF:def 4;

            then MDist (a,b) by A6, AFVECT0: 3, AFVECT0: 15;

            hence (a,b) // (b,a) by AFVECT0:def 2;

          end;

          assume

           A7: a <> b;

          then (a,q) // (q,b) by A4, Lm1;

          then

           A8: Mid (a,q,b) by AFVECT0:def 3;

           A9:

          now

            assume p = q;

            then (a,b) // (p,p) by A2, DIRAF:def 4;

            hence contradiction by A7, AFVECT0:def 1;

          end;

          (a,p) // (p,b) by A3, A7, Lm1;

          then Mid (a,p,b) by AFVECT0:def 3;

          hence (a,b) // (b,a) by A8, A9, A5, AFVECT0: 20;

        end;

        hence (a,b) // (b,a) by AFVECT0: 2;

      end;

      now

        assume

         A10: (a,b) // (b,a);

         A11:

        now

          assume a <> b;

          then

           A12: MDist (a,b) by A10, AFVECT0:def 2;

          consider p such that

           A13: Mid (a,p,b) by AFVECT0: 19;



           A14: (a,p) // (p,b) by A13, AFVECT0:def 3;

          consider q such that

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

          take p, q;

           Mid (a,q,b) by A13, A15, A12, AFVECT0: 15, AFVECT0: 23;

          then (a,q) // (q,b) by AFVECT0:def 3;

          hence (a,b) '||' (p,q) & (a,p) '||' (p,b) & (a,q) '||' (q,b) by A15, A14, DIRAF:def 4;

        end;

        now

          assume

           A16: a = b;

          take p = a, q = a;

          (a,b) // (p,q) by A16, AFVECT0: 2;

          hence (a,b) '||' (p,q) & (a,p) '||' (p,b) & (a,q) '||' (q,b) by A16, DIRAF:def 4;

        end;

        hence ex p, q st (a,b) '||' (p,q) & (a,p) '||' (p,b) & (a,q) '||' (q,b) by A11;

      end;

      hence thesis by A1;

    end;



     Lm3: (a,b) '||' (c,d) implies (b,a) '||' (c,d)

    proof

      assume (a,b) '||' (c,d);

      then (a,b) // (c,d) or (a,b) // (d,c) by DIRAF:def 4;

      then (b,a) // (d,c) or (b,a) // (c,d) by AFVECT0: 7;

      hence thesis by DIRAF:def 4;

    end;



     Lm4: (a,b) '||' (b,a)

    proof

      (a,b) // (a,b) by AFVECT0: 1;

      hence thesis by DIRAF:def 4;

    end;



     Lm5: (a,b) '||' (p,p) implies a = b

    proof

      assume (a,b) '||' (p,p);

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

      hence thesis by AFVECT0:def 1;

    end;



     Lm6: for a, b, c, d, p, q holds (a,b) '||' (p,q) & (c,d) '||' (p,q) implies (a,b) '||' (c,d)

    proof

      let a, b, c, d, p, q;

      assume (a,b) '||' (p,q) & (c,d) '||' (p,q);

      then (a,b) // (p,q) & (c,d) // (p,q) or (a,b) // (p,q) & (c,d) // (q,p) or (a,b) // (q,p) & (c,d) // (p,q) or (a,b) // (q,p) & (c,d) // (q,p) by DIRAF:def 4;

      then (a,b) // (c,d) or (a,b) // (p,q) & (d,c) // (p,q) or (a,b) // (q,p) & (d,c) // (q,p) by AFVECT0: 7, AFVECT0:def 1;

      then (a,b) // (c,d) or (a,b) // (d,c) by AFVECT0:def 1;

      hence thesis by DIRAF:def 4;

    end;



     Lm7: ex b st (a,b) '||' (b,c)

    proof

      consider b such that

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

      take b;

      thus thesis by A1, DIRAF:def 4;

    end;



     Lm8: for a, a9, b, b9, p st a <> a9 & b <> b9 & (p,a) '||' (p,a9) & (p,b) '||' (p,b9) holds (a,b) '||' (a9,b9)

    proof

      let a, a9, b, b9, p;

      assume that

       A1: a <> a9 and

       A2: b <> b9 and

       A3: (p,a) '||' (p,a9) and

       A4: (p,b) '||' (p,b9);

      (b,p) // (p,b9) by A2, A4, Lm1, Lm3;

      then

       A5: Mid (b,p,b9) by AFVECT0:def 3;

      (a,p) // (p,a9) by A1, A3, Lm1, Lm3;

      then Mid (a,p,a9) by AFVECT0:def 3;

      then (a,b) // (b9,a9) by A5, AFVECT0: 25;

      hence thesis by DIRAF:def 4;

    end;



     Lm9: a = b or ex c st a <> c & (a,b) '||' (b,c) or ex p, p9 st p <> p9 & (a,b) '||' (p,p9) & (a,p) '||' (p,b) & (a,p9) '||' (p9,b)

    proof

      consider c such that

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

       A2:

      now

        assume a = c;

        then

        consider p, p9 such that

         A3: (a,b) '||' (p,p9) and

         A4: (a,p) '||' (p,b) & (a,p9) '||' (p9,b) by A1, Lm2;

        p = p9 implies a = b by A3, Lm5;

        hence a = b or ex p, p9 st p <> p9 & (a,b) '||' (p,p9) & (a,p) '||' (p,b) & (a,p9) '||' (p9,b) by A3, A4;

      end;

      now

        assume

         A5: a <> c;

        (a,b) '||' (b,c) by A1, DIRAF:def 4;

        hence ex c st a <> c & (a,b) '||' (b,c) by A5;

      end;

      hence thesis by A2;

    end;



     Lm10: for a, b, b9, p, p9, c st (a,b) '||' (b,c) & (b,b9) '||' (p,p9) & (b,p) '||' (p,b9) & (b,p9) '||' (p9,b9) holds (a,b9) '||' (b9,c)

    proof

      let a, b, b9, p, p9, c;

      assume that

       A1: (a,b) '||' (b,c) and

       A2: (b,b9) '||' (p,p9) & (b,p) '||' (p,b9) & (b,p9) '||' (p9,b9);



       A3: (b,b9) // (b9,b) by A2, Lm2;

       A4:

      now

        assume

         A5: (a,b) // (b,c);

        then

         A6: Mid (a,b,c) by AFVECT0:def 3;

         A7:

        now

          assume MDist (b,b9);

          then Mid (a,b9,c) by A6, AFVECT0: 23;

          then (a,b9) // (b9,c) by AFVECT0:def 3;

          hence thesis by DIRAF:def 4;

        end;

        b = b9 implies thesis by A5, DIRAF:def 4;

        hence thesis by A3, A7, AFVECT0:def 2;

      end;

      now

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

        then a = c by AFVECT0: 4, AFVECT0: 7;

        then (a,b9) // (c,b9) by AFVECT0: 1;

        hence thesis by DIRAF:def 4;

      end;

      hence thesis by A1, A4, DIRAF:def 4;

    end;



     Lm11: for a, b, b9, c st a <> c & b <> b9 & (a,b) '||' (b,c) & (a,b9) '||' (b9,c) holds ex p, p9 st p <> p9 & (b,b9) '||' (p,p9) & (b,p) '||' (p,b9) & (b,p9) '||' (p9,b9)

    proof

      let a, b, b9, c;

      assume that

       A1: a <> c and

       A2: b <> b9 and

       A3: (a,b) '||' (b,c) and

       A4: (a,b9) '||' (b9,c);

      (a,b9) // (b9,c) by A1, A4, Lm1;

      then

       A5: Mid (a,b9,c) by AFVECT0:def 3;

      (a,b) // (b,c) by A1, A3, Lm1;

      then Mid (a,b,c) by AFVECT0:def 3;

      then MDist (b,b9) by A2, A5, AFVECT0: 20;

      then (b,b9) // (b9,b) by AFVECT0:def 2;

      then

      consider p, p9 such that

       A6: (b,b9) '||' (p,p9) and

       A7: (b,p) '||' (p,b9) & (b,p9) '||' (p9,b9) by Lm2;

      p <> p9 implies thesis by A6, A7;

      hence thesis by A2, A6, Lm5;

    end;



     Lm12: for a, b, c, p, p9, q, q9 st (a,b) '||' (p,p9) & (a,c) '||' (q,q9) & (a,p) '||' (p,b) & (a,q) '||' (q,c) & (a,p9) '||' (p9,b) & (a,q9) '||' (q9,c) holds ex r, r9 st (b,c) '||' (r,r9) & (b,r) '||' (r,c) & (b,r9) '||' (r9,c)

    proof

      let a, b, c, p, p9, q, q9;

      assume (a,b) '||' (p,p9) & (a,c) '||' (q,q9) & (a,p) '||' (p,b) & (a,q) '||' (q,c) & (a,p9) '||' (p9,b) & (a,q9) '||' (q9,c);

      then (a,b) // (b,a) & (a,c) // (c,a) by Lm2;

      then (b,c) // (c,b) by AFVECT0: 12;

      hence thesis by Lm2;

    end;

    set AFV0 = the WeakAffVect;

    set X = the carrier of AFV0;

    set XX = [:X, X:];

    defpred P[ object, object] means ex a,b,c,d be Element of X st $1 = [a, b] & $2 = [c, d] & (a,b) '||' (c,d);

    consider P be Relation of XX, XX such that

     Lm13: for x,y be object holds [x, y] in P iff x in XX & y in XX & P[x, y] from RELSET_1:sch 1;



     Lm14: for a,b,c,d be Element of X holds [ [a, b], [c, d]] in P iff (a,b) '||' (c,d)

    proof

      let a,b,c,d be Element of X;



       A1: [ [a, b], [c, d]] in P implies (a,b) '||' (c,d)

      proof

        assume [ [a, b], [c, d]] in P;

        then

        consider a9,b9,c9,d9 be Element of X such that

         A2: [a, b] = [a9, b9] and

         A3: [c, d] = [c9, d9] and

         A4: (a9,b9) '||' (c9,d9) by Lm13;



         A5: c = c9 by A3, XTUPLE_0: 1;

        a = a9 & b = b9 by A2, XTUPLE_0: 1;

        hence thesis by A3, A4, A5, XTUPLE_0: 1;

      end;

       [a, b] in XX & [c, d] in XX by ZFMISC_1:def 2;

      hence thesis by A1, Lm13;

    end;

    set WAS = AffinStruct (# the carrier of AFV0, P #);



     Lm15: for a,b,c,d be Element of AFV0, a9,b9,c9,d9 be Element of WAS st a = a9 & b = b9 & c = c9 & d = d9 holds (a,b) '||' (c,d) iff (a9,b9) // (c9,d9)

    proof

      let a,b,c,d be Element of AFV0, a9,b9,c9,d9 be Element of WAS such that

       A1: a = a9 & b = b9 & c = c9 & d = d9;

       A2:

      now

        assume (a9,b9) // (c9,d9);

        then [ [a9, b9], [c9, d9]] in P by ANALOAF:def 2;

        hence (a,b) '||' (c,d) by A1, Lm14;

      end;

      now

        assume (a,b) '||' (c,d);

        then [ [a, b], [c, d]] in the CONGR of WAS by Lm14;

        hence (a9,b9) // (c9,d9) by A1, ANALOAF:def 2;

      end;

      hence thesis by A2;

    end;

     Lm16:

    now

      thus ex a9,b9 be Element of WAS st a9 <> b9 by STRUCT_0:def 10;

      thus for a9,b9 be Element of WAS holds (a9,b9) // (b9,a9)

      proof

        let a9,b9 be Element of WAS;

        reconsider a = a9, b = b9 as Element of AFV0;

        (a,b) '||' (b,a) by Lm4;

        hence thesis by Lm15;

      end;

      thus for a9,b9 be Element of WAS st (a9,b9) // (a9,a9) holds a9 = b9

      proof

        let a9,b9 be Element of WAS such that

         A1: (a9,b9) // (a9,a9);

        reconsider a = a9, b = b9 as Element of AFV0;

        (a,b) '||' (a,a) by A1, Lm15;

        hence thesis by Lm5;

      end;

      thus for a,b,c,d,p,q be Element of WAS st (a,b) // (p,q) & (c,d) // (p,q) holds (a,b) // (c,d)

      proof

        let a,b,c,d,p,q be Element of WAS such that

         A2: (a,b) // (p,q) & (c,d) // (p,q);

        reconsider a1 = a, b1 = b, c1 = c, d1 = d, p1 = p, q1 = q as Element of AFV0;

        (a1,b1) '||' (p1,q1) & (c1,d1) '||' (p1,q1) by A2, Lm15;

        then (a1,b1) '||' (c1,d1) by Lm6;

        hence thesis by Lm15;

      end;

      thus for a,c be Element of WAS holds ex b be Element of WAS st (a,b) // (b,c)

      proof

        let a,c be Element of WAS;

        reconsider a1 = a, c1 = c as Element of AFV0;

        consider b1 be Element of AFV0 such that

         A3: (a1,b1) '||' (b1,c1) by Lm7;

        reconsider b = b1 as Element of WAS;

        (a,b) // (b,c) by A3, Lm15;

        hence thesis;

      end;

      thus for a,a9,b,b9,p be Element of WAS st a <> a9 & b <> b9 & (p,a) // (p,a9) & (p,b) // (p,b9) holds (a,b) // (a9,b9)

      proof

        let a,a9,b,b9,p be Element of WAS such that

         A4: a <> a9 & b <> b9 and

         A5: (p,a) // (p,a9) & (p,b) // (p,b9);

        reconsider a1 = a, a19 = a9, b1 = b, b19 = b9, p1 = p as Element of AFV0;

        (p1,a1) '||' (p1,a19) & (p1,b1) '||' (p1,b19) by A5, Lm15;

        then (a1,b1) '||' (a19,b19) by A4, Lm8;

        hence thesis by Lm15;

      end;

      thus for a,b be Element of WAS holds a = b or ex c be Element of WAS st a <> c & (a,b) // (b,c) or ex p,p9 be Element of WAS st p <> p9 & (a,b) // (p,p9) & (a,p) // (p,b) & (a,p9) // (p9,b)

      proof

        let a,b be Element of WAS such that

         A6: not a = b;

        reconsider a1 = a, b1 = b as Element of AFV0;

         A7:

        now

          given p1,p19 be Element of AFV0 such that

           A8: p1 <> p19 and

           A9: (a1,b1) '||' (p1,p19) & (a1,p1) '||' (p1,b1) and

           A10: (a1,p19) '||' (p19,b1);

          reconsider p = p1, p9 = p19 as Element of WAS;



           A11: (a,p9) // (p9,b) by A10, Lm15;

          (a,b) // (p,p9) & (a,p) // (p,b) by A9, Lm15;

          hence ex p,p9 be Element of WAS st p <> p9 & (a,b) // (p,p9) & (a,p) // (p,b) & (a,p9) // (p9,b) by A8, A11;

        end;

        now

          given c1 be Element of AFV0 such that

           A12: a1 <> c1 and

           A13: (a1,b1) '||' (b1,c1);

          reconsider c = c1 as Element of WAS;

          (a,b) // (b,c) by A13, Lm15;

          hence ex c be Element of WAS st a <> c & (a,b) // (b,c) by A12;

        end;

        hence thesis by A6, A7, Lm9;

      end;

      thus for a,b,b9,p,p9,c be Element of WAS st (a,b) // (b,c) & (b,b9) // (p,p9) & (b,p) // (p,b9) & (b,p9) // (p9,b9) holds (a,b9) // (b9,c)

      proof

        let a,b,b9,p,p9,c be Element of WAS such that

         A14: (a,b) // (b,c) & (b,b9) // (p,p9) and

         A15: (b,p) // (p,b9) & (b,p9) // (p9,b9);

        reconsider a1 = a, b1 = b, b19 = b9, p1 = p, p19 = p9, c1 = c as Element of AFV0;



         A16: (b1,p1) '||' (p1,b19) & (b1,p19) '||' (p19,b19) by A15, Lm15;

        (a1,b1) '||' (b1,c1) & (b1,b19) '||' (p1,p19) by A14, Lm15;

        then (a1,b19) '||' (b19,c1) by A16, Lm10;

        hence thesis by Lm15;

      end;

      thus for a,b,b9,c be Element of WAS st a <> c & b <> b9 & (a,b) // (b,c) & (a,b9) // (b9,c) holds ex p,p9 be Element of WAS st p <> p9 & (b,b9) // (p,p9) & (b,p) // (p,b9) & (b,p9) // (p9,b9)

      proof

        let a,b,b9,c be Element of WAS such that

         A17: a <> c & b <> b9 and

         A18: (a,b) // (b,c) & (a,b9) // (b9,c);

        reconsider a1 = a, b1 = b, b19 = b9, c1 = c as Element of AFV0;

        (a1,b1) '||' (b1,c1) & (a1,b19) '||' (b19,c1) by A18, Lm15;

        then

        consider p1,p19 be Element of AFV0 such that

         A19: p1 <> p19 and

         A20: (b1,b19) '||' (p1,p19) & (b1,p1) '||' (p1,b19) and

         A21: (b1,p19) '||' (p19,b19) by A17, Lm11;

        reconsider p = p1, p9 = p19 as Element of WAS;



         A22: (b,p9) // (p9,b9) by A21, Lm15;

        (b,b9) // (p,p9) & (b,p) // (p,b9) by A20, Lm15;

        hence thesis by A19, A22;

      end;

      thus for a,b,c,p,p9,q,q9 be Element of WAS st (a,b) // (p,p9) & (a,c) // (q,q9) & (a,p) // (p,b) & (a,q) // (q,c) & (a,p9) // (p9,b) & (a,q9) // (q9,c) holds ex r,r9 be Element of WAS st (b,c) // (r,r9) & (b,r) // (r,c) & (b,r9) // (r9,c)

      proof

        let a,b,c,p,p9,q,q9 be Element of WAS such that

         A23: (a,b) // (p,p9) & (a,c) // (q,q9) and

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

         A25: (a,p9) // (p9,b) & (a,q9) // (q9,c);

        reconsider a1 = a, b1 = b, c1 = c, p1 = p, p19 = p9, q1 = q, q19 = q9 as Element of AFV0;



         A26: (a1,p1) '||' (p1,b1) & (a1,q1) '||' (q1,c1) by A24, Lm15;



         A27: (a1,p19) '||' (p19,b1) & (a1,q19) '||' (q19,c1) by A25, Lm15;

        (a1,b1) '||' (p1,p19) & (a1,c1) '||' (q1,q19) by A23, Lm15;

        then

        consider r1,r19 be Element of AFV0 such that

         A28: (b1,c1) '||' (r1,r19) & (b1,r1) '||' (r1,c1) and

         A29: (b1,r19) '||' (r19,c1) by A26, A27, Lm12;

        reconsider r = r1, r9 = r19 as Element of WAS;



         A30: (b,r9) // (r9,c) by A29, Lm15;

        (b,c) // (r,r9) & (b,r) // (r,c) by A28, Lm15;

        hence thesis by A30;

      end;

    end;

    definition

      let IT be non empty AffinStruct;

      :: AFVECT01:def1

      attr IT is WeakAffSegm-like means

      : Def1: (for a,b be Element of IT holds (a,b) // (b,a)) & (for a,b be Element of IT st (a,b) // (a,a) holds a = b) & (for a,b,c,d,p,q be Element of IT st (a,b) // (p,q) & (c,d) // (p,q) holds (a,b) // (c,d)) & (for a,c be Element of IT holds ex b be Element of IT st (a,b) // (b,c)) & (for a,a9,b,b9,p be Element of IT st a <> a9 & b <> b9 & (p,a) // (p,a9) & (p,b) // (p,b9) holds (a,b) // (a9,b9)) & (for a,b be Element of IT holds a = b or ex c be Element of IT st (a <> c & (a,b) // (b,c)) or ex p,p9 be Element of IT st (p <> p9 & (a,b) // (p,p9) & (a,p) // (p,b) & (a,p9) // (p9,b))) & (for a,b,b9,p,p9,c be Element of IT st (a,b) // (b,c) & (b,b9) // (p,p9) & (b,p) // (p,b9) & (b,p9) // (p9,b9) holds (a,b9) // (b9,c)) & (for a,b,b9,c be Element of IT st a <> c & b <> b9 & (a,b) // (b,c) & (a,b9) // (b9,c) holds ex p,p9 be Element of IT st p <> p9 & (b,b9) // (p,p9) & (b,p) // (p,b9) & (b,p9) // (p9,b9)) & for a,b,c,p,p9,q,q9 be Element of IT st (a,b) // (p,p9) & (a,c) // (q,q9) & (a,p) // (p,b) & (a,q) // (q,c) & (a,p9) // (p9,b) & (a,q9) // (q9,c) holds ex r,r9 be Element of IT st (b,c) // (r,r9) & (b,r) // (r,c) & (b,r9) // (r9,c);

    end

    registration

      cluster strict WeakAffSegm-like for non trivial AffinStruct;

      existence

      proof

        WAS is WeakAffSegm-like non trivial by Lm16;

        hence thesis;

      end;

    end

    definition

      mode WeakAffSegm is WeakAffSegm-like non trivial AffinStruct;

    end

    reserve AFV for WeakAffSegm;

    reserve a,b,b9,b99,c,d,p,p9 for Element of AFV;

    theorem :: AFVECT01:1



     Th1: (a,b) // (a,b)

    proof

      (a,b) // (b,a) by Def1;

      hence thesis by Def1;

    end;

    theorem :: AFVECT01:2



     Th2: (a,b) // (c,d) implies (c,d) // (a,b)

    proof

      assume

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

      (c,d) // (c,d) by Th1;

      hence thesis by A1, Def1;

    end;

    theorem :: AFVECT01:3



     Th3: (a,b) // (c,d) implies (a,b) // (d,c)

    proof

      assume

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

      (d,c) // (c,d) by Def1;

      hence thesis by A1, Def1;

    end;

    theorem :: AFVECT01:4



     Th4: (a,b) // (c,d) implies (b,a) // (c,d)

    proof

      assume (a,b) // (c,d);

      then (c,d) // (a,b) by Th2;

      then (c,d) // (b,a) by Th3;

      hence thesis by Th2;

    end;

    theorem :: AFVECT01:5



     Th5: for a, b holds (a,a) // (b,b)

    proof

      let a, b;

      now

        consider c such that

         A1: (a,c) // (c,b) by Def1;

        assume

         A2: a <> b;

        (c,a) // (c,b) by A1, Th4;

        hence thesis by A2, Def1;

      end;

      hence thesis by Def1;

    end;

    theorem :: AFVECT01:6



     Th6: (a,b) // (c,c) implies a = b

    proof

      assume

       A1: (a,b) // (c,c);

      (a,a) // (c,c) by Th5;

      then (a,b) // (a,a) by A1, Def1;

      hence thesis by Def1;

    end;

    theorem :: AFVECT01:7



     Th7: (a,b) // (p,p9) & (a,b) // (b,c) & (a,p) // (p,b) & (a,p9) // (p9,b) implies a = c

    proof

      assume that

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

       A2: (a,b) // (b,c) and

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

       A4: (a,p9) // (p9,b);

      (p,b) // (a,p) by A3, Th2;

      then (p,b) // (p,a) by Th3;

      then

       A5: (b,p) // (p,a) by Th4;

      (p9,b) // (a,p9) by A4, Th2;

      then (p9,b) // (p9,a) by Th3;

      then

       A6: (b,p9) // (p9,a) by Th4;

      (b,a) // (p,p9) by A1, Th4;

      then (a,a) // (a,c) by A2, A5, A6, Def1;

      then (a,c) // (a,a) by Th2;

      hence thesis by Def1;

    end;

    theorem :: AFVECT01:8

    (a,b9) // (a,b99) & (a,b) // (a,b99) implies b = b9 or b = b99 or b9 = b99

    proof

      assume

       A1: (a,b9) // (a,b99) & (a,b) // (a,b99);

      now

        assume b9 <> b99 & b <> b99;

        then (b9,b) // (b99,b99) by A1, Def1;

        hence thesis by Th6;

      end;

      hence thesis;

    end;

    definition

      let AFV;

      let a, b;

      :: AFVECT01:def2

      pred MDist a,b means ex p, p9 st p <> p9 & (a,b) // (p,p9) & (a,p) // (p,b) & (a,p9) // (p9,b);

    end

    definition

      let AFV;

      let a, b, c;

      :: AFVECT01:def3

      pred Mid a,b,c means a = b & b = c & a = c or a = c & MDist (a,b) or a <> c & (a,b) // (b,c);

    end

    theorem :: AFVECT01:9

    a <> b & not MDist (a,b) implies ex c st a <> c & (a,b) // (b,c) by Def1;

    theorem :: AFVECT01:10

     MDist (a,b) & (a,b) // (b,c) implies a = c by Th7;

    theorem :: AFVECT01:11

     MDist (a,b) implies a <> b by Th2, Th6;