diraf.miz

    begin

    reserve x,y for set;

    reserve X for non empty set;

    reserve a,b,c,d for Element of X;

    definition

      let X;

      let R be Relation of [:X, X:];

      :: DIRAF:def1

      func lambda (R) -> Relation of [:X, X:] means

      : Def1: for a,b,c,d be Element of X holds [ [a, b], [c, d]] in it iff ( [ [a, b], [c, d]] in R or [ [a, b], [d, c]] in R);

      existence

      proof

        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]] in R or [ [a, b], [d, c]] in R);

        set XX = [:X, X:];

        consider P be Relation of XX, XX such that

         A1: 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;

        take P;

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

         [ [a, b], [c, d]] in P implies ( [ [a, b], [c, d]] in R or [ [a, b], [d, c]] in R)

        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]] in R or [ [a9, b9], [d9, c9]] in R by A1;

          c = c9 by A3, XTUPLE_0: 1;

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

        end;

        hence thesis by A1;

      end;

      uniqueness

      proof

        set XX = [:X, X:];

        let P,Q be Relation of [:X, X:] such that

         A5: for a,b,c,d be Element of X holds [ [a, b], [c, d]] in P iff ( [ [a, b], [c, d]] in R or [ [a, b], [d, c]] in R) and

         A6: for a,b,c,d be Element of X holds [ [a, b], [c, d]] in Q iff ( [ [a, b], [c, d]] in R or [ [a, b], [d, c]] in R);

        for x,y be object holds [x, y] in P iff [x, y] in Q

        proof

          let x,y be object;

           A7:

          now

            assume

             A8: [x, y] in Q;

            then y in XX by ZFMISC_1: 87;

            then

            consider c, d such that

             A9: y = [c, d] by DOMAIN_1: 1;

            x in XX by A8, ZFMISC_1: 87;

            then

             A10: ex a, b st x = [a, b] by DOMAIN_1: 1;

            then [x, y] in Q iff [x, y] in R or [x, [d, c]] in R by A6, A9;

            hence [x, y] in P by A5, A8, A10, A9;

          end;

          now

            assume

             A11: [x, y] in P;

            then y in XX by ZFMISC_1: 87;

            then

            consider c, d such that

             A12: y = [c, d] by DOMAIN_1: 1;

            x in XX by A11, ZFMISC_1: 87;

            then

             A13: ex a, b st x = [a, b] by DOMAIN_1: 1;

            then [x, y] in P iff [x, y] in R or [x, [d, c]] in R by A5, A12;

            hence [x, y] in Q by A6, A11, A13, A12;

          end;

          hence thesis by A7;

        end;

        hence thesis by RELAT_1:def 2;

      end;

    end

    definition

      let S be non empty AffinStruct;

      :: DIRAF:def2

      func Lambda (S) -> strict AffinStruct equals AffinStruct (# the carrier of S, ( lambda the CONGR of S) #);

      correctness ;

    end

    registration

      let S be non empty AffinStruct;

      cluster ( Lambda S) -> non empty;

      coherence ;

    end

    reserve S for OAffinSpace;

    reserve a,b,c,d,p,q,r,x,y,z,t,u,w for Element of S;

    theorem :: DIRAF:1



     Th1: (x,y) // (x,y)

    proof

      (x,y) // (y,y) by ANALOAF:def 5;

      hence thesis by ANALOAF:def 5;

    end;



     Lm1: (x,y) // (z,t) implies (z,t) // (x,y)

    proof

      assume

       A1: (x,y) // (z,t);

      now

        assume

         A2: x <> y;

        (x,y) // (x,y) by Th1;

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

      end;

      hence thesis by ANALOAF:def 5;

    end;

    theorem :: DIRAF:2



     Th2: (x,y) // (z,t) implies (y,x) // (t,z) & (z,t) // (x,y) & (t,z) // (y,x)

    proof

      assume (x,y) // (z,t);

      hence (y,x) // (t,z) & (z,t) // (x,y) by Lm1, ANALOAF:def 5;

      hence thesis by ANALOAF:def 5;

    end;

    theorem :: DIRAF:3



     Th3: z <> t & (x,y) // (z,t) & (z,t) // (u,w) implies (x,y) // (u,w)

    proof

      assume

       A1: z <> t;

      assume that

       A2: (x,y) // (z,t) and

       A3: (z,t) // (u,w);

      (z,t) // (x,y) by A2, Th2;

      hence thesis by A1, A3, ANALOAF:def 5;

    end;

    theorem :: DIRAF:4



     Th4: (x,x) // (y,z) & (y,z) // (x,x)

    proof

      (y,z) // (x,x) by ANALOAF:def 5;

      hence thesis by Th2;

    end;

    theorem :: DIRAF:5



     Th5: (x,y) // (z,t) & (x,y) // (t,z) implies x = y or z = t

    proof

      assume that

       A1: (x,y) // (z,t) & (x,y) // (t,z) & x <> y and

       A2: z <> t;

      (z,t) // (t,z) by A1, ANALOAF:def 5;

      hence contradiction by A2, ANALOAF:def 5;

    end;

    theorem :: DIRAF:6



     Th6: (x,y) // (x,z) iff (x,y) // (y,z) or (x,z) // (z,y)

    proof

      now

        assume (x,y) // (y,z) or (x,z) // (z,y);

        then (x,y) // (x,z) or (x,z) // (x,y) by ANALOAF:def 5;

        hence (x,y) // (x,z) by Th2;

      end;

      hence thesis by ANALOAF:def 5;

    end;

    definition

      let S be non empty AffinStruct;

      let a,b,c be Element of S;

      :: DIRAF:def3

      pred Mid a,b,c means (a,b) // (b,c);

    end

    theorem :: DIRAF:7



     Th7: (x,y) // (x,z) iff Mid (x,y,z) or Mid (x,z,y) by Th6;

    theorem :: DIRAF:8



     Th8: Mid (a,b,a) implies a = b by ANALOAF:def 5;

    theorem :: DIRAF:9

     Mid (a,b,c) implies Mid (c,b,a) by Th2;

    theorem :: DIRAF:10

     Mid (x,x,y) & Mid (x,y,y) by Th4;

    theorem :: DIRAF:11

     Mid (a,b,c) & Mid (a,c,d) implies Mid (b,c,d)

    proof

      assume that

       A1: Mid (a,b,c) and

       A2: Mid (a,c,d);

      now



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

        then (a,b) // (a,c) by ANALOAF:def 5;

        then

         A4: (b,c) // (a,c) or a = b by A3, ANALOAF:def 5;

        assume

         A5: a <> c;

        (a,c) // (c,d) by A2;

        then (b,c) // (c,d) by A5, A4, Th3;

        hence thesis;

      end;

      hence thesis by A1, A2, Th8;

    end;

    theorem :: DIRAF:12

    b <> c & Mid (a,b,c) & Mid (b,c,d) implies Mid (a,c,d)

    proof

      assume that

       A1: b <> c and

       A2: Mid (a,b,c) and

       A3: Mid (b,c,d);

      now

        assume

         A4: a <> b;



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

        (b,c) // (c,d) by A3;

        then

         A6: (a,b) // (c,d) by A1, A5, Th3;

        (a,b) // (a,c) by A5, ANALOAF:def 5;

        then (a,c) // (c,d) by A4, A6, ANALOAF:def 5;

        hence thesis;

      end;

      hence thesis by A3;

    end;

    theorem :: DIRAF:13



     Th13: ex z st Mid (x,y,z) & y <> z

    proof

      consider z such that

       A1: (x,y) // (y,z) and (x,y) // (y,z) and

       A2: y <> z by ANALOAF:def 5;

       Mid (x,y,z) by A1;

      hence thesis by A2;

    end;

    theorem :: DIRAF:14

     Mid (x,y,z) & Mid (y,x,z) implies x = y

    proof

      assume that

       A1: Mid (x,y,z) and

       A2: Mid (y,x,z);

      (x,y) // (y,z) by A1;

      then

       A3: (x,y) // (x,z) by ANALOAF:def 5;

      (y,x) // (x,z) by A2;

      then

       A4: (x,y) // (z,x) by ANALOAF:def 5;

      x = z implies x = y by A1, Th8;

      hence thesis by A3, A4, Th5;

    end;

    theorem :: DIRAF:15

    x <> y & Mid (x,y,z) & Mid (x,y,t) implies Mid (y,z,t) or Mid (y,t,z)

    proof

      assume

       A1: x <> y;

      assume Mid (x,y,z) & Mid (x,y,t);

      then (x,y) // (y,z) & (x,y) // (y,t);

      then (y,z) // (y,t) by A1, ANALOAF:def 5;

      hence thesis by Th7;

    end;

    theorem :: DIRAF:16

    x <> y & Mid (x,y,z) & Mid (x,y,t) implies Mid (x,z,t) or Mid (x,t,z)

    proof

      assume

       A1: x <> y;

      assume that

       A2: Mid (x,y,z) and

       A3: Mid (x,y,t);

      (x,y) // (y,t) by A3;

      then

       A4: (x,y) // (x,t) by ANALOAF:def 5;

      (x,y) // (y,z) by A2;

      then (x,y) // (x,z) by ANALOAF:def 5;

      then (x,z) // (x,t) by A1, A4, ANALOAF:def 5;

      hence thesis by Th7;

    end;

    theorem :: DIRAF:17

     Mid (x,y,t) & Mid (x,z,t) implies Mid (x,y,z) or Mid (x,z,y)

    proof

      assume that

       A1: Mid (x,y,t) and

       A2: Mid (x,z,t);



       A3: (x,z) // (z,t) by A2;



       A4: (x,y) // (y,t) by A1;

      now

        (x,z) // (x,t) by A3, ANALOAF:def 5;

        then

         A5: (x,t) // (x,z) by Th2;

        assume

         A6: x <> t;

        (x,y) // (x,t) by A4, ANALOAF:def 5;

        then (x,y) // (x,z) by A6, A5, Th3;

        hence thesis by Th7;

      end;

      hence thesis by A1, A2, Th8;

    end;

    definition

      let S be non empty AffinStruct;

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

      :: DIRAF:def4

      pred a,b '||' c,d means (a,b) // (c,d) or (a,b) // (d,c);

    end

    theorem :: DIRAF:18

    (a,b) '||' (c,d) iff [ [a, b], [c, d]] in ( lambda the CONGR of S)

    proof

      thus (a,b) '||' (c,d) implies [ [a, b], [c, d]] in ( lambda the CONGR of S)

      proof

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

        then [ [a, b], [c, d]] in the CONGR of S or [ [a, b], [d, c]] in the CONGR of S;

        hence thesis by Def1;

      end;

      assume [ [a, b], [c, d]] in ( lambda the CONGR of S);

      then [ [a, b], [c, d]] in the CONGR of S or [ [a, b], [d, c]] in the CONGR of S by Def1;

      hence (a,b) // (c,d) or (a,b) // (d,c);

    end;

    theorem :: DIRAF:19



     Th19: (x,y) '||' (y,x) & (x,y) '||' (x,y) by Th1;

    theorem :: DIRAF:20



     Th20: (x,y) '||' (z,z) & (z,z) '||' (x,y) by Th4;



     Lm2: x <> y & (x,y) '||' (z,t) & (x,y) '||' (u,w) implies (z,t) '||' (u,w)

    proof

      assume that

       A1: x <> y and

       A2: (x,y) '||' (z,t) and

       A3: (x,y) '||' (u,w);



       A4: (x,y) // (u,w) or (x,y) // (w,u) by A3;

       A5:

      now

        assume (x,y) // (t,z);

        then (t,z) // (u,w) or (t,z) // (w,u) by A1, A4, ANALOAF:def 5;

        then (z,t) // (w,u) or (z,t) // (u,w) by ANALOAF:def 5;

        hence thesis;

      end;

      (x,y) // (z,t) implies thesis by A1, A4, ANALOAF:def 5;

      hence thesis by A2, A5;

    end;

    theorem :: DIRAF:21



     Th21: (x,y) '||' (x,z) implies (y,x) '||' (y,z)

    proof

       A1:

      now

        assume (x,y) // (z,x);

        then (y,x) // (x,z) by ANALOAF:def 5;

        then (y,x) // (y,z) by ANALOAF:def 5;

        hence thesis;

      end;

       A2:

      now

         A3:

        now

          assume (x,z) // (z,y);

          then (y,z) // (z,x) by Th2;

          then (y,z) // (y,x) by ANALOAF:def 5;

          then (y,x) // (y,z) by Th2;

          hence thesis;

        end;



         A4: (x,y) // (y,z) implies thesis by ANALOAF:def 5;

        assume (x,y) // (x,z);

        hence thesis by A4, A3, ANALOAF:def 5;

      end;

      assume (x,y) '||' (x,z);

      hence thesis by A2, A1;

    end;

    theorem :: DIRAF:22



     Th22: (x,y) '||' (z,t) implies (x,y) '||' (t,z) & (y,x) '||' (z,t) & (y,x) '||' (t,z) & (z,t) '||' (x,y) & (z,t) '||' (y,x) & (t,z) '||' (x,y) & (t,z) '||' (y,x) by Th2;

    theorem :: DIRAF:23



     Th23: a <> b & ((a,b) '||' (x,y) & (a,b) '||' (z,t) or (a,b) '||' (x,y) & (z,t) '||' (a,b) or (x,y) '||' (a,b) & (z,t) '||' (a,b) or (x,y) '||' (a,b) & (a,b) '||' (z,t)) implies (x,y) '||' (z,t)

    proof

      assume that

       A1: a <> b and

       A2: (a,b) '||' (x,y) & (a,b) '||' (z,t) or (a,b) '||' (x,y) & (z,t) '||' (a,b) or (x,y) '||' (a,b) & (z,t) '||' (a,b) or (x,y) '||' (a,b) & (a,b) '||' (z,t);

      (a,b) '||' (x,y) & (a,b) '||' (z,t) by A2, Th22;

      hence thesis by A1, Lm2;

    end;

    theorem :: DIRAF:24



     Th24: ex x, y, z st not (x,y) '||' (x,z)

    proof

      consider x, y, z, t such that

       A1: not (x,y) // (z,t) and

       A2: not (x,y) // (t,z) by ANALOAF:def 5;



       A3: x <> y by A1, Th4;

      now

        assume

         A4: (x,y) '||' (x,z);

        thus not (x,y) '||' (x,t)

        proof

          assume

           A5: (x,y) '||' (x,t);

          then (x,z) '||' (x,t) by A3, A4, Th23;

          then (z,x) '||' (z,t) by Th21;

          then (x,z) '||' (z,t) by Th22;

          then (x,y) '||' (z,t) or x = z by A4, Th23;

          hence contradiction by A1, A2, A5;

        end;

      end;

      hence thesis;

    end;

    theorem :: DIRAF:25



     Th25: ex t st (x,z) '||' (y,t) & y <> t

    proof

      consider t such that (x,y) // (z,t) and

       A1: (x,z) // (y,t) and

       A2: y <> t by ANALOAF:def 5;

      (x,z) '||' (y,t) by A1;

      hence thesis by A2;

    end;

    theorem :: DIRAF:26



     Th26: ex t st (x,y) '||' (z,t) & (x,z) '||' (y,t)

    proof

      consider t such that

       A1: (x,y) // (z,t) & (x,z) // (y,t) and y <> t by ANALOAF:def 5;

      (x,y) '||' (z,t) & (x,z) '||' (y,t) by A1;

      hence thesis;

    end;

    theorem :: DIRAF:27



     Th27: (z,x) '||' (x,t) & x <> z implies ex u st (y,x) '||' (x,u) & (y,z) '||' (t,u)

    proof

      assume that

       A1: (z,x) '||' (x,t) and

       A2: x <> z;

       A3:

      now

        consider p such that

         A4: Mid (z,x,p) and

         A5: x <> p by Th13;



         A6: (z,x) // (x,p) by A4;

        then

        consider q such that

         A7: (y,x) // (x,q) and

         A8: (y,z) // (p,q) by A2, ANALOAF:def 5;

        assume

         A9: (z,x) // (t,x);

        then (x,p) // (t,x) by A2, A6, ANALOAF:def 5;

        then (p,x) // (x,t) by Th2;

        then

        consider r such that

         A10: (q,x) // (x,r) and

         A11: (q,p) // (t,r) by A5, ANALOAF:def 5;

         A12:

        now

          assume q = p;

          then

           A13: (x,p) // (y,x) by A7, Th2;

          (x,p) // (z,x) by A6, Th2;

          then (z,x) // (y,x) by A5, A13, ANALOAF:def 5;

          then (y,x) // (t,x) by A2, A9, ANALOAF:def 5;

          then

           A14: (y,x) '||' (x,t);

          (y,z) // (t,t) by ANALOAF:def 5;

          then (y,z) '||' (t,t);

          hence thesis by A14;

        end;

         A15:

        now



           A16: (x,z) // (x,t) by A9, Th2;

          assume

           A17: q = x;

          (p,x) // (x,z) by A6, Th2;

          then (y,z) // (x,z) by A5, A8, A17, Th3;

          then (y,z) // (x,t) by A2, A16, Th3;

          then

           A18: (y,z) '||' (t,x);

          (y,x) // (x,x) by Th4;

          then (y,x) '||' (x,x);

          hence thesis by A18;

        end;

        now

          assume that

           A19: q <> p and

           A20: q <> x;

          (x,q) // (r,x) by A10, Th2;

          then (y,x) // (r,x) by A7, A20, Th3;

          then

           A21: (y,x) '||' (x,r);

          (p,q) // (r,t) by A11, Th2;

          then (y,z) // (r,t) by A8, A19, Th3;

          then (y,z) '||' (t,r);

          hence thesis by A21;

        end;

        hence thesis by A12, A15;

      end;

      now

        assume (z,x) // (x,t);

        then

        consider u such that

         A22: (y,x) // (x,u) & (y,z) // (t,u) by A2, ANALOAF:def 5;

        (y,x) '||' (x,u) & (y,z) '||' (t,u) by A22;

        hence thesis;

      end;

      hence thesis by A1, A3;

    end;

    definition

      let S be non empty AffinStruct;

      let a,b,c be Element of S;

      :: DIRAF:def5

      pred a,b,c are_collinear means (a,b) '||' (a,c);

    end

    theorem :: DIRAF:28

     Mid (a,b,c) implies (a,b,c) are_collinear

    proof

      assume Mid (a,b,c);

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

      then (a,b) // (a,c) by ANALOAF:def 5;

      then (a,b) '||' (a,c);

      hence thesis;

    end;

    theorem :: DIRAF:29

    (a,b,c) are_collinear implies Mid (a,b,c) or Mid (b,a,c) or Mid (a,c,b)

    proof



       A1: (a,b) // (c,a) implies Mid (b,a,c) by ANALOAF:def 5;

      assume (a,b,c) are_collinear ;

      then

       A2: (a,b) '||' (a,c);

      (a,b) // (a,c) implies ( Mid (a,b,c) or Mid (a,c,b)) by Th7;

      hence thesis by A2, A1;

    end;



     Lm3: (x,y,z) are_collinear implies (x,z,y) are_collinear & (y,x,z) are_collinear by Th21, Th22;

    theorem :: DIRAF:30



     Th30: (x,y,z) are_collinear implies (x,z,y) are_collinear & (y,x,z) are_collinear & (y,z,x) are_collinear & (z,x,y) are_collinear & (z,y,x) are_collinear

    proof

      assume (x,y,z) are_collinear ;

      hence (x,z,y) are_collinear & (y,x,z) are_collinear by Lm3;

      hence (y,z,x) are_collinear & (z,x,y) are_collinear by Lm3;

      hence thesis by Lm3;

    end;

    theorem :: DIRAF:31



     Th31: (x,x,y) are_collinear & (x,y,y) are_collinear & (x,y,x) are_collinear by Th19, Th20;

    theorem :: DIRAF:32



     Th32: x <> y & (x,y,z) are_collinear & (x,y,t) are_collinear & (x,y,u) are_collinear implies (z,t,u) are_collinear

    proof

      assume that

       A1: x <> y and

       A2: (x,y,z) are_collinear and

       A3: (x,y,t) are_collinear and

       A4: (x,y,u) are_collinear ;

       A5:

      now



         A6: (x,y) '||' (x,z) by A2;

        (x,y) '||' (x,u) by A4;

        then (x,z) '||' (x,u) by A1, A6, Th23;

        then

         A7: (z,x) '||' (z,u) by Th21;

        (x,y) '||' (x,t) by A3;

        then (x,z) '||' (x,t) by A1, A6, Th23;

        then

         A8: (z,x) '||' (z,t) by Th21;

        assume x <> z;

        then (z,t) '||' (z,u) by A8, A7, Th23;

        hence thesis;

      end;

      x = z implies thesis by A3, A4, A1, Th23;

      hence thesis by A5;

    end;

    theorem :: DIRAF:33

    x <> y & (x,y,z) are_collinear & (x,y) '||' (z,t) implies (x,y,t) are_collinear

    proof

      assume that

       A1: x <> y and

       A2: (x,y,z) are_collinear and

       A3: (x,y) '||' (z,t);

      now

        (x,y) '||' (x,z) by A2;

        then (x,z) '||' (z,t) by A1, A3, Th23;

        then (z,x) '||' (z,t) by Th22;

        then (z,x,t) are_collinear ;

        then

         A4: (x,z,t) are_collinear by Th30;

        assume

         A5: z <> x;

        (x,z,y) are_collinear & (x,z,x) are_collinear by A2, Th30, Th31;

        hence thesis by A5, A4, Th32;

      end;

      hence thesis by A3;

    end;

    theorem :: DIRAF:34

    (x,y,z) are_collinear & (x,y,t) are_collinear implies (x,y) '||' (z,t)

    proof

      assume

       A1: (x,y,z) are_collinear & (x,y,t) are_collinear ;

      now



         A2: (x,y) '||' (x,z) & (x,y) '||' (x,t) by A1;

        assume x <> y;

        then (x,z) '||' (x,t) by A2, Th23;

        then (z,x) '||' (z,t) by Th21;

        then (x,z) '||' (z,t) by Th22;

        hence thesis by A2, Th23;

      end;

      hence thesis by Th20;

    end;

    theorem :: DIRAF:35

    u <> z & (x,y,u) are_collinear & (x,y,z) are_collinear & (u,z,w) are_collinear implies (x,y,w) are_collinear

    proof

      assume that

       A1: u <> z and

       A2: (x,y,u) are_collinear & (x,y,z) are_collinear and

       A3: (u,z,w) are_collinear ;

      now

        assume

         A4: x <> y;

        (x,y,x) are_collinear by Th31;

        then

         A5: (z,u,x) are_collinear by A2, A4, Th32;

        (x,y,y) are_collinear by Th31;

        then

         A6: (z,u,y) are_collinear by A2, A4, Th32;

        (z,u,w) are_collinear by A3, Th30;

        hence thesis by A1, A6, A5, Th32;

      end;

      hence thesis by Th31;

    end;

    theorem :: DIRAF:36



     Th36: ex x, y, z st not (x,y,z) are_collinear

    proof

      consider x, y, z such that

       A1: not (x,y) '||' (x,z) by Th24;

       not (x,y,z) are_collinear by A1;

      hence thesis;

    end;

    theorem :: DIRAF:37

    x <> y implies ex z st not (x,y,z) are_collinear

    proof

      assume

       A1: x <> y;

      consider a, b, c such that

       A2: not (a,b,c) are_collinear by Th36;

      assume

       A3: not thesis;

      then

       A4: (x,y,c) are_collinear ;

      (x,y,a) are_collinear & (x,y,b) are_collinear by A3;

      hence contradiction by A1, A2, A4, Th32;

    end;

    reserve AS for non empty AffinStruct;

    theorem :: DIRAF:38



     Th38: AS = ( Lambda S) implies for a,b,c,d be Element of S, a9,b9,c9,d9 be Element of AS st a = a9 & b = b9 & c = c9 & d = d9 holds (a9,b9) // (c9,d9) iff (a,b) '||' (c,d)

    proof

      assume

       A1: AS = ( Lambda S);

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

      let a9,b9,c9,d9 be Element of AS;

      assume

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

      thus (a9,b9) // (c9,d9) implies (a,b) '||' (c,d)

      proof

        assume

         A3: [ [a9, b9], [c9, d9]] in the CONGR of AS;

        assume not [ [a, b], [c, d]] in the CONGR of S;

        hence [ [a, b], [d, c]] in the CONGR of S by A1, A2, A3, Def1;

      end;

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

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

      then [ [a, b], [c, d]] in the CONGR of S or [ [a, b], [d, c]] in the CONGR of S;

      hence [ [a9, b9], [c9, d9]] in the CONGR of AS by A1, A2, Def1;

    end;

    theorem :: DIRAF:39



     Th39: AS = ( Lambda S) implies (ex x,y be Element of AS st x <> y) & (for x,y,z,t,u,w be Element of AS holds (x,y) // (y,x) & (x,y) // (z,z) & (x <> y & (x,y) // (z,t) & (x,y) // (u,w) implies (z,t) // (u,w)) & ((x,y) // (x,z) implies (y,x) // (y,z))) & (ex x,y,z be Element of AS st not (x,y) // (x,z)) & (for x,y,z be Element of AS holds ex t be Element of AS st (x,z) // (y,t) & y <> t) & (for x,y,z be Element of AS holds ex t be Element of AS st (x,y) // (z,t) & (x,z) // (y,t)) & for x,y,z,t be Element of AS st (z,x) // (x,t) & x <> z holds ex u be Element of AS st (y,x) // (x,u) & (y,z) // (t,u)

    proof

      assume

       A1: AS = ( Lambda S);

      hence ex x,y be Element of AS st x <> y by STRUCT_0:def 10;

      thus for x,y,z,t,u,w be Element of AS holds (x,y) // (y,x) & (x,y) // (z,z) & (x <> y & (x,y) // (z,t) & (x,y) // (u,w) implies (z,t) // (u,w)) & ((x,y) // (x,z) implies (y,x) // (y,z))

      proof

        let x,y,z,t,u,w be Element of AS;

        reconsider x9 = x, y9 = y, z9 = z, t9 = t, u9 = u, w9 = w as Element of S by A1;

        (x9,y9) '||' (y9,x9) & (x9,y9) '||' (z9,z9) by Th19, Th20;

        hence (x,y) // (y,x) & (x,y) // (z,z) by A1, Th38;

        x9 <> y9 & (x9,y9) '||' (z9,t9) & (x9,y9) '||' (u9,w9) implies (z9,t9) '||' (u9,w9) by Lm2;

        hence x <> y & (x,y) // (z,t) & (x,y) // (u,w) implies (z,t) // (u,w) by A1, Th38;

        (x9,y9) '||' (x9,z9) implies (y9,x9) '||' (y9,z9) by Th21;

        hence thesis by A1, Th38;

      end;

      thus ex x,y,z be Element of AS st not (x,y) // (x,z)

      proof

        consider x9,y9,z9 be Element of S such that

         A2: not (x9,y9) '||' (x9,z9) by Th24;

        reconsider x = x9, y = y9, z = z9 as Element of AS by A1;

         not (x,y) // (x,z) by A1, A2, Th38;

        hence thesis;

      end;

      thus for x,y,z be Element of AS holds ex t be Element of AS st (x,z) // (y,t) & y <> t

      proof

        let x,y,z be Element of AS;

        reconsider x9 = x, y9 = y, z9 = z as Element of S by A1;

        consider t9 be Element of S such that

         A3: (x9,z9) '||' (y9,t9) and

         A4: y9 <> t9 by Th25;

        reconsider t = t9 as Element of AS by A1;

        (x,z) // (y,t) by A1, A3, Th38;

        hence thesis by A4;

      end;

      thus for x,y,z be Element of AS holds ex t be Element of AS st (x,y) // (z,t) & (x,z) // (y,t)

      proof

        let x,y,z be Element of AS;

        reconsider x9 = x, y9 = y, z9 = z as Element of S by A1;

        consider t9 be Element of S such that

         A5: (x9,y9) '||' (z9,t9) & (x9,z9) '||' (y9,t9) by Th26;

        reconsider t = t9 as Element of AS by A1;

        (x,y) // (z,t) & (x,z) // (y,t) by A1, A5, Th38;

        hence thesis;

      end;

      thus for x,y,z,t be Element of AS st (z,x) // (x,t) & x <> z holds ex u be Element of AS st (y,x) // (x,u) & (y,z) // (t,u)

      proof

        let x,y,z,t be Element of AS such that

         A6: (z,x) // (x,t) and

         A7: x <> z;

        reconsider x9 = x, y9 = y, z9 = z, t9 = t as Element of S by A1;

        (z9,x9) '||' (x9,t9) by A1, A6, Th38;

        then

        consider u9 be Element of S such that

         A8: (y9,x9) '||' (x9,u9) & (y9,z9) '||' (t9,u9) by A7, Th27;

        reconsider u = u9 as Element of AS by A1;

        (y,x) // (x,u) & (y,z) // (t,u) by A1, A8, Th38;

        hence thesis;

      end;

    end;

    definition

      let IT be non empty AffinStruct;

      :: DIRAF:def6

      attr IT is AffinSpace-like means

      : Def6: (for x,y,z,t,u,w be Element of IT holds (x,y) // (y,x) & (x,y) // (z,z) & (x <> y & (x,y) // (z,t) & (x,y) // (u,w) implies (z,t) // (u,w)) & ((x,y) // (x,z) implies (y,x) // (y,z))) & (ex x,y,z be Element of IT st not (x,y) // (x,z)) & (for x,y,z be Element of IT holds ex t be Element of IT st (x,z) // (y,t) & y <> t) & (for x,y,z be Element of IT holds ex t be Element of IT st (x,y) // (z,t) & (x,z) // (y,t)) & for x,y,z,t be Element of IT st (z,x) // (x,t) & x <> z holds ex u be Element of IT st (y,x) // (x,u) & (y,z) // (t,u);

    end

    registration

      cluster strict AffinSpace-like for non trivial AffinStruct;

      existence

      proof

        set S = the OAffinSpace;



         A1: (for x,y,z be Element of ( Lambda S) holds ex t be Element of ( Lambda S) st (x,z) // (y,t) & y <> t) & for x,y,z be Element of ( Lambda S) holds ex t be Element of ( Lambda S) st (x,y) // (z,t) & (x,z) // (y,t) by Th39;



         A2: for x,y,z,t be Element of ( Lambda S) st (z,x) // (x,t) & x <> z holds ex u be Element of ( Lambda S) st (y,x) // (x,u) & (y,z) // (t,u) by Th39;

        (for x,y,z,t,u,w be Element of ( Lambda S) holds (x,y) // (y,x) & (x,y) // (z,z) & (x <> y & (x,y) // (z,t) & (x,y) // (u,w) implies (z,t) // (u,w)) & ((x,y) // (x,z) implies (y,x) // (y,z))) & ex x,y,z be Element of ( Lambda S) st not (x,y) // (x,z) by Th39;

        then ( Lambda S) is non trivial AffinSpace-like by A1, A2;

        hence thesis;

      end;

    end

    definition

      mode AffinSpace is AffinSpace-like non trivial AffinStruct;

    end

    theorem :: DIRAF:40

    for AS be AffinSpace holds (ex x,y be Element of AS st x <> y) & (for x,y,z,t,u,w be Element of AS holds ((x,y) // (y,x) & (x,y) // (z,z)) & (x <> y & (x,y) // (z,t) & (x,y) // (u,w) implies (z,t) // (u,w)) & ((x,y) // (x,z) implies (y,x) // (y,z))) & (ex x,y,z be Element of AS st not (x,y) // (x,z)) & (for x,y,z be Element of AS holds ex t be Element of AS st (x,z) // (y,t) & y <> t) & (for x,y,z be Element of AS holds ex t be Element of AS st (x,y) // (z,t) & (x,z) // (y,t)) & for x,y,z,t be Element of AS st (z,x) // (x,t) & x <> z holds ex u be Element of AS st (y,x) // (x,u) & (y,z) // (t,u) by Def6, STRUCT_0:def 10;

    theorem :: DIRAF:41



     Th41: ( Lambda S) is AffinSpace

    proof

      set AS = ( Lambda S);



       A1: (for x,y,z be Element of AS holds ex t be Element of AS st (x,z) // (y,t) & y <> t) & for x,y,z be Element of AS holds ex t be Element of AS st (x,y) // (z,t) & (x,z) // (y,t) by Th39;



       A2: for x,y,z,t be Element of AS st (z,x) // (x,t) & x <> z holds ex u be Element of AS st (y,x) // (x,u) & (y,z) // (t,u) by Th39;

      (for x,y,z,t,u,w be Element of AS holds (x,y) // (y,x) & (x,y) // (z,z) & (x <> y & (x,y) // (z,t) & (x,y) // (u,w) implies (z,t) // (u,w)) & ((x,y) // (x,z) implies (y,x) // (y,z))) & ex x,y,z be Element of AS st not (x,y) // (x,z) by Th39;

      hence thesis by A1, A2, Def6;

    end;

    theorem :: DIRAF:42

    (ex x,y be Element of AS st x <> y) & (for x,y,z,t,u,w be Element of AS holds (x,y) // (y,x) & (x,y) // (z,z) & (x <> y & (x,y) // (z,t) & (x,y) // (u,w) implies (z,t) // (u,w)) & ((x,y) // (x,z) implies (y,x) // (y,z))) & (ex x,y,z be Element of AS st not (x,y) // (x,z)) & (for x,y,z be Element of AS holds ex t be Element of AS st (x,z) // (y,t) & y <> t) & (for x,y,z be Element of AS holds ex t be Element of AS st (x,y) // (z,t) & (x,z) // (y,t)) & (for x,y,z,t be Element of AS st (z,x) // (x,t) & x <> z holds ex u be Element of AS st (y,x) // (x,u) & (y,z) // (t,u)) iff AS is AffinSpace by Def6, STRUCT_0:def 10;

    reserve S for OAffinPlane;

    reserve x,y,z,t,u for Element of S;

    theorem :: DIRAF:43



     Th43: not (x,y) '||' (z,t) implies ex u st (x,y) '||' (x,u) & (z,t) '||' (z,u)

    proof

      assume not (x,y) '||' (z,t);

      then ( not (x,y) // (z,t)) & not (x,y) // (t,z);

      then

      consider u such that

       A1: ((x,y) // (x,u) or (x,y) // (u,x)) & ((z,t) // (z,u) or (z,t) // (u,z)) by ANALOAF:def 6;

      (x,y) '||' (x,u) & (z,t) '||' (z,u) by A1;

      hence thesis;

    end;

    theorem :: DIRAF:44



     Th44: AS = ( Lambda S) implies for x,y,z,t be Element of AS st not (x,y) // (z,t) holds ex u be Element of AS st (x,y) // (x,u) & (z,t) // (z,u)

    proof

      assume

       A1: AS = ( Lambda S);

      let x,y,z,t be Element of AS;

      reconsider x9 = x, y9 = y, z9 = z, t9 = t as Element of S by A1;

      assume not (x,y) // (z,t);

      then not (x9,y9) '||' (z9,t9) by A1, Th38;

      then

      consider u9 be Element of S such that

       A2: (x9,y9) '||' (x9,u9) & (z9,t9) '||' (z9,u9) by Th43;

      reconsider u = u9 as Element of AS by A1;

      (x,y) // (x,u) & (z,t) // (z,u) by A1, A2, Th38;

      hence thesis;

    end;

    definition

      let IT be non empty AffinStruct;

      :: DIRAF:def7

      attr IT is 2-dimensional means

      : Def7: for x,y,z,t be Element of IT st not (x,y) // (z,t) holds ex u be Element of IT st (x,y) // (x,u) & (z,t) // (z,u);

    end

    registration

      cluster strict 2-dimensional for AffinSpace;

      existence

      proof

        set S = the OAffinPlane;

        reconsider AS = ( Lambda S) as AffinSpace by Th41;

        for x,y,z,t be Element of AS st not (x,y) // (z,t) holds ex u be Element of AS st (x,y) // (x,u) & (z,t) // (z,u) by Th44;

        then AS is 2-dimensional;

        hence thesis;

      end;

    end

    definition

      mode AffinPlane is 2-dimensional AffinSpace;

    end

    theorem :: DIRAF:45

    ( Lambda S) is AffinPlane

    proof

      set AS = ( Lambda S);

      for x,y,z,t be Element of AS st not (x,y) // (z,t) holds ex u be Element of AS st (x,y) // (x,u) & (z,t) // (z,u) by Th44;

      hence thesis by Def7, Th41;

    end;

    theorem :: DIRAF:46

    AS is AffinPlane iff (ex x,y be Element of AS st x <> y) & (for x,y,z,t,u,w be Element of AS holds (x,y) // (y,x) & (x,y) // (z,z) & (x <> y & (x,y) // (z,t) & (x,y) // (u,w) implies (z,t) // (u,w)) & ((x,y) // (x,z) implies (y,x) // (y,z))) & (ex x,y,z be Element of AS st not (x,y) // (x,z)) & (for x,y,z be Element of AS holds ex t be Element of AS st (x,z) // (y,t) & y <> t) & (for x,y,z be Element of AS holds ex t be Element of AS st (x,y) // (z,t) & (x,z) // (y,t)) & (for x,y,z,t be Element of AS st (z,x) // (x,t) & x <> z holds ex u be Element of AS st (y,x) // (x,u) & (y,z) // (t,u)) & for x,y,z,t be Element of AS st not (x,y) // (z,t) holds ex u be Element of AS st (x,y) // (x,u) & (z,t) // (z,u) by Def6, Def7, STRUCT_0:def 10;