papdesaf.miz



    begin

    registration

      let OAS be OAffinSpace;

      cluster ( Lambda OAS) -> AffinSpace-like non trivial;

      correctness by DIRAF: 41;

    end

    registration

      let OAS be OAffinPlane;

      cluster ( Lambda OAS) -> 2-dimensional;

      correctness by DIRAF: 45;

    end

    theorem :: PAPDESAF:1

    

     Th1: for OAS be OAffinSpace, x be set holds (x is Element of OAS iff x is Element of ( Lambda OAS)) & (x is Subset of OAS iff x is Subset of ( Lambda OAS))

    proof

      let OAS be OAffinSpace;

      ( Lambda OAS) = AffinStruct (# the carrier of OAS, ( lambda the CONGR of OAS) #) by DIRAF:def 2;

      hence thesis;

    end;

    theorem :: PAPDESAF:2

    

     Th2: for OAS be OAffinSpace holds for a,b,c be Element of OAS, a9,b9,c9 be Element of ( Lambda OAS) st a = a9 & b = b9 & c = c9 holds (a,b,c) are_collinear iff LIN (a9,b9,c9)

    proof

      let OAS be OAffinSpace;

      let a,b,c be Element of OAS, a9,b9,c9 be Element of ( Lambda OAS) such that

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

       A2:

      now

        assume (a,b,c) are_collinear ;

        then (a,b) '||' (a,c) by DIRAF:def 5;

        then (a9,b9) // (a9,c9) by A1, DIRAF: 38;

        hence LIN (a9,b9,c9) by AFF_1:def 1;

      end;

      now

        assume LIN (a9,b9,c9);

        then (a9,b9) // (a9,c9) by AFF_1:def 1;

        then (a,b) '||' (a,c) by A1, DIRAF: 38;

        hence (a,b,c) are_collinear by DIRAF:def 5;

      end;

      hence thesis by A2;

    end;

    theorem :: PAPDESAF:3

    

     Th3: for V be RealLinearSpace, x be set holds (x is Element of ( OASpace V) iff x is VECTOR of V)

    proof

      let V be RealLinearSpace, x be set;

      ( OASpace V) = AffinStruct (# the carrier of V, ( DirPar V) #) by ANALOAF:def 4;

      hence thesis;

    end;

    theorem :: PAPDESAF:4

    

     Th4: for V be RealLinearSpace, OAS be OAffinSpace st OAS = ( OASpace V) holds for a,b,c,d be Element of OAS, u,v,w,y be VECTOR of V st a = u & b = v & c = w & d = y holds ((a,b) '||' (c,d) iff (u,v) '||' (w,y))

    proof

      let V be RealLinearSpace, OAS be OAffinSpace such that

       A1: OAS = ( OASpace V);

      let a,b,c,d be Element of OAS, u,v,w,y be VECTOR of V;

      assume

       A2: a = u & b = v & c = w & d = y;

       A3:

      now

        assume (u,v) '||' (w,y);

        then (u,v) // (w,y) or (u,v) // (y,w) by GEOMTRAP:def 1;

        then (a,b) // (c,d) or (a,b) // (d,c) by A1, A2, GEOMTRAP: 2;

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

      end;

      now

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

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

        then (u,v) // (w,y) or (u,v) // (y,w) by A1, A2, GEOMTRAP: 2;

        hence (u,v) '||' (w,y) by GEOMTRAP:def 1;

      end;

      hence thesis by A3;

    end;

    theorem :: PAPDESAF:5

    for V be RealLinearSpace, OAS be OAffinSpace st OAS = ( OASpace V) holds ex u,v be VECTOR of V st for a,b be Real st ((a * u) + (b * v)) = ( 0. V) holds a = 0 & b = 0

    proof

      let V be RealLinearSpace, OAS be OAffinSpace such that

       A1: OAS = ( OASpace V);

      consider a,b,c,d be Element of OAS such that

       A2: ( not (a,b) // (c,d)) & not (a,b) // (d,c) by ANALOAF:def 5;

      reconsider u = a, v = b, w = c, y = d as VECTOR of V by A1, Th3;

      take z1 = (v - u), z2 = (y - w);

      now

        let r1,r2 be Real;

        assume ((r1 * z1) + (r2 * z2)) = ( 0. V);

        

        then

         A3: (r1 * z1) = ( - (r2 * z2)) by RLVECT_1: 6

        .= (r2 * ( - z2)) by RLVECT_1: 25

        .= (( - r2) * z2) by RLVECT_1: 24;

        assume r1 <> 0 or r2 <> 0 ;

        then r1 <> 0 or ( - r2) <> 0 ;

        then (u,v) // (w,y) or (u,v) // (y,w) by A3, ANALMETR: 14;

        hence r1 = 0 & r2 = 0 by A1, A2, GEOMTRAP: 2;

      end;

      hence thesis;

    end;

    definition

      let AS be AffinSpace;

      :: original: Fanoian

      redefine

      :: PAPDESAF:def1

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

      compatibility

      proof

        thus AS is Fanoian implies for a,b,c,d be Element of AS st (a,b) // (c,d) & (a,c) // (b,d) & (a,d) // (b,c) holds (a,b) // (a,c)

        proof

          assume

           A1: for a,b,c,d be Element of AS st (a,b) // (c,d) & (a,c) // (b,d) & (a,d) // (b,c) holds LIN (a,b,c);

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

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

          then LIN (a,b,c) by A1;

          hence thesis by AFF_1:def 1;

        end;

        assume

         A2: for a,b,c,d be Element of AS st (a,b) // (c,d) & (a,c) // (b,d) & (a,d) // (b,c) holds (a,b) // (a,c);

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

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

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

        hence thesis by AFF_1:def 1;

      end;

    end

    definition

      let IT be OAffinSpace;

      :: PAPDESAF:def2

      attr IT is Pappian means

      : Def2: ( Lambda IT) is Pappian;

      :: PAPDESAF:def3

      attr IT is Desarguesian means

      : Def3: ( Lambda IT) is Desarguesian;

      :: PAPDESAF:def4

      attr IT is Moufangian means

      : Def4: ( Lambda IT) is Moufangian;

      :: PAPDESAF:def5

      attr IT is translation means

      : Def5: ( Lambda IT) is translational;

    end

    definition

      let OAS be OAffinSpace;

      :: PAPDESAF:def6

      attr OAS is satisfying_DES means for o,a,b,c,a1,b1,c1 be Element of OAS st (o,a) // (o,a1) & (o,b) // (o,b1) & (o,c) // (o,c1) & not (o,a,b) are_collinear & not (o,a,c) are_collinear & (a,b) // (a1,b1) & (a,c) // (a1,c1) holds (b,c) // (b1,c1);

    end

    definition

      let OAS be OAffinSpace;

      :: PAPDESAF:def7

      attr OAS is satisfying_DES_1 means for o,a,b,c,a1,b1,c1 be Element of OAS st (a,o) // (o,a1) & (b,o) // (o,b1) & (c,o) // (o,c1) & not (o,a,b) are_collinear & not (o,a,c) are_collinear & (a,b) // (b1,a1) & (a,c) // (c1,a1) holds (b,c) // (c1,b1);

    end

    theorem :: PAPDESAF:6

    

     Th6: for OAS be OAffinSpace st OAS is satisfying_DES_1 holds OAS is satisfying_DES

    proof

      let OAS be OAffinSpace such that

       A1: OAS is satisfying_DES_1;

      for o,a,b,c,a1,b1,c1 be Element of OAS st (o,a) // (o,a1) & (o,b) // (o,b1) & (o,c) // (o,c1) & not (o,a,b) are_collinear & not (o,a,c) are_collinear & (a,b) // (a1,b1) & (a,c) // (a1,c1) holds (b,c) // (b1,c1)

      proof

        let o,a,b,c,a1,b1,c1 be Element of OAS such that

         A2: (o,a) // (o,a1) and

         A3: (o,b) // (o,b1) and

         A4: (o,c) // (o,c1) and

         A5: not (o,a,b) are_collinear and

         A6: not (o,a,c) are_collinear and

         A7: (a,b) // (a1,b1) and

         A8: (a,c) // (a1,c1);

        consider a2 be Element of OAS such that

         A9: Mid (a,o,a2) and

         A10: o <> a2 by DIRAF: 13;

        

         A11: (a,o) // (o,a2) by A9, DIRAF:def 3;

        

         A12: o <> a by A5, DIRAF: 31;

        then

        consider c2 be Element of OAS such that

         A13: (c,o) // (o,c2) and

         A14: (c,a) // (a2,c2) by A11, ANALOAF:def 5;

        

         A15: (c2,a2) // (a,c) by A14, DIRAF: 2;

        

         A16: (c2,o) // (o,c) by A13, DIRAF: 2;

        then Mid (c2,o,c) by DIRAF:def 3;

        then

         A17: (c2,o,c) are_collinear by DIRAF: 28;

        (a,o,a2) are_collinear by A9, DIRAF: 28;

        then

         A18: (o,a2,a) are_collinear by DIRAF: 30;

        

         A19: o <> c2

        proof

          assume o = c2;

          then (o,a2) // (a,c) by A14, DIRAF: 2;

          then (o,a2) '||' (a,c) by DIRAF:def 4;

          then (o,a2,o) are_collinear & (o,a2,c) are_collinear by A10, A18, DIRAF: 31, DIRAF: 33;

          hence contradiction by A6, A10, A18, DIRAF: 32;

        end;

        

         A20: not (o,a2,c2) are_collinear

        proof

          

           A21: (c2,o,o) are_collinear by DIRAF: 31;

          

           A22: (o,a2,o) are_collinear by DIRAF: 31;

          assume (o,a2,c2) are_collinear ;

          then (c2,o,a) are_collinear by A10, A18, A22, DIRAF: 32;

          hence contradiction by A6, A17, A19, A21, DIRAF: 32;

        end;

        consider b2 be Element of OAS such that

         A23: (b,o) // (o,b2) and

         A24: (b,a) // (a2,b2) by A12, A11, ANALOAF:def 5;

        

         A25: (b2,a2) // (a,b) by A24, DIRAF: 2;

        a <> b by A5, DIRAF: 31;

        then (b2,a2) // (a1,b1) by A7, A25, DIRAF: 3;

        then

         A26: (a2,b2) // (b1,a1) by DIRAF: 2;

        o <> c by A6, DIRAF: 31;

        then

         A27: (c2,o) // (o,c1) by A4, A16, DIRAF: 3;

        

         A28: (a,c) // (c2,a2) by A14, ANALOAF:def 5;

        

         A29: (b2,o) // (o,b) by A23, DIRAF: 2;

        then Mid (b2,o,b) by DIRAF:def 3;

        then

         A30: (b2,o,b) are_collinear by DIRAF: 28;

        

         A31: o <> b2

        proof

          assume o = b2;

          then (o,a2) // (a,b) by A24, DIRAF: 2;

          then (o,a2) '||' (a,b) by DIRAF:def 4;

          then (o,a2,o) are_collinear & (o,a2,b) are_collinear by A10, A18, DIRAF: 31, DIRAF: 33;

          hence contradiction by A5, A10, A18, DIRAF: 32;

        end;

        

         A32: not (o,a2,b2) are_collinear

        proof

          

           A33: (b2,o,o) are_collinear by DIRAF: 31;

          

           A34: (o,a2,o) are_collinear by DIRAF: 31;

          assume (o,a2,b2) are_collinear ;

          then (b2,o,a) are_collinear by A10, A18, A34, DIRAF: 32;

          hence contradiction by A5, A30, A31, A33, DIRAF: 32;

        end;

         A35:

        now

          (b2,a2) // (a,b) by A24, DIRAF: 2;

          then

           A36: (b2,a2) '||' (a,b) by DIRAF:def 4;

          assume

           A37: c2 = b2;

          then

           A38: (o,b2,c) are_collinear by A17, DIRAF: 30;

          (c2,a2) // (a,c) by A14, DIRAF: 2;

          then

           A39: (b2,a2) '||' (a,c) by A37, DIRAF:def 4;

          ( not (o,b2,a2) are_collinear ) & (o,b2,b) are_collinear by A30, A32, DIRAF: 30;

          then b = c by A18, A38, A36, A39, PASCH: 4;

          hence thesis by DIRAF: 4;

        end;

        (a2,o) // (o,a) by A11, DIRAF: 2;

        then

         A40: (a2,o) // (o,a1) by A2, A12, DIRAF: 3;

        a <> c by A6, DIRAF: 31;

        then (c2,a2) // (a1,c1) by A8, A15, DIRAF: 3;

        then

         A41: (a2,c2) // (c1,a1) by DIRAF: 2;

        o <> b by A5, DIRAF: 31;

        then (b2,o) // (o,b1) by A3, A29, DIRAF: 3;

        then

         A42: (c2,b2) // (b1,c1) by A1, A40, A27, A41, A26, A32, A20;

        (a,b) // (b2,a2) by A24, ANALOAF:def 5;

        then (b,c) // (c2,b2) by A1, A5, A6, A11, A23, A13, A28;

        hence thesis by A42, A35, DIRAF: 3;

      end;

      hence thesis;

    end;

    theorem :: PAPDESAF:7

    

     Th7: for OAS be OAffinSpace holds for o,a,b,a9,b9 be Element of OAS st not (o,a,b) are_collinear & (a,o) // (o,a9) & (o,b,b9) are_collinear & (a,b) '||' (a9,b9) holds (b,o) // (o,b9) & (a,b) // (b9,a9)

    proof

      let OAS be OAffinSpace;

      let o,a,b,a9,b9 be Element of OAS such that

       A1: not (o,a,b) are_collinear and

       A2: (a,o) // (o,a9) and

       A3: (o,b,b9) are_collinear and

       A4: (a,b) '||' (a9,b9);

       Mid (a,o,a9) & (a,b) '||' (b9,a9) by A2, A4, DIRAF: 22, DIRAF:def 3;

      then Mid (b,o,b9) by A1, A3, PASCH: 6;

      hence (b,o) // (o,b9) by DIRAF:def 3;

      hence thesis by A1, A2, A4, PASCH: 12;

    end;

    theorem :: PAPDESAF:8

    

     Th8: for OAS be OAffinSpace holds for o,a,b,a9,b9 be Element of OAS st not (o,a,b) are_collinear & (o,a) // (o,a9) & (o,b,b9) are_collinear & (a,b) '||' (a9,b9) holds (o,b) // (o,b9) & (a,b) // (a9,b9)

    proof

      let OAS be OAffinSpace;

      let o,a,b,a9,b9 be Element of OAS such that

       A1: not (o,a,b) are_collinear and

       A2: (o,a) // (o,a9) and

       A3: (o,b,b9) are_collinear and

       A4: (a,b) '||' (a9,b9);

      

       A5: o <> a by A1, DIRAF: 31;

      consider a2 be Element of OAS such that

       A6: Mid (a,o,a2) and

       A7: o <> a2 by DIRAF: 13;

      (a,o) // (o,a2) by A6, DIRAF:def 3;

      then

      consider b2 be Element of OAS such that

       A8: (b,o) // (o,b2) and

       A9: (b,a) // (a2,b2) by A5, ANALOAF:def 5;

      

       A10: (o,b) // (b2,o) by A8, DIRAF: 2;

      (a,o) // (o,a2) by A6, DIRAF:def 3;

      then (a2,o) // (o,a) by DIRAF: 2;

      then

       A11: (a2,o) // (o,a9) by A2, A5, DIRAF: 3;

      (a,o,a2) are_collinear by A6, DIRAF: 28;

      then

       A12: (o,a2,a) are_collinear by DIRAF: 30;

      

       A13: o <> b2

      proof

        assume o = b2;

        then (o,a2) // (a,b) by A9, DIRAF: 2;

        then (o,a2) '||' (a,b) by DIRAF:def 4;

        then (o,a2,o) are_collinear & (o,a2,b) are_collinear by A7, A12, DIRAF: 31, DIRAF: 33;

        hence contradiction by A1, A7, A12, DIRAF: 32;

      end;

       Mid (b,o,b2) by A8, DIRAF:def 3;

      then (b,o,b2) are_collinear by DIRAF: 28;

      then

       A14: (b2,o,b) are_collinear by DIRAF: 30;

      

       A15: not (o,a2,b2) are_collinear

      proof

        

         A16: (b2,o,o) are_collinear by DIRAF: 31;

        

         A17: (o,a2,o) are_collinear by DIRAF: 31;

        assume (o,a2,b2) are_collinear ;

        then (b2,o,a) are_collinear by A7, A12, A17, DIRAF: 32;

        hence contradiction by A1, A14, A13, A16, DIRAF: 32;

      end;

      (a2,b2) // (b,a) by A9, DIRAF: 2;

      then

       A18: (a2,b2) '||' (a,b) by DIRAF:def 4;

      b <> a by A1, DIRAF: 31;

      then

       A19: (a2,b2) '||' (a9,b9) by A4, A18, DIRAF: 23;

      

       A20: (a,b) // (b2,a2) by A9, DIRAF: 2;

       Mid (b,o,b2) by A8, DIRAF:def 3;

      then (b,o,b2) are_collinear by DIRAF: 28;

      then

       A21: (o,b,b2) are_collinear by DIRAF: 30;

      

       A22: (o,b,o) are_collinear by DIRAF: 31;

      o <> b by A1, DIRAF: 31;

      then

       A23: (o,b2,b9) are_collinear by A3, A21, A22, DIRAF: 32;

      then (a2,b2) // (b9,a9) by A15, A11, A19, Th7;

      then

       A24: (b2,a2) // (a9,b9) by DIRAF: 2;

      (b2,o) // (o,b9) by A15, A11, A19, A23, Th7;

      hence (o,b) // (o,b9) by A13, A10, DIRAF: 3;

      a2 <> b2 by A15, DIRAF: 31;

      hence thesis by A20, A24, DIRAF: 3;

    end;

    theorem :: PAPDESAF:9

    

     Th9: for OAP be OAffinSpace st OAP is satisfying_DES_1 holds ( Lambda OAP) is Desarguesian

    proof

      let OAP be OAffinSpace;

      set AP = ( Lambda OAP);

      assume

       A1: OAP is satisfying_DES_1;

      then

       A2: OAP is satisfying_DES by Th6;

      for A,P,C be Subset of AP, o,a,b,c,a9,b9,c9 be Element of AP st o in A & o in P & o in C & o <> a & o <> b & o <> c & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & (a,b) // (a9,b9) & (a,c) // (a9,c9) holds (b,c) // (b9,c9)

      proof

        let A,P,C be Subset of AP;

        let o,a,b,c,a9,b9,c9 be Element of AP;

        reconsider o1 = o, a1 = a, b1 = b, c1 = c, a19 = a9, b19 = b9, c19 = c9 as Element of OAP by Th1;

        assume that

         A3: o in A and

         A4: o in P and

         A5: o in C and

         A6: o <> a and

         A7: o <> b and

         A8: o <> c and

         A9: a in A and

         A10: a9 in A and

         A11: b in P and

         A12: b9 in P and

         A13: c in C and

         A14: c9 in C and

         A15: A is being_line and

         A16: P is being_line and

         A17: C is being_line and

         A18: A <> P and

         A19: A <> C and

         A20: (a,b) // (a9,b9) & (a,c) // (a9,c9);

         LIN (o,b,b9) by A4, A11, A12, A16, AFF_1: 21;

        then

         A21: (o1,b1,b19) are_collinear by Th2;

        

         A22: not (o1,a1,b1) are_collinear & not (o1,a1,c1) are_collinear

        proof

           A23:

          now

            assume LIN (o,a,c);

            then

            consider X be Subset of ( Lambda OAP) such that

             A24: X is being_line & o in X and

             A25: a in X and

             A26: c in X by AFF_1: 21;

            X = C by A5, A8, A13, A17, A24, A26, AFF_1: 18;

            hence contradiction by A3, A6, A9, A15, A19, A24, A25, AFF_1: 18;

          end;

           A27:

          now

            assume LIN (o,a,b);

            then

            consider X be Subset of ( Lambda OAP) such that

             A28: X is being_line & o in X and

             A29: a in X and

             A30: b in X by AFF_1: 21;

            X = P by A4, A7, A11, A16, A28, A30, AFF_1: 18;

            hence contradiction by A3, A6, A9, A15, A18, A28, A29, AFF_1: 18;

          end;

          assume not thesis;

          hence contradiction by A27, A23, Th2;

        end;

         LIN (o,c,c9) by A5, A13, A14, A17, AFF_1: 21;

        then

         A31: (o1,c1,c19) are_collinear by Th2;

        

         A32: (a1,b1) '||' (a19,b19) & (a1,c1) '||' (a19,c19) by A20, DIRAF: 38;

         A33:

        now

          assume

           A34: (a1,o1) // (o1,a19);

          then

           A35: (a1,b1) // (b19,a19) & (a1,c1) // (c19,a19) by A21, A31, A22, A32, Th7;

          (b1,o1) // (o1,b19) & (c1,o1) // (o1,c19) by A21, A31, A22, A32, A34, Th7;

          then (b1,c1) // (c19,b19) by A1, A22, A34, A35;

          then (b1,c1) '||' (b19,c19) by DIRAF:def 4;

          hence thesis by DIRAF: 38;

        end;

         A36:

        now

          assume

           A37: (o1,a1) // (o1,a19);

          then

           A38: (a1,b1) // (a19,b19) & (a1,c1) // (a19,c19) by A21, A31, A22, A32, Th8;

          (o1,b1) // (o1,b19) & (o1,c1) // (o1,c19) by A21, A31, A22, A32, A37, Th8;

          then (b1,c1) // (b19,c19) by A2, A22, A37, A38;

          then (b1,c1) '||' (b19,c19) by DIRAF:def 4;

          hence thesis by DIRAF: 38;

        end;

         LIN (o,a,a9) by A3, A9, A10, A15, AFF_1: 21;

        then (o1,a1,a19) are_collinear by Th2;

        then Mid (o1,a1,a19) or Mid (a1,o1,a19) or Mid (o1,a19,a1) by DIRAF: 29;

        hence thesis by A33, A36, DIRAF: 7, DIRAF:def 3;

      end;

      hence thesis by AFF_2:def 4;

    end;

    theorem :: PAPDESAF:10

    

     Th10: for V be RealLinearSpace holds for o,u,v,u1,v1 be VECTOR of V, r be Real st (o - u) = (r * (u1 - o)) & r <> 0 & (o,v) '||' (o,v1) & not (o,u) '||' (o,v) & (u,v) '||' (u1,v1) holds v1 = (u1 + ((( - r) " ) * (v - u))) & v1 = (o + ((( - r) " ) * (v - o))) & (v - u) = (( - r) * (v1 - u1))

    proof

      let V be RealLinearSpace;

      let o,u,v,u1,v1 be VECTOR of V, r be Real such that

       A1: (o - u) = (r * (u1 - o)) and

       A2: r <> 0 and

       A3: (o,v) '||' (o,v1) and

       A4: not (o,u) '||' (o,v) and

       A5: (u,v) '||' (u1,v1);

      

       A6: ( - r) <> 0 by A2;

      for r1,r2 be Real st ((r1 * (u - o)) + (r2 * (v - o))) = ( 0. V) holds r1 = 0 & r2 = 0

      proof

        let r1,r2 be Real;

        assume ((r1 * (u - o)) + (r2 * (v - o))) = ( 0. V);

        

        then

         A7: (r1 * (u - o)) = ( - (r2 * (v - o))) by RLVECT_1: 6

        .= (r2 * ( - (v - o))) by RLVECT_1: 25

        .= (( - r2) * (v - o)) by RLVECT_1: 24;

        assume r1 <> 0 or r2 <> 0 ;

        then r1 <> 0 or ( - r2) <> 0 ;

        then (o,u) // (o,v) or (o,u) // (v,o) by A7, ANALMETR: 14;

        hence contradiction by A4, GEOMTRAP:def 1;

      end;

      then

      reconsider X = ( OASpace V) as OAffinSpace by ANALOAF: 26;

      set w = (u1 + ((( - r) " ) * (v - u)));

      reconsider p = o, a = u, a1 = u1, b = v, b1 = v1, q = w as Element of X by Th3;

      (a,b) '||' (a1,b1) by A5, Th4;

      then

       A8: (b,a) '||' (a1,b1) by DIRAF: 22;

      (p,b) '||' (p,b1) by A3, Th4;

      then

       A9: (p,b,b1) are_collinear by DIRAF:def 5;

      

       A10: (( - r) * (w - u1)) = (( - r) * ((( - r) " ) * (v - u))) by RLSUB_2: 61

      .= ((( - r) * (( - r) " )) * (v - u)) by RLVECT_1:def 7

      .= (1 * (v - u)) by A6, XCMPLX_0:def 7;

      then

       A11: (v - u) = (( - r) * (w - u1)) by RLVECT_1:def 8;

      (u,v) // (u1,w) or (u,v) // (w,u1) by A10, ANALMETR: 14;

      then (u,v) '||' (u1,w) by GEOMTRAP:def 1;

      then (a,b) '||' (a1,q) by Th4;

      then

       A12: (b,a) '||' (a1,q) by DIRAF: 22;

      

       A13: (( - r) * (o - w)) = ((( - r) * o) - (( - r) * w)) by RLVECT_1: 34

      .= ((( - r) * o) - ((( - r) * u1) + (( - r) * ((( - r) " ) * (v - u))))) by RLVECT_1:def 5

      .= ((( - r) * o) - ((( - r) * u1) + ((( - r) * (( - r) " )) * (v - u)))) by RLVECT_1:def 7

      .= ((( - r) * o) - ((( - r) * u1) + (1 * (v - u)))) by A6, XCMPLX_0:def 7

      .= ((( - r) * o) - ((( - r) * u1) + (v - u))) by RLVECT_1:def 8

      .= (((( - r) * o) - (( - r) * u1)) - (v - u)) by RLVECT_1: 27

      .= ((( - r) * (o - u1)) - (v - u)) by RLVECT_1: 34

      .= ((r * ( - (o - u1))) - (v - u)) by RLVECT_1: 24

      .= ((o - u) - (v - u)) by A1, RLVECT_1: 33

      .= (o - ((v - u) + u)) by RLVECT_1: 27

      .= (o - v) by RLSUB_2: 61

      .= (1 * (o - v)) by RLVECT_1:def 8;

      then (v,o) // (w,o) or (v,o) // (o,w) by ANALMETR: 14;

      then (o,v) // (w,o) or (o,v) // (o,w) by ANALOAF: 12;

      then (o,v) '||' (o,w) by GEOMTRAP:def 1;

      then (p,b) '||' (p,q) by Th4;

      then

       A14: (p,b,q) are_collinear by DIRAF:def 5;

      (1 * (u - o)) = (( - 1) * ( - (u - o))) by RLVECT_1: 26

      .= (( - 1) * (r * (u1 - o))) by A1, RLVECT_1: 33

      .= ((( - 1) * r) * (u1 - o)) by RLVECT_1:def 7

      .= (( - r) * (u1 - o));

      then (o,u) // (o,u1) or (o,u) // (u1,o) by ANALMETR: 14;

      then (o,u) '||' (o,u1) by GEOMTRAP:def 1;

      then (p,a) '||' (p,a1) by Th4;

      then

       A15: (p,a,a1) are_collinear by DIRAF:def 5;

      

       A16: not (p,b,a) are_collinear

      proof

        assume (p,b,a) are_collinear ;

        then (p,b) '||' (p,a) by DIRAF:def 5;

        then (p,a) '||' (p,b) by DIRAF: 22;

        hence contradiction by A4, Th4;

      end;

      

       A17: (( - r) * (w - o)) = (r * ( - (w - o))) by RLVECT_1: 24

      .= (r * (o - w)) by RLVECT_1: 33

      .= ( - ( - (r * (o - w)))) by RLVECT_1: 17

      .= ( - (r * ( - (o - w)))) by RLVECT_1: 25

      .= ( - (1 * (o - v))) by A13, RLVECT_1: 24

      .= ( - (o - v)) by RLVECT_1:def 8

      .= (v - o) by RLVECT_1: 33;

      w = (o + (w - o)) by RLSUB_2: 61

      .= (o + ((( - r) " ) * (v - o))) by A6, A17, ANALOAF: 6;

      hence thesis by A11, A16, A9, A14, A15, A12, A8, PASCH: 4;

    end;

    

     Lm1: for V be RealLinearSpace holds for u,v,w be VECTOR of V st u <> v & w <> v & (u,v) // (v,w) holds ex r be Real st (v - u) = (r * (w - v)) & 0 < r

    proof

      let V be RealLinearSpace;

      let u,v,w be VECTOR of V;

      assume u <> v & w <> v & (u,v) // (v,w);

      then

      consider a,b be Real such that

       A1: (a * (v - u)) = (b * (w - v)) and

       A2: 0 < a and

       A3: 0 < b by ANALOAF: 7;

      take r = ((a " ) * b);

       0 < (a " ) by A2, XREAL_1: 122;

      then

       A4: ( 0 * b) < r by A3, XREAL_1: 68;

      (v - u) = (1 * (v - u)) by RLVECT_1:def 8

      .= (((a " ) * a) * (v - u)) by A2, XCMPLX_0:def 7

      .= ((a " ) * (b * (w - v))) by A1, RLVECT_1:def 7

      .= (r * (w - v)) by RLVECT_1:def 7;

      hence thesis by A4;

    end;

    theorem :: PAPDESAF:11

    

     Th11: for V be RealLinearSpace, OAS be OAffinSpace st OAS = ( OASpace V) holds OAS is satisfying_DES_1

    proof

      let V be RealLinearSpace, OAS be OAffinSpace such that

       A1: OAS = ( OASpace V);

      for o,a,b,c,a1,b1,c1 be Element of OAS st (a,o) // (o,a1) & (b,o) // (o,b1) & (c,o) // (o,c1) & not (o,a,b) are_collinear & not (o,a,c) are_collinear & (a,b) // (b1,a1) & (a,c) // (c1,a1) holds (b,c) // (c1,b1)

      proof

        let o,a,b,c,a1,b1,c1 be Element of OAS such that

         A2: (a,o) // (o,a1) and

         A3: (b,o) // (o,b1) and

         A4: (c,o) // (o,c1) and

         A5: not (o,a,b) are_collinear and

         A6: not (o,a,c) are_collinear and

         A7: (a,b) // (b1,a1) and

         A8: (a,c) // (c1,a1);

        reconsider y = o, u = a, v = b, w = c, u1 = a1, v1 = b1, w1 = c1 as VECTOR of V by A1, Th3;

        

         A9: o <> a by A5, DIRAF: 31;

         A10:

        now

          

           A11: not (y,u) '||' (y,v) & not (y,u) '||' (y,w)

          proof

            assume not thesis;

            then (y,u) // (y,v) or (y,u) // (v,y) or (y,u) // (y,w) or (y,u) // (w,y) by GEOMTRAP:def 1;

            then (o,a) // (o,b) or (o,a) // (b,o) or (o,a) // (o,c) or (o,a) // (c,o) by A1, GEOMTRAP: 2;

            then (o,a) '||' (o,b) or (o,a) '||' (o,c) by DIRAF:def 4;

            hence contradiction by A5, A6, DIRAF:def 5;

          end;

          (o,c) // (c1,o) by A4, DIRAF: 2;

          then (y,w) // (w1,y) by A1, GEOMTRAP: 2;

          then

           A12: (y,w) '||' (y,w1) by GEOMTRAP:def 1;

          (o,b) // (b1,o) by A3, DIRAF: 2;

          then (y,v) // (v1,y) by A1, GEOMTRAP: 2;

          then

           A13: (y,v) '||' (y,v1) by GEOMTRAP:def 1;

          assume

           A14: o <> a1;

          (u,y) // (y,u1) by A1, A2, GEOMTRAP: 2;

          then

          consider r be Real such that

           A15: (y - u) = (r * (u1 - y)) and

           A16: 0 < r by A9, A14, Lm1;

          (u,w) // (w1,u1) by A1, A8, GEOMTRAP: 2;

          then (u,w) '||' (u1,w1) by GEOMTRAP:def 1;

          then

           A17: w1 = (u1 + ((( - r) " ) * (w - u))) by A15, A16, A12, A11, Th10;

          (u,v) // (v1,u1) by A1, A7, GEOMTRAP: 2;

          then (u,v) '||' (u1,v1) by GEOMTRAP:def 1;

          then v1 = (u1 + ((( - r) " ) * (v - u))) by A15, A16, A13, A11, Th10;

          

          then

           A18: (1 * (w1 - v1)) = ((u1 + ((( - r) " ) * (w - u))) - (u1 + ((( - r) " ) * (v - u)))) by A17, RLVECT_1:def 8

          .= (((((( - r) " ) * (w - u)) + u1) - u1) - ((( - r) " ) * (v - u))) by RLVECT_1: 27

          .= (((( - r) " ) * (w - u)) - ((( - r) " ) * (v - u))) by RLSUB_2: 61

          .= ((( - r) " ) * ((w - u) - (v - u))) by RLVECT_1: 34

          .= ((( - r) " ) * (w - ((v - u) + u))) by RLVECT_1: 27

          .= ((( - r) " ) * (w - v)) by RLSUB_2: 61

          .= (( - (r " )) * (w - v)) by XCMPLX_1: 222

          .= ((r " ) * ( - (w - v))) by RLVECT_1: 24

          .= ((r " ) * (v - w)) by RLVECT_1: 33;

           0 < (r " ) by A16, XREAL_1: 122;

          then (w,v) // (v1,w1) by A18, ANALOAF:def 1;

          then (c,b) // (b1,c1) by A1, GEOMTRAP: 2;

          hence thesis by DIRAF: 2;

        end;

        now

          assume

           A19: o = a1;

          

           A20: o = c1

          proof

            (c,o) '||' (o,c1) by A4, DIRAF:def 4;

            then (o,c1) '||' (o,c) by DIRAF: 22;

            then

             A21: (o,c1,c) are_collinear by DIRAF:def 5;

            

             A22: (o,c1,o) are_collinear by DIRAF: 31;

            assume

             A23: o <> c1;

            (a,c) '||' (c1,o) by A8, A19, DIRAF:def 4;

            then (o,c1) '||' (c,a) by DIRAF: 22;

            then (o,c1,a) are_collinear by A23, A21, DIRAF: 33;

            hence contradiction by A6, A23, A21, A22, DIRAF: 32;

          end;

          o = b1

          proof

            (b,o) '||' (o,b1) by A3, DIRAF:def 4;

            then (o,b1) '||' (o,b) by DIRAF: 22;

            then

             A24: (o,b1,b) are_collinear by DIRAF:def 5;

            

             A25: (o,b1,o) are_collinear by DIRAF: 31;

            assume

             A26: o <> b1;

            (a,b) '||' (b1,o) by A7, A19, DIRAF:def 4;

            then (o,b1) '||' (b,a) by DIRAF: 22;

            then (o,b1,a) are_collinear by A26, A24, DIRAF: 33;

            hence contradiction by A5, A26, A24, A25, DIRAF: 32;

          end;

          hence thesis by A20, DIRAF: 4;

        end;

        hence thesis by A10;

      end;

      hence thesis;

    end;

    theorem :: PAPDESAF:12

    for V be RealLinearSpace, OAS be OAffinSpace st OAS = ( OASpace V) holds OAS is satisfying_DES_1 & OAS is satisfying_DES by Th6, Th11;

    

     Lm2: for V be RealLinearSpace holds for y,u,v be VECTOR of V st (y,u) '||' (y,v) & y <> u & y <> v holds ex r be Real st (u - y) = (r * (v - y)) & r <> 0

    proof

      let V be RealLinearSpace;

      let y,u,v be VECTOR of V such that

       A1: (y,u) '||' (y,v) and

       A2: y <> u and

       A3: y <> v;

      (y,u) // (y,v) or (y,u) // (v,y) by A1, GEOMTRAP:def 1;

      then

      consider a,b be Real such that

       A4: (a * (u - y)) = (b * (v - y)) and

       A5: a <> 0 or b <> 0 by ANALMETR: 14;

       A6:

      now

        assume

         A7: b = 0 ;

        then ( 0. V) = (a * (u - y)) by A4, RLVECT_1: 10;

        then (u - y) = ( 0. V) by A5, A7, RLVECT_1: 11;

        hence contradiction by A2, RLVECT_1: 21;

      end;

       A8:

      now

        assume

         A9: a = 0 ;

        then ( 0. V) = (b * (v - y)) by A4, RLVECT_1: 10;

        then (v - y) = ( 0. V) by A5, A9, RLVECT_1: 11;

        hence contradiction by A3, RLVECT_1: 21;

      end;

      then

       A10: (a " ) <> 0 by XCMPLX_1: 202;

      take r = ((a " ) * b);

      (r * (v - y)) = ((a " ) * (a * (u - y))) by A4, RLVECT_1:def 7

      .= (((a " ) * a) * (u - y)) by RLVECT_1:def 7

      .= (1 * (u - y)) by A8, XCMPLX_0:def 7

      .= (u - y) by RLVECT_1:def 8;

      hence thesis by A6, A10, XCMPLX_1: 6;

    end;

    

     Lm3: for V be RealLinearSpace holds for u,v,y be VECTOR of V holds ((u - y) - (v - y)) = (u - v)

    proof

      let V be RealLinearSpace;

      let u,v,y be VECTOR of V;

      

      thus ((u - y) - (v - y)) = (u - ((v - y) + y)) by RLVECT_1: 27

      .= (u - v) by RLSUB_2: 61;

    end;

    theorem :: PAPDESAF:13

    

     Th13: for V be RealLinearSpace, OAS be OAffinSpace st OAS = ( OASpace V) holds ( Lambda OAS) is Pappian

    proof

      let V be RealLinearSpace, OAS be OAffinSpace such that

       A1: OAS = ( OASpace V);

      set AS = ( Lambda OAS);

      for M,N be Subset of AS, o,a,b,c,a9,b9,c9 be Element of AS st M is being_line & N is being_line & M <> N & o in M & o in N & o <> a & o <> a9 & o <> b & o <> b9 & o <> c & o <> c9 & a in M & b in M & c in M & a9 in N & b9 in N & c9 in N & (a,b9) // (b,a9) & (b,c9) // (c,b9) holds (a,c9) // (c,a9)

      proof

        let M,N be Subset of AS, o,a,b,c,a9,b9,c9 be Element of AS such that

         A2: M is being_line and

         A3: N is being_line and

         A4: M <> N and

         A5: o in M and

         A6: o in N and

         A7: o <> a and

         A8: o <> a9 and

         A9: o <> b and o <> b9 and

         A10: o <> c and

         A11: o <> c9 and

         A12: a in M and

         A13: b in M and

         A14: c in M and

         A15: a9 in N and

         A16: b9 in N and

         A17: c9 in N and

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

         A19: (b,c9) // (c,b9);

        reconsider o1 = o, a1 = a, b1 = b, c1 = c, a19 = a9, b19 = b9, c19 = c9 as Element of OAS by Th1;

        reconsider q = o1, u = a1, v = b1, w = c1, u9 = a19, v9 = b19, w9 = c19 as VECTOR of V by A1, Th3;

        (b1,c19) '||' (c1,b19) by A19, DIRAF: 38;

        then

         A20: (v,w9) '||' (w,v9) by A1, Th4;

        

         A21: not (q,v) '||' (q,w9) & not (q,v) '||' (q,u9)

        proof

          assume not thesis;

          then (o1,b1) '||' (o1,c19) or (o1,b1) '||' (o1,a19) by A1, Th4;

          then (o,b) // (o,c9) or (o,b) // (o,a9) by DIRAF: 38;

          then LIN (o,b,c9) or LIN (o,b,a9) by AFF_1:def 1;

          then c9 in M or a9 in M by A2, A5, A9, A13, AFF_1: 25;

          hence contradiction by A2, A3, A4, A5, A6, A8, A11, A15, A17, AFF_1: 18;

        end;

         LIN (o,c,b) by A2, A5, A13, A14, AFF_1: 21;

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

        then (o1,c1) '||' (o1,b1) by DIRAF: 38;

        then (q,w) '||' (q,v) by A1, Th4;

        then

        consider r2 be Real such that

         A22: (w - q) = (r2 * (v - q)) and

         A23: r2 <> 0 by A9, A10, Lm2;

        

         A24: ( - r2) <> 0 by A23;

         LIN (o,a,b) by A2, A5, A12, A13, AFF_1: 21;

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

        then (o1,a1) '||' (o1,b1) by DIRAF: 38;

        then (q,u) '||' (q,v) by A1, Th4;

        then

        consider r1 be Real such that

         A25: (u - q) = (r1 * (v - q)) and

         A26: r1 <> 0 by A7, A9, Lm2;

        

         A27: (( - r1) * (q - v)) = (r1 * ( - (q - v))) by RLVECT_1: 24

        .= (u - q) by A25, RLVECT_1: 33;

         LIN (o,c9,b9) by A3, A6, A16, A17, AFF_1: 21;

        then (o,c9) // (o,b9) by AFF_1:def 1;

        then (o1,c19) '||' (o1,b19) by DIRAF: 38;

        then

         A28: (q,w9) '||' (q,v9) by A1, Th4;

        (( - r2) * (q - v)) = (r2 * ( - (q - v))) by RLVECT_1: 24

        .= (w - q) by A22, RLVECT_1: 33;

        then

         A29: (q - v) = ((( - r2) " ) * (w - q)) by A24, ANALOAF: 5;

        (( - r2) " ) <> 0 by A24, XCMPLX_1: 202;

        

        then v9 = (q + ((( - (( - r2) " )) " ) * (w9 - q))) by A20, A29, A28, A21, Th10

        .= (q + ((( - ( - (r2 " ))) " ) * (w9 - q))) by XCMPLX_1: 222

        .= (q + (r2 * (w9 - q)));

        then

         A30: (v9 - q) = (r2 * (w9 - q)) by RLSUB_2: 61;

         LIN (o,a9,b9) by A3, A6, A15, A16, AFF_1: 21;

        then (o,a9) // (o,b9) by AFF_1:def 1;

        then (o1,a19) '||' (o1,b19) by DIRAF: 38;

        then

         A31: (q,u9) '||' (q,v9) by A1, Th4;

        (a1,b19) '||' (b1,a19) by A18, DIRAF: 38;

        then (b1,a19) '||' (a1,b19) by DIRAF: 22;

        then

         A32: (v,u9) '||' (u,v9) by A1, Th4;

        (r1 " ) <> 0 by A26, XCMPLX_1: 202;

        then

         A33: ((r1 " ) * r2) <> 0 by A23, XCMPLX_1: 6;

        set s = (r1 * (r2 " ));

        

         A34: (u - q) = (r1 * ((r2 " ) * (w - q))) by A25, A22, A23, ANALOAF: 6

        .= (s * (w - q)) by RLVECT_1:def 7;

        ( - r1) <> 0 by A26;

        then

         A35: (( - r1) " ) <> 0 by XCMPLX_1: 202;

        ( - r1) <> 0 by A26;

        then (q - v) = ((( - r1) " ) * (u - q)) by A27, ANALOAF: 6;

        

        then v9 = (q + ((( - (( - r1) " )) " ) * (u9 - q))) by A32, A35, A31, A21, Th10

        .= (q + ((( - ( - (r1 " ))) " ) * (u9 - q))) by XCMPLX_1: 222

        .= (q + (r1 * (u9 - q)));

        then (v9 - q) = (r1 * (u9 - q)) by RLSUB_2: 61;

        

        then (u9 - q) = ((r1 " ) * (r2 * (w9 - q))) by A26, A30, ANALOAF: 6

        .= (((r1 " ) * r2) * (w9 - q)) by RLVECT_1:def 7;

        

        then

         A36: (w9 - q) = ((((r1 " ) * r2) " ) * (u9 - q)) by A33, ANALOAF: 6

        .= ((((r1 " ) " ) * (r2 " )) * (u9 - q)) by XCMPLX_1: 204

        .= (s * (u9 - q));

        (1 * (w9 - u)) = (w9 - u) by RLVECT_1:def 8

        .= ((s * (u9 - q)) - (s * (w - q))) by A36, A34, Lm3

        .= (s * ((u9 - q) - (w - q))) by RLVECT_1: 34

        .= (s * (u9 - w)) by Lm3;

        then (u,w9) // (w,u9) or (u,w9) // (u9,w) by ANALMETR: 14;

        then (u,w9) '||' (w,u9) by GEOMTRAP:def 1;

        then (a1,c19) '||' (c1,a19) by A1, Th4;

        hence thesis by DIRAF: 38;

      end;

      hence thesis by AFF_2:def 2;

    end;

    theorem :: PAPDESAF:14

    

     Th14: for V be RealLinearSpace, OAS be OAffinSpace st OAS = ( OASpace V) holds ( Lambda OAS) is Desarguesian by Th9, Th11;

    theorem :: PAPDESAF:15

    

     Th15: for AS be AffinSpace st AS is Desarguesian holds AS is Moufangian

    proof

      let AS be AffinSpace such that

       A1: AS is Desarguesian;

      now

        let K be Subset of AS, o,a,b,c,a9,b9,c9 be Element of AS such that

         A2: K is being_line and

         A3: o in K and

         A4: c in K & c9 in K and

         A5: not a in K and

         A6: o <> c and

         A7: a <> b and

         A8: LIN (o,a,a9) and

         A9: LIN (o,b,b9) and

         A10: (a,b) // (a9,b9) & (a,c) // (a9,c9) and

         A11: (a,b) // K;

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

        

         A12: o in A by A3, A5, AFF_1: 24;

         A13:

        now

          assume

           A14: o = b;

          (b,a) // K by A11, AFF_1: 34;

          hence contradiction by A2, A3, A5, A14, AFF_1: 23;

        end;

        then

         A15: b in P by AFF_1: 24;

        

         A16: a in A by A3, A5, AFF_1: 24;

        

         A17: A is being_line by A3, A5, AFF_1: 24;

        

         A18: A <> P

        proof

          assume A = P;

          then (a,b) // A by A17, A16, A15, AFF_1: 40, AFF_1: 41;

          hence contradiction by A3, A5, A7, A11, A12, A16, AFF_1: 45, AFF_1: 53;

        end;

        

         A19: P is being_line & o in P by A13, AFF_1: 24;

        then

         A20: b9 in P by A9, A13, A15, AFF_1: 25;

        a9 in A by A3, A5, A8, A17, A12, A16, AFF_1: 25;

        hence (b,c) // (b9,c9) by A1, A2, A3, A4, A5, A6, A10, A13, A17, A12, A16, A19, A15, A20, A18, AFF_2:def 4;

      end;

      hence thesis by AFF_2:def 7;

    end;

    theorem :: PAPDESAF:16

    

     Th16: for V be RealLinearSpace, OAS be OAffinSpace st OAS = ( OASpace V) holds ( Lambda OAS) is Moufangian

    proof

      let V be RealLinearSpace, OAS be OAffinSpace;

      assume OAS = ( OASpace V);

      then ( Lambda OAS) is Desarguesian by Th9, Th11;

      hence thesis by Th15;

    end;

    theorem :: PAPDESAF:17

    

     Th17: for V be RealLinearSpace, OAS be OAffinSpace st OAS = ( OASpace V) holds ( Lambda OAS) is translational

    proof

      let V be RealLinearSpace, OAS be OAffinSpace such that

       A1: OAS = ( OASpace V);

      set AS = ( Lambda OAS);

      for A,P,C be Subset of AS, a,b,c,a9,b9,c9 be Element of AS st A // P & A // C & a in A & a9 in A & b in P & b9 in P & c in C & c9 in C & A is being_line & P is being_line & C is being_line & A <> P & A <> C & (a,b) // (a9,b9) & (a,c) // (a9,c9) holds (b,c) // (b9,c9)

      proof

        let A,P,C be Subset of AS, a,b,c,a9,b9,c9 be Element of AS such that

         A2: A // P and

         A3: A // C and

         A4: a in A and

         A5: a9 in A and

         A6: b in P and

         A7: b9 in P and

         A8: c in C and

         A9: c9 in C and

         A10: A is being_line and

         A11: P is being_line and

         A12: C is being_line and

         A13: A <> P and

         A14: A <> C and

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

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

        reconsider a1 = a, b1 = b, c1 = c, a19 = a9, b19 = b9, c19 = c9 as Element of OAS by Th1;

        reconsider u = a1, v = b1, w = c1, u9 = a19 as VECTOR of V by A1, Th3;

         A17:

        now

          assume

           A18: a <> a9;

          

           A19: not (a1,a19,b1) are_collinear

          proof

            assume (a1,a19,b1) are_collinear ;

            then LIN (a,a9,b) by Th2;

            then b in A by A4, A5, A10, A18, AFF_1: 25;

            hence contradiction by A2, A6, A13, AFF_1: 45;

          end;

          

           A20: not (a1,a19,c1) are_collinear

          proof

            assume (a1,a19,c1) are_collinear ;

            then LIN (a,a9,c) by Th2;

            then c in A by A4, A5, A10, A18, AFF_1: 25;

            hence contradiction by A3, A8, A14, AFF_1: 45;

          end;

          (a,a9) // (c,c9) by A3, A4, A5, A8, A9, AFF_1: 39;

          then

           A21: (a1,a19) '||' (c1,c19) by DIRAF: 38;

          (a,a9) // (b,b9) by A2, A4, A5, A6, A7, AFF_1: 39;

          then

           A22: (a1,a19) '||' (b1,b19) by DIRAF: 38;

          set v99 = ((u9 + v) - u), w99 = ((u9 + w) - u);

          reconsider b199 = v99, c199 = w99 as Element of OAS by A1, Th3;

          (w99 - v99) = ((u9 + w) - (((u9 + v) - u) + u)) by RLVECT_1: 27

          .= ((u9 + w) - (u9 + v)) by RLSUB_2: 61

          .= (((w + u9) - u9) - v) by RLVECT_1: 27

          .= (w - v) by RLSUB_2: 61;

          then (v,w) // (v99,w99) by ANALOAF: 15;

          then

           A23: (v,w) '||' (v99,w99) by GEOMTRAP:def 1;

          (u,u9) // (v,v99) by ANALOAF: 16;

          then (u,u9) '||' (v,v99) by GEOMTRAP:def 1;

          then

           A24: (a1,a19) '||' (b1,b199) by A1, Th4;

          (u,w) // (u9,w99) by ANALOAF: 16;

          then (u,w) '||' (u9,w99) by GEOMTRAP:def 1;

          then

           A25: (a1,c1) '||' (a19,c199) by A1, Th4;

          (u,u9) // (w,w99) by ANALOAF: 16;

          then (u,u9) '||' (w,w99) by GEOMTRAP:def 1;

          then

           A26: (a1,a19) '||' (c1,c199) by A1, Th4;

          (u,v) // (u9,v99) by ANALOAF: 16;

          then (u,v) '||' (u9,v99) by GEOMTRAP:def 1;

          then

           A27: (a1,b1) '||' (a19,b199) by A1, Th4;

          (a1,c1) '||' (a19,c19) by A16, DIRAF: 38;

          then

           A28: c199 = c19 by A20, A21, A26, A25, PASCH: 5;

          (a1,b1) '||' (a19,b19) by A15, DIRAF: 38;

          then b199 = b19 by A19, A22, A24, A27, PASCH: 5;

          then (b1,c1) '||' (b19,c19) by A1, A28, A23, Th4;

          hence thesis by DIRAF: 38;

        end;

        now

          assume

           A29: a = a9;

          

           A30: c = c9

          proof

             LIN (a,c,c9) by A16, A29, AFF_1:def 1;

            then

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

            assume c <> c9;

            then a in C by A8, A9, A12, A31, AFF_1: 25;

            hence contradiction by A3, A4, A14, AFF_1: 45;

          end;

          b = b9

          proof

             LIN (a,b,b9) by A15, A29, AFF_1:def 1;

            then

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

            assume b <> b9;

            then a in P by A6, A7, A11, A32, AFF_1: 25;

            hence contradiction by A2, A4, A13, AFF_1: 45;

          end;

          hence thesis by A30, AFF_1: 2;

        end;

        hence thesis by A17;

      end;

      hence thesis by AFF_2:def 11;

    end;

    theorem :: PAPDESAF:18

    

     Th18: for OAS be OAffinSpace holds ( Lambda OAS) is Fanoian

    proof

      let OAS be OAffinSpace;

      set AS = ( Lambda OAS);

      for a,b,c,d be Element of AS st (a,b) // (c,d) & (a,c) // (b,d) & (a,d) // (b,c) holds (a,b) // (a,c)

      proof

        let a,b,c,d be Element of AS such that

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

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

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

        reconsider a1 = a, b1 = b, c1 = c, d1 = d as Element of OAS by Th1;

        set P = ( Line (a,d)), Q = ( Line (b,c));

        assume

         A4: not (a,b) // (a,c);

        then

         A5: a <> d by A1, AFF_1: 4;

        then

         A6: P is being_line by AFF_1:def 3;

        

         A7: not (a1,b1,c1) are_collinear

        proof

          assume not thesis;

          then (a1,b1) '||' (a1,c1) by DIRAF:def 5;

          hence contradiction by A4, DIRAF: 38;

        end;

        (a1,b1) '||' (c1,d1) & (a1,c1) '||' (b1,d1) by A1, A2, DIRAF: 38;

        then

        consider x1 be Element of OAS such that

         A8: (x1,a1,d1) are_collinear and

         A9: (x1,b1,c1) are_collinear by A7, PASCH: 25;

        reconsider x = x1 as Element of AS by Th1;

        

         A10: d in P by AFF_1: 15;

        (x1,a1) '||' (x1,d1) by A8, DIRAF:def 5;

        then (x,a) // (x,d) by DIRAF: 38;

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

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

        then

         A11: x in P by AFF_1:def 2;

        

         A12: a in P & b in Q by AFF_1: 15;

        (x1,b1) '||' (x1,c1) by A9, DIRAF:def 5;

        then (x,b) // (x,c) by DIRAF: 38;

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

        then LIN (b,c,x) by AFF_1: 6;

        then

         A13: x in Q by AFF_1:def 2;

        

         A14: c in Q by AFF_1: 15;

        

         A15: not LIN (a,b,c) by A4, AFF_1:def 1;

        then

         A16: b <> c by AFF_1: 7;

        then Q is being_line by AFF_1:def 3;

        then P // Q by A3, A16, A5, A6, A10, A12, A14, AFF_1: 38;

        then P = Q by A11, A13, AFF_1: 45;

        hence contradiction by A15, A6, A12, A14, AFF_1: 21;

      end;

      hence thesis;

    end;

    registration

      cluster Pappian Desarguesian Moufangian translation for OAffinSpace;

      existence

      proof

        consider V be RealLinearSpace such that

         A1: ex u,v be VECTOR of V st for a,b be Real st ((a * u) + (b * v)) = ( 0. V) holds a = 0 & b = 0 by FUNCSDOM: 23;

        reconsider X = ( OASpace V) as OAffinSpace by A1, ANALOAF: 26;

        take X;

        set AS = ( Lambda X);

        

         A2: AS is Moufangian & AS is translational by Th16, Th17;

        AS is Pappian & AS is Desarguesian by Th9, Th11, Th13;

        hence thesis by A2;

      end;

    end

    registration

      cluster strict Fanoian Pappian Desarguesian Moufangian translational for AffinPlane;

      existence

      proof

        consider V be RealLinearSpace such that

         A1: ex u,v be VECTOR of V st (for a,b be Real st ((a * u) + (b * v)) = ( 0. V) holds a = 0 & b = 0 ) & for w be VECTOR of V holds ex a,b be Real st w = ((a * u) + (b * v)) by FUNCSDOM: 23;

        reconsider OAS = ( OASpace V) as OAffinPlane by A1, ANALOAF: 28;

        take X = ( Lambda OAS);

        

         A2: X is Pappian by Th13;

        then X is Moufangian by AFF_2: 11, AFF_2: 12;

        hence thesis by A2, Th18, AFF_2: 11, AFF_2: 14;

      end;

    end

    registration

      cluster strict Fanoian Pappian Desarguesian Moufangian translational for AffinSpace;

      existence

      proof

        consider V be RealLinearSpace such that

         A1: ex u,v be VECTOR of V st for a,b be Real st ((a * u) + (b * v)) = ( 0. V) holds a = 0 & b = 0 by FUNCSDOM: 23;

        reconsider X = ( OASpace V) as OAffinSpace by A1, ANALOAF: 26;

        take ( Lambda X);

        thus thesis by Th13, Th14, Th16, Th17, Th18;

      end;

    end

    registration

      let OAS be OAffinSpace;

      cluster ( Lambda OAS) -> Fanoian;

      correctness by Th18;

    end

    registration

      let OAS be Pappian OAffinSpace;

      cluster ( Lambda OAS) -> Pappian;

      correctness by Def2;

    end

    registration

      let OAS be Desarguesian OAffinSpace;

      cluster ( Lambda OAS) -> Desarguesian;

      correctness by Def3;

    end

    registration

      let OAS be Moufangian OAffinSpace;

      cluster ( Lambda OAS) -> Moufangian;

      correctness by Def4;

    end

    registration

      let OAS be translation OAffinSpace;

      cluster ( Lambda OAS) -> translational;

      correctness by Def5;

    end