afproj.miz



    begin

    reserve AS for AffinSpace;

    reserve A,K,M,X,Y,Z,X9,Y9 for Subset of AS;

    reserve zz for Element of AS;

    reserve x,y for set;

    theorem :: AFPROJ:1

    

     Th1: AS is AffinPlane & X = the carrier of AS implies X is being_plane

    proof

      assume that

       A1: AS is AffinPlane and

       A2: X = the carrier of AS;

      consider a,b,c be Element of AS such that

       A3: not LIN (a,b,c) by AFF_1: 12;

      set P = ( Line (a,b)), K = ( Line (a,c));

      

       A4: b in P by AFF_1: 15;

      

       A5: c in K by AFF_1: 15;

      a <> b by A3, AFF_1: 7;

      then

       A6: P is being_line by AFF_1:def 3;

      set Y = ( Plane (K,P));

      

       A7: a in P by AFF_1: 15;

      a <> c by A3, AFF_1: 7;

      then

       A8: K is being_line by AFF_1:def 3;

      

       A9: a in K by AFF_1: 15;

      

       A10: not K // P

      proof

        assume K // P;

        then c in P by A7, A9, A5, AFF_1: 45;

        hence contradiction by A3, A7, A4, A6, AFF_1: 21;

      end;

      now

        let x be object;

        assume x in X;

        then

        reconsider a = x as Element of AS;

        set K9 = (a * K);

        

         A11: K9 is being_line by A8, AFF_4: 27;

        

         A12: K // K9 by A8, AFF_4:def 3;

        then not K9 // P by A10, AFF_1: 44;

        then

        consider b be Element of AS such that

         A13: b in K9 and

         A14: b in P by A1, A6, A11, AFF_1: 58;

        a in K9 by A8, AFF_4:def 3;

        then (a,b) // K by A12, A13, AFF_1: 40;

        then a in { zz : ex b be Element of AS st (zz,b) // K & b in P } by A14;

        hence x in Y by AFF_4:def 1;

      end;

      then

       A15: X c= Y;

      Y is being_plane by A6, A8, A10, AFF_4:def 2;

      hence thesis by A2, A15, XBOOLE_0:def 10;

    end;

    theorem :: AFPROJ:2

    

     Th2: AS is AffinPlane & X is being_plane implies X = the carrier of AS

    proof

      assume that

       A1: AS is AffinPlane and

       A2: X is being_plane;

      the carrier of AS c= the carrier of AS;

      then

      reconsider Z = the carrier of AS as Subset of AS;

      Z is being_plane by A1, Th1;

      hence thesis by A2, AFF_4: 33;

    end;

    theorem :: AFPROJ:3

    

     Th3: AS is AffinPlane & X is being_plane & Y is being_plane implies X = Y

    proof

      assume that

       A1: AS is AffinPlane and

       A2: X is being_plane and

       A3: Y is being_plane;

      X = the carrier of AS by A1, A2, Th2;

      hence thesis by A1, A3, Th2;

    end;

    theorem :: AFPROJ:4

    X = the carrier of AS & X is being_plane implies AS is AffinPlane

    proof

      assume that

       A1: X = the carrier of AS and

       A2: X is being_plane;

      assume not AS is AffinPlane;

      then ex zz st not zz in X by A2, AFF_4: 48;

      hence contradiction by A1;

    end;

    theorem :: AFPROJ:5

    

     Th5: not A // K & A '||' X & A '||' Y & K '||' X & K '||' Y & A is being_line & K is being_line & X is being_plane & Y is being_plane implies X '||' Y

    proof

      assume that

       A1: not A // K and

       A2: A '||' X and

       A3: A '||' Y and

       A4: K '||' X and

       A5: K '||' Y and

       A6: A is being_line and

       A7: K is being_line and

       A8: X is being_plane and

       A9: Y is being_plane;

      set y = the Element of Y;

      set x = the Element of X;

      

       A10: Y <> {} by A9, AFF_4: 59;

      

       A11: X <> {} by A8, AFF_4: 59;

      then

      reconsider a = x, b = y as Element of AS by A10, TARSKI:def 3;

      

       A12: K // (a * K) by A7, AFF_4:def 3;

      

       A13: A // (a * A) by A6, AFF_4:def 3;

      

       A14: not (a * A) // (a * K)

      proof

        assume not thesis;

        then (a * A) // K by A12, AFF_1: 44;

        hence contradiction by A1, A13, AFF_1: 44;

      end;

      (a * K) c= (a + X) by A4, A7, A8, AFF_4: 68;

      then

       A15: (a * K) c= X by A8, A11, AFF_4: 66;

      K // (b * K) by A7, AFF_4:def 3;

      then

       A16: (a * K) // (b * K) by A12, AFF_1: 44;

      (b * A) c= (b + Y) by A3, A6, A9, AFF_4: 68;

      then

       A17: (b * A) c= Y by A9, A10, AFF_4: 66;

      A // (b * A) by A6, AFF_4:def 3;

      then

       A18: (a * A) // (b * A) by A13, AFF_1: 44;

      (b * K) c= (b + Y) by A5, A7, A9, AFF_4: 68;

      then

       A19: (b * K) c= Y by A9, A10, AFF_4: 66;

      (a * A) c= (a + X) by A2, A6, A8, AFF_4: 68;

      then (a * A) c= X by A8, A11, AFF_4: 66;

      hence thesis by A8, A9, A15, A17, A19, A14, A18, A16, AFF_4: 55;

    end;

    theorem :: AFPROJ:6

    X is being_plane & A '||' X & X '||' Y implies A '||' Y by AFF_4: 59, AFF_4: 60;

    definition

      let AS;

      :: AFPROJ:def1

      func AfLines (AS) -> Subset-Family of AS equals { A : A is being_line };

      coherence

      proof

        set X = { A : A is being_line };

        X c= ( bool the carrier of AS)

        proof

          let x be object;

          assume x in X;

          then ex A st x = A & A is being_line;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    definition

      let AS;

      :: AFPROJ:def2

      func AfPlanes (AS) -> Subset-Family of AS equals { A : A is being_plane };

      coherence

      proof

        set X = { A : A is being_plane };

        X c= ( bool the carrier of AS)

        proof

          let x be object;

          assume x in X;

          then ex A st x = A & A is being_plane;

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: AFPROJ:7

    for x holds (x in ( AfLines AS) iff ex X st x = X & X is being_line);

    theorem :: AFPROJ:8

    for x holds (x in ( AfPlanes AS) iff ex X st x = X & X is being_plane);

    definition

      let AS;

      :: AFPROJ:def3

      func LinesParallelity (AS) -> Equivalence_Relation of ( AfLines AS) equals { [K, M] : K is being_line & M is being_line & K '||' M };

      coherence

      proof

        set AFL = ( AfLines AS), AFL2 = [:( AfLines AS), ( AfLines AS):];

        set R1 = { [X, Y] : X is being_line & Y is being_line & X '||' Y };

        now

          let x be object;

          assume x in R1;

          then

          consider X, Y such that

           A1: x = [X, Y] and

           A2: X is being_line and

           A3: Y is being_line and X '||' Y;

          

           A4: Y in AFL by A3;

          X in AFL by A2;

          hence x in AFL2 by A1, A4, ZFMISC_1:def 2;

        end;

        then

        reconsider R2 = R1 as Relation of AFL, AFL by TARSKI:def 3;

        now

          let x be object;

          assume x in AFL;

          then

          consider X such that

           A5: x = X and

           A6: X is being_line;

          X // X by A6, AFF_1: 41;

          then X '||' X by A6, AFF_4: 40;

          hence [x, x] in R2 by A5, A6;

        end;

        then

         A7: R2 is_reflexive_in AFL by RELAT_2:def 1;

        then

         A8: ( field R2) = AFL by ORDERS_1: 13;

        

         A9: X is being_line & Y is being_line implies ( [X, Y] in R1 iff X '||' Y)

        proof

          assume that

           A10: X is being_line and

           A11: Y is being_line;

          now

            assume [X, Y] in R1;

            then

            consider X9, Y9 such that

             A12: [X, Y] = [X9, Y9] and X9 is being_line and Y9 is being_line and

             A13: X9 '||' Y9;

            X = X9 by A12, XTUPLE_0: 1;

            hence X '||' Y by A12, A13, XTUPLE_0: 1;

          end;

          hence thesis by A10, A11;

        end;

        now

          let x,y,z be object;

          assume that

           A14: x in AFL and

           A15: y in AFL and

           A16: z in AFL and

           A17: [x, y] in R2 and

           A18: [y, z] in R2;

          consider Y such that

           A19: y = Y and

           A20: Y is being_line by A15;

          consider Z such that

           A21: z = Z and

           A22: Z is being_line by A16;

          Y '||' Z by A9, A18, A19, A20, A21, A22;

          then

           A23: Y // Z by A20, A22, AFF_4: 40;

          consider X such that

           A24: x = X and

           A25: X is being_line by A14;

          X '||' Y by A9, A17, A24, A25, A19, A20;

          then X // Y by A25, A20, AFF_4: 40;

          then X // Z by A23, AFF_1: 44;

          then X '||' Z by A25, A22, AFF_4: 40;

          hence [x, z] in R2 by A24, A25, A21, A22;

        end;

        then

         A26: R2 is_transitive_in AFL by RELAT_2:def 8;

        now

          let x,y be object;

          assume that

           A27: x in AFL and

           A28: y in AFL and

           A29: [x, y] in R2;

          consider X such that

           A30: x = X and

           A31: X is being_line by A27;

          consider Y such that

           A32: y = Y and

           A33: Y is being_line by A28;

          X '||' Y by A9, A29, A30, A31, A32, A33;

          then X // Y by A31, A33, AFF_4: 40;

          then Y '||' X by A31, A33, AFF_4: 40;

          hence [y, x] in R2 by A30, A31, A32, A33;

        end;

        then

         A34: R2 is_symmetric_in AFL by RELAT_2:def 3;

        ( dom R2) = AFL by A7, ORDERS_1: 13;

        hence thesis by A8, A34, A26, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16;

      end;

    end

    definition

      let AS;

      :: AFPROJ:def4

      func PlanesParallelity (AS) -> Equivalence_Relation of ( AfPlanes AS) equals { [X, Y] : X is being_plane & Y is being_plane & X '||' Y };

      coherence

      proof

        set AFP = ( AfPlanes AS), AFP2 = [:( AfPlanes AS), ( AfPlanes AS):];

        set R1 = { [X, Y] : X is being_plane & Y is being_plane & X '||' Y };

        now

          let x be object;

          assume x in R1;

          then

          consider X, Y such that

           A1: x = [X, Y] and

           A2: X is being_plane and

           A3: Y is being_plane and X '||' Y;

          

           A4: Y in AFP by A3;

          X in AFP by A2;

          hence x in AFP2 by A1, A4, ZFMISC_1:def 2;

        end;

        then

        reconsider R2 = R1 as Relation of AFP, AFP by TARSKI:def 3;

        now

          let x be object;

          assume x in AFP;

          then

          consider X such that

           A5: x = X and

           A6: X is being_plane;

          X '||' X by A6, AFF_4: 57;

          hence [x, x] in R2 by A5, A6;

        end;

        then

         A7: R2 is_reflexive_in AFP by RELAT_2:def 1;

        then

         A8: ( field R2) = AFP by ORDERS_1: 13;

        

         A9: X is being_plane & Y is being_plane implies ( [X, Y] in R1 iff X '||' Y)

        proof

          assume that

           A10: X is being_plane and

           A11: Y is being_plane;

          now

            assume [X, Y] in R1;

            then

            consider X9, Y9 such that

             A12: [X, Y] = [X9, Y9] and X9 is being_plane and Y9 is being_plane and

             A13: X9 '||' Y9;

            X = X9 by A12, XTUPLE_0: 1;

            hence X '||' Y by A12, A13, XTUPLE_0: 1;

          end;

          hence thesis by A10, A11;

        end;

        now

          let x,y,z be object;

          assume that

           A14: x in AFP and

           A15: y in AFP and

           A16: z in AFP and

           A17: [x, y] in R2 and

           A18: [y, z] in R2;

          consider X such that

           A19: x = X and

           A20: X is being_plane by A14;

          consider Y such that

           A21: y = Y and

           A22: Y is being_plane by A15;

          consider Z such that

           A23: z = Z and

           A24: Z is being_plane by A16;

          

           A25: Y '||' Z by A9, A18, A21, A22, A23, A24;

          X '||' Y by A9, A17, A19, A20, A21, A22;

          then X '||' Z by A20, A22, A24, A25, AFF_4: 61;

          hence [x, z] in R2 by A19, A20, A23, A24;

        end;

        then

         A26: R2 is_transitive_in AFP by RELAT_2:def 8;

        now

          let x,y be object;

          assume that

           A27: x in AFP and

           A28: y in AFP and

           A29: [x, y] in R2;

          consider X such that

           A30: x = X and

           A31: X is being_plane by A27;

          consider Y such that

           A32: y = Y and

           A33: Y is being_plane by A28;

          X '||' Y by A9, A29, A30, A31, A32, A33;

          then Y '||' X by A31, A33, AFF_4: 58;

          hence [y, x] in R2 by A30, A31, A32, A33;

        end;

        then

         A34: R2 is_symmetric_in AFP by RELAT_2:def 3;

        ( dom R2) = AFP by A7, ORDERS_1: 13;

        hence thesis by A8, A34, A26, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16;

      end;

    end

    definition

      let AS, X;

      :: AFPROJ:def5

      func LDir (X) -> Subset of ( AfLines AS) equals ( Class (( LinesParallelity AS),X));

      correctness ;

    end

    definition

      let AS, X;

      :: AFPROJ:def6

      func PDir (X) -> Subset of ( AfPlanes AS) equals ( Class (( PlanesParallelity AS),X));

      correctness ;

    end

    theorem :: AFPROJ:9

    

     Th9: X is being_line implies for x holds x in ( LDir X) iff ex Y st x = Y & Y is being_line & X '||' Y

    proof

      assume

       A1: X is being_line;

      let x;

       A2:

      now

        assume x in ( LDir X);

        then [x, X] in ( LinesParallelity AS) by EQREL_1: 19;

        then

        consider K, M such that

         A3: [x, X] = [K, M] and

         A4: K is being_line and

         A5: M is being_line and

         A6: K '||' M;

        take Y = K;

        

         A7: X = M by A3, XTUPLE_0: 1;

        K // M by A4, A5, A6, AFF_4: 40;

        hence x = Y & Y is being_line & X '||' Y by A3, A4, A5, A7, AFF_4: 40, XTUPLE_0: 1;

      end;

      now

        given Y such that

         A8: x = Y and

         A9: Y is being_line and

         A10: X '||' Y;

        X // Y by A1, A9, A10, AFF_4: 40;

        then Y '||' X by A1, A9, AFF_4: 40;

        then [Y, X] in { [K, M] : K is being_line & M is being_line & K '||' M } by A1, A9;

        hence x in ( LDir X) by A8, EQREL_1: 19;

      end;

      hence thesis by A2;

    end;

    theorem :: AFPROJ:10

    

     Th10: X is being_plane implies for x holds x in ( PDir X) iff ex Y st x = Y & Y is being_plane & X '||' Y

    proof

      assume

       A1: X is being_plane;

      let x;

       A2:

      now

        assume x in ( PDir X);

        then [x, X] in ( PlanesParallelity AS) by EQREL_1: 19;

        then

        consider K, M such that

         A3: [x, X] = [K, M] and

         A4: K is being_plane and

         A5: M is being_plane and

         A6: K '||' M;

        take Y = K;

        X = M by A3, XTUPLE_0: 1;

        hence x = Y & Y is being_plane & X '||' Y by A3, A4, A5, A6, AFF_4: 58, XTUPLE_0: 1;

      end;

      now

        given Y such that

         A7: x = Y and

         A8: Y is being_plane and

         A9: X '||' Y;

        Y '||' X by A1, A8, A9, AFF_4: 58;

        then [Y, X] in { [K, M] : K is being_plane & M is being_plane & K '||' M } by A1, A8;

        hence x in ( PDir X) by A7, EQREL_1: 19;

      end;

      hence thesis by A2;

    end;

    theorem :: AFPROJ:11

    

     Th11: X is being_line & Y is being_line implies (( LDir X) = ( LDir Y) iff X // Y)

    proof

      assume that

       A1: X is being_line and

       A2: Y is being_line;

      

       A3: ( LDir Y) = ( Class (( LinesParallelity AS),Y));

      

       A4: Y in ( AfLines AS) by A2;

       A5:

      now

        assume ( LDir X) = ( LDir Y);

        then X in ( Class (( LinesParallelity AS),Y)) by A4, EQREL_1: 23;

        then ex Y9 st X = Y9 & Y9 is being_line & Y '||' Y9 by A2, A3, Th9;

        hence X // Y by A2, AFF_4: 40;

      end;

      

       A6: ( LDir X) = ( Class (( LinesParallelity AS),X));

      

       A7: X in ( AfLines AS) by A1;

      now

        assume X // Y;

        then X '||' Y by A1, A2, AFF_4: 40;

        then Y in ( Class (( LinesParallelity AS),X)) by A1, A2, A6, Th9;

        hence ( LDir X) = ( LDir Y) by A7, EQREL_1: 23;

      end;

      hence thesis by A5;

    end;

    theorem :: AFPROJ:12

    

     Th12: X is being_line & Y is being_line implies (( LDir X) = ( LDir Y) iff X '||' Y)

    proof

      assume that

       A1: X is being_line and

       A2: Y is being_line;

      ( LDir X) = ( LDir Y) iff X // Y by A1, A2, Th11;

      hence thesis by A1, A2, AFF_4: 40;

    end;

    theorem :: AFPROJ:13

    

     Th13: X is being_plane & Y is being_plane implies (( PDir X) = ( PDir Y) iff X '||' Y)

    proof

      assume that

       A1: X is being_plane and

       A2: Y is being_plane;

      

       A3: ( PDir Y) = ( Class (( PlanesParallelity AS),Y));

      

       A4: Y in ( AfPlanes AS) by A2;

       A5:

      now

        assume ( PDir X) = ( PDir Y);

        then X in ( Class (( PlanesParallelity AS),Y)) by A4, EQREL_1: 23;

        then ex Y9 st X = Y9 & Y9 is being_plane & Y '||' Y9 by A2, A3, Th10;

        hence X '||' Y by A2, AFF_4: 58;

      end;

      

       A6: ( PDir X) = ( Class (( PlanesParallelity AS),X));

      

       A7: X in ( AfPlanes AS) by A1;

      now

        assume X '||' Y;

        then Y in ( Class (( PlanesParallelity AS),X)) by A1, A2, A6, Th10;

        hence ( PDir X) = ( PDir Y) by A7, EQREL_1: 23;

      end;

      hence thesis by A5;

    end;

    definition

      let AS;

      :: AFPROJ:def7

      func Dir_of_Lines (AS) -> non empty set equals ( Class ( LinesParallelity AS));

      coherence

      proof

        consider a,b be Element of AS such that

         A1: a <> b by DIRAF: 40;

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

        A is being_line by A1, AFF_1:def 3;

        then A in ( AfLines AS);

        then ( Class (( LinesParallelity AS),A)) in ( Class ( LinesParallelity AS)) by EQREL_1:def 3;

        hence thesis;

      end;

    end

    definition

      let AS;

      :: AFPROJ:def8

      func Dir_of_Planes (AS) -> non empty set equals ( Class ( PlanesParallelity AS));

      coherence

      proof

        set a = the Element of AS;

        consider A such that a in A and a in A and a in A and

         A1: A is being_plane by AFF_4: 37;

        A in ( AfPlanes AS) by A1;

        then ( Class (( PlanesParallelity AS),A)) in ( Class ( PlanesParallelity AS)) by EQREL_1:def 3;

        hence thesis;

      end;

    end

    theorem :: AFPROJ:14

    

     Th14: for x holds x in ( Dir_of_Lines AS) iff ex X st x = ( LDir X) & X is being_line

    proof

      let x;

       A1:

      now

        assume

         A2: x in ( Dir_of_Lines AS);

        then

        reconsider x99 = x as Subset of ( AfLines AS);

        consider x9 be object such that

         A3: x9 in ( AfLines AS) and

         A4: x99 = ( Class (( LinesParallelity AS),x9)) by A2, EQREL_1:def 3;

        consider X such that

         A5: x9 = X and

         A6: X is being_line by A3;

        take X;

        thus x = ( LDir X) by A4, A5;

        thus X is being_line by A6;

      end;

      now

        given X such that

         A7: x = ( LDir X) and

         A8: X is being_line;

        X in ( AfLines AS) by A8;

        hence x in ( Dir_of_Lines AS) by A7, EQREL_1:def 3;

      end;

      hence thesis by A1;

    end;

    theorem :: AFPROJ:15

    

     Th15: for x holds x in ( Dir_of_Planes AS) iff ex X st x = ( PDir X) & X is being_plane

    proof

      let x;

       A1:

      now

        assume

         A2: x in ( Dir_of_Planes AS);

        then

        reconsider x99 = x as Subset of ( AfPlanes AS);

        consider x9 be object such that

         A3: x9 in ( AfPlanes AS) and

         A4: x99 = ( Class (( PlanesParallelity AS),x9)) by A2, EQREL_1:def 3;

        consider X such that

         A5: x9 = X and

         A6: X is being_plane by A3;

        take X;

        thus x = ( PDir X) by A4, A5;

        thus X is being_plane by A6;

      end;

      now

        given X such that

         A7: x = ( PDir X) and

         A8: X is being_plane;

        X in ( AfPlanes AS) by A8;

        hence x in ( Dir_of_Planes AS) by A7, EQREL_1:def 3;

      end;

      hence thesis by A1;

    end;

    theorem :: AFPROJ:16

    

     Th16: the carrier of AS misses ( Dir_of_Lines AS)

    proof

      assume not thesis;

      then

      consider x be object such that

       A1: x in the carrier of AS and

       A2: x in ( Dir_of_Lines AS) by XBOOLE_0: 3;

      reconsider a = x as Element of AS by A1;

      consider X such that

       A3: x = ( LDir X) and

       A4: X is being_line by A2, Th14;

      set A = (a * X);

      

       A5: A is being_line by A4, AFF_4: 27;

      X // A by A4, AFF_4:def 3;

      then X '||' A by A4, A5, AFF_4: 40;

      then A in a by A3, A4, A5, Th9;

      hence contradiction by A4, AFF_4:def 3;

    end;

    theorem :: AFPROJ:17

    AS is AffinPlane implies ( AfLines AS) misses ( Dir_of_Planes AS)

    proof

      the carrier of AS c= the carrier of AS;

      then

      reconsider X9 = the carrier of AS as Subset of AS;

      assume AS is AffinPlane;

      then

       A1: X9 is being_plane by Th1;

      assume not thesis;

      then

      consider x be object such that

       A2: x in ( AfLines AS) and

       A3: x in ( Dir_of_Planes AS) by XBOOLE_0: 3;

      consider Y such that

       A4: x = Y and

       A5: Y is being_line by A2;

      consider X such that

       A6: x = ( PDir X) and

       A7: X is being_plane by A3, Th15;

      consider a,b be Element of AS such that

       A8: a in Y and b in Y and a <> b by A5, AFF_1: 19;

      consider Y9 such that

       A9: a = Y9 and

       A10: Y9 is being_plane and X '||' Y9 by A6, A7, A4, A8, Th10;

      

       A11: not Y9 in Y9;

      Y9 = X9 by A1, A10, AFF_4: 33;

      hence contradiction by A9, A11;

    end;

    theorem :: AFPROJ:18

    

     Th18: for x holds (x in [:( AfLines AS), {1}:] iff ex X st x = [X, 1] & X is being_line)

    proof

      let x;

       A1:

      now

        assume x in [:( AfLines AS), {1}:];

        then

        consider x1,x2 be object such that

         A2: x1 in ( AfLines AS) and

         A3: x2 in {1} and

         A4: x = [x1, x2] by ZFMISC_1:def 2;

        consider X such that

         A5: x1 = X and

         A6: X is being_line by A2;

        take X;

        thus x = [X, 1] by A3, A4, A5, TARSKI:def 1;

        thus X is being_line by A6;

      end;

      now

        given X such that

         A7: x = [X, 1] and

         A8: X is being_line;

        X in ( AfLines AS) by A8;

        hence x in [:( AfLines AS), {1}:] by A7, ZFMISC_1: 106;

      end;

      hence thesis by A1;

    end;

    theorem :: AFPROJ:19

    

     Th19: for x holds (x in [:( Dir_of_Planes AS), {2}:] iff ex X st x = [( PDir X), 2] & X is being_plane)

    proof

      let x;

       A1:

      now

        assume x in [:( Dir_of_Planes AS), {2}:];

        then

        consider x1,x2 be object such that

         A2: x1 in ( Dir_of_Planes AS) and

         A3: x2 in {2} and

         A4: x = [x1, x2] by ZFMISC_1:def 2;

        consider X such that

         A5: x1 = ( PDir X) and

         A6: X is being_plane by A2, Th15;

        take X;

        thus x = [( PDir X), 2] by A3, A4, A5, TARSKI:def 1;

        thus X is being_plane by A6;

      end;

      (ex X st x = [( PDir X), 2] & X is being_plane) implies x in [:( Dir_of_Planes AS), {2}:] by Th15, ZFMISC_1: 106;

      hence thesis by A1;

    end;

    definition

      let AS;

      :: AFPROJ:def9

      func ProjectivePoints (AS) -> non empty set equals (the carrier of AS \/ ( Dir_of_Lines AS));

      correctness ;

    end

    definition

      let AS;

      :: AFPROJ:def10

      func ProjectiveLines (AS) -> non empty set equals ( [:( AfLines AS), {1}:] \/ [:( Dir_of_Planes AS), {2}:]);

      coherence ;

    end

    definition

      let AS;

      :: AFPROJ:def11

      func Proj_Inc (AS) -> Relation of ( ProjectivePoints AS), ( ProjectiveLines AS) means

      : Def11: for x,y be object holds [x, y] in it iff (ex K st K is being_line & y = [K, 1] & (x in the carrier of AS & x in K or x = ( LDir K))) or ex K, X st K is being_line & X is being_plane & x = ( LDir K) & y = [( PDir X), 2] & K '||' X;

      existence

      proof

        defpred P[ object, object] means ((ex K st K is being_line & $2 = [K, 1] & ($1 in the carrier of AS & $1 in K or $1 = ( LDir K))) or (ex K, X st K is being_line & X is being_plane & $1 = ( LDir K) & $2 = [( PDir X), 2] & K '||' X));

        set VV1 = ( ProjectivePoints AS), VV2 = ( ProjectiveLines AS);

        consider P be Relation of VV1, VV2 such that

         A1: for x,y be object holds [x, y] in P iff x in VV1 & y in VV2 & P[x, y] from RELSET_1:sch 1;

        take P;

        let x,y be object;

        thus [x, y] in P implies (ex K st K is being_line & y = [K, 1] & (x in the carrier of AS & x in K or x = ( LDir K))) or ex K, X st K is being_line & X is being_plane & x = ( LDir K) & y = [( PDir X), 2] & K '||' X by A1;

        assume

         A2: (ex K st K is being_line & y = [K, 1] & (x in the carrier of AS & x in K or x = ( LDir K))) or ex K, X st K is being_line & X is being_plane & x = ( LDir K) & y = [( PDir X), 2] & K '||' X;

        x in VV1 & y in VV2

        proof

           A3:

          now

            given K such that

             A4: K is being_line and

             A5: y = [K, 1] and

             A6: x in the carrier of AS & x in K or x = ( LDir K);

             A7:

            now

              assume x = ( LDir K);

              then x in ( Dir_of_Lines AS) by A4, Th14;

              hence x in VV1 by XBOOLE_0:def 3;

            end;

            y in [:( AfLines AS), {1}:] by A4, A5, Th18;

            hence thesis by A6, A7, XBOOLE_0:def 3;

          end;

          now

            given K, X such that

             A8: K is being_line and

             A9: X is being_plane and

             A10: x = ( LDir K) and

             A11: y = [( PDir X), 2] and K '||' X;

            x in ( Dir_of_Lines AS) by A8, A10, Th14;

            hence x in VV1 by XBOOLE_0:def 3;

            y in [:( Dir_of_Planes AS), {2}:] by A9, A11, Th19;

            hence y in VV2 by XBOOLE_0:def 3;

          end;

          hence thesis by A2, A3;

        end;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let P,Q be Relation of ( ProjectivePoints AS), ( ProjectiveLines AS) such that

         A12: for x,y be object holds [x, y] in P iff (ex K st K is being_line & y = [K, 1] & (x in the carrier of AS & x in K or x = ( LDir K))) or ex K, X st K is being_line & X is being_plane & x = ( LDir K) & y = [( PDir X), 2] & K '||' X and

         A13: for x,y be object holds [x, y] in Q iff (ex K st K is being_line & y = [K, 1] & (x in the carrier of AS & x in K or x = ( LDir K))) or ex K, X st K is being_line & X is being_plane & x = ( LDir K) & y = [( PDir X), 2] & K '||' X;

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

        proof

          let x,y be object;

           [x, y] in P iff (ex K st K is being_line & y = [K, 1] & (x in the carrier of AS & x in K or x = ( LDir K))) or ex K, X st K is being_line & X is being_plane & x = ( LDir K) & y = [( PDir X), 2] & K '||' X by A12;

          hence thesis by A13;

        end;

        hence thesis by RELAT_1:def 2;

      end;

    end

    definition

      let AS;

      :: AFPROJ:def12

      func Inc_of_Dir (AS) -> Relation of ( Dir_of_Lines AS), ( Dir_of_Planes AS) means

      : Def12: for x,y be object holds [x, y] in it iff ex A, X st x = ( LDir A) & y = ( PDir X) & A is being_line & X is being_plane & A '||' X;

      existence

      proof

        defpred P[ object, object] means ex A, X st $1 = ( LDir A) & $2 = ( PDir X) & A is being_line & X is being_plane & A '||' X;

        set VV1 = ( Dir_of_Lines AS), VV2 = ( Dir_of_Planes AS);

        consider P be Relation of VV1, VV2 such that

         A1: for x,y be object holds [x, y] in P iff x in VV1 & y in VV2 & P[x, y] from RELSET_1:sch 1;

        take P;

        let x,y be object;

        thus [x, y] in P implies ex A, X st x = ( LDir A) & y = ( PDir X) & A is being_line & X is being_plane & A '||' X by A1;

        assume

         A2: ex A, X st x = ( LDir A) & y = ( PDir X) & A is being_line & X is being_plane & A '||' X;

        then

         A3: y in VV2 by Th15;

        x in VV1 by A2, Th14;

        hence thesis by A1, A2, A3;

      end;

      uniqueness

      proof

        let P,Q be Relation of ( Dir_of_Lines AS), ( Dir_of_Planes AS) such that

         A4: for x,y be object holds [x, y] in P iff ex A, X st x = ( LDir A) & y = ( PDir X) & A is being_line & X is being_plane & A '||' X and

         A5: for x,y be object holds [x, y] in Q iff ex A, X st x = ( LDir A) & y = ( PDir X) & A is being_line & X is being_plane & A '||' X;

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

        proof

          let x,y be object;

           [x, y] in P iff ex A, X st x = ( LDir A) & y = ( PDir X) & A is being_line & X is being_plane & A '||' X by A4;

          hence thesis by A5;

        end;

        hence thesis by RELAT_1:def 2;

      end;

    end

    definition

      let AS;

      :: AFPROJ:def13

      func IncProjSp_of (AS) -> strict IncProjStr equals IncProjStr (# ( ProjectivePoints AS), ( ProjectiveLines AS), ( Proj_Inc AS) #);

      correctness ;

    end

    definition

      let AS;

      :: AFPROJ:def14

      func ProjHorizon (AS) -> strict IncProjStr equals IncProjStr (# ( Dir_of_Lines AS), ( Dir_of_Planes AS), ( Inc_of_Dir AS) #);

      correctness ;

    end

    theorem :: AFPROJ:20

    

     Th20: for x holds (x is POINT of ( IncProjSp_of AS) iff (x is Element of AS or ex X st x = ( LDir X) & X is being_line))

    proof

      let x;

       A1:

      now

         A2:

        now

          given X such that

           A3: x = ( LDir X) and

           A4: X is being_line;

          x in ( Dir_of_Lines AS) by A3, A4, Th14;

          hence x is POINT of ( IncProjSp_of AS) by XBOOLE_0:def 3;

        end;

        assume x is Element of AS or ex X st x = ( LDir X) & X is being_line;

        hence x is POINT of ( IncProjSp_of AS) by A2, XBOOLE_0:def 3;

      end;

      now

        assume

         A5: x is POINT of ( IncProjSp_of AS);

        x in ( Dir_of_Lines AS) implies ex X st x = ( LDir X) & X is being_line by Th14;

        hence x is Element of AS or ex X st x = ( LDir X) & X is being_line by A5, XBOOLE_0:def 3;

      end;

      hence thesis by A1;

    end;

    theorem :: AFPROJ:21

    x is Element of the Points of ( ProjHorizon AS) iff ex X st x = ( LDir X) & X is being_line by Th14;

    theorem :: AFPROJ:22

    

     Th22: x is Element of the Points of ( ProjHorizon AS) implies x is POINT of ( IncProjSp_of AS)

    proof

      assume x is Element of the Points of ( ProjHorizon AS);

      then ex X st x = ( LDir X) & X is being_line by Th14;

      hence thesis by Th20;

    end;

    theorem :: AFPROJ:23

    

     Th23: for x holds (x is LINE of ( IncProjSp_of AS) iff ex X st (x = [X, 1] & X is being_line or x = [( PDir X), 2] & X is being_plane))

    proof

      let x;

       A1:

      now

        given X such that

         A2: x = [X, 1] & X is being_line or x = [( PDir X), 2] & X is being_plane;

         A3:

        now

          assume that

           A4: x = [( PDir X), 2] and

           A5: X is being_plane;

          x in [:( Dir_of_Planes AS), {2}:] by A4, A5, Th19;

          hence x is LINE of ( IncProjSp_of AS) by XBOOLE_0:def 3;

        end;

        now

          assume that

           A6: x = [X, 1] and

           A7: X is being_line;

          x in [:( AfLines AS), {1}:] by A6, A7, Th18;

          hence x is LINE of ( IncProjSp_of AS) by XBOOLE_0:def 3;

        end;

        hence x is LINE of ( IncProjSp_of AS) by A2, A3;

      end;

      now

        

         A8: x in [:( Dir_of_Planes AS), {2}:] implies ex X st x = [X, 1] & X is being_line or x = [( PDir X), 2] & X is being_plane by Th19;

        assume

         A9: x is LINE of ( IncProjSp_of AS);

        x in [:( AfLines AS), {1}:] implies ex X st x = [X, 1] & X is being_line or x = [( PDir X), 2] & X is being_plane by Th18;

        hence ex X st x = [X, 1] & X is being_line or x = [( PDir X), 2] & X is being_plane by A9, A8, XBOOLE_0:def 3;

      end;

      hence thesis by A1;

    end;

    theorem :: AFPROJ:24

    x is Element of the Lines of ( ProjHorizon AS) iff ex X st x = ( PDir X) & X is being_plane by Th15;

    theorem :: AFPROJ:25

    

     Th25: x is Element of the Lines of ( ProjHorizon AS) implies [x, 2] is LINE of ( IncProjSp_of AS)

    proof

      assume x is Element of the Lines of ( ProjHorizon AS);

      then ex X st x = ( PDir X) & X is being_plane by Th15;

      hence thesis by Th23;

    end;

    reserve x,y,z,t,u,w for Element of AS;

    reserve K,X,Y,Z,X9,Y9 for Subset of AS;

    reserve a,b,c,d,p,q,r,p9 for POINT of ( IncProjSp_of AS);

    reserve A for LINE of ( IncProjSp_of AS);

    theorem :: AFPROJ:26

    

     Th26: x = a & [X, 1] = A implies (a on A iff X is being_line & x in X)

    proof

      assume that

       A1: x = a and

       A2: [X, 1] = A;

       A3:

      now

         A4:

        now

          given K such that

           A5: K is being_line and

           A6: [X, 1] = [K, 1] and

           A7: x in the carrier of AS & x in K or x = ( LDir K);

           A8:

          now

            assume x = ( LDir K);

            then x in ( Dir_of_Lines AS) by A5, Th14;

            then (the carrier of AS /\ ( Dir_of_Lines AS)) <> {} by XBOOLE_0:def 4;

            then the carrier of AS meets ( Dir_of_Lines AS) by XBOOLE_0:def 7;

            hence contradiction by Th16;

          end;

          X = ( [K, 1] `1 ) by A6

          .= K;

          hence X is being_line & x in X by A5, A7, A8;

        end;

        assume a on A;

        then

         A9: [a, A] in the Inc of ( IncProjSp_of AS) by INCSP_1:def 1;

         not ex K, X9 st K is being_line & X9 is being_plane & x = ( LDir K) & [X, 1] = [( PDir X9), 2] & K '||' X9 by XTUPLE_0: 1;

        hence X is being_line & x in X by A1, A2, A9, A4, Def11;

      end;

      now

        assume that

         A10: X is being_line and

         A11: x in X;

         [x, [X, 1]] in ( Proj_Inc AS) by A10, A11, Def11;

        hence a on A by A1, A2, INCSP_1:def 1;

      end;

      hence thesis by A3;

    end;

    theorem :: AFPROJ:27

    

     Th27: x = a & [( PDir X), 2] = A implies not a on A

    proof

      assume that

       A1: x = a and

       A2: [( PDir X), 2] = A;

       A3:

      now

        given K such that K is being_line and

         A4: [( PDir X), 2] = [K, 1] and x in the carrier of AS & x in K or x = ( LDir K);

        2 = ( [K, 1] `2 ) by A4

        .= 1;

        hence contradiction;

      end;

       A5:

      now

        given K, X9 such that

         A6: K is being_line and X9 is being_plane and

         A7: x = ( LDir K) and [( PDir X), 2] = [( PDir X9), 2] and K '||' X9;

        x in ( Dir_of_Lines AS) by A6, A7, Th14;

        then (the carrier of AS /\ ( Dir_of_Lines AS)) <> {} by XBOOLE_0:def 4;

        then the carrier of AS meets ( Dir_of_Lines AS) by XBOOLE_0:def 7;

        hence contradiction by Th16;

      end;

      assume a on A;

      then [a, A] in the Inc of ( IncProjSp_of AS) by INCSP_1:def 1;

      hence contradiction by A1, A2, A3, A5, Def11;

    end;

    theorem :: AFPROJ:28

    

     Th28: a = ( LDir Y) & [X, 1] = A & Y is being_line & X is being_line implies (a on A iff Y '||' X)

    proof

      assume that

       A1: a = ( LDir Y) and

       A2: [X, 1] = A and

       A3: Y is being_line and

       A4: X is being_line;

       A5:

      now

         A6:

        now

          given K such that

           A7: K is being_line and

           A8: [X, 1] = [K, 1] and

           A9: ( LDir Y) in the carrier of AS & ( LDir Y) in K or ( LDir Y) = ( LDir K);

          

           A10: K in ( AfLines AS) by A7;

          

           A11: X = K by A8, XTUPLE_0: 1;

           A12:

          now

            assume ( LDir Y) = ( LDir K);

            then

             A13: Y in ( Class (( LinesParallelity AS),K)) by A10, EQREL_1: 23;

            ( LDir K) = ( Class (( LinesParallelity AS),K));

            then

            consider K9 be Subset of AS such that

             A14: Y = K9 and

             A15: K9 is being_line and

             A16: K '||' K9 by A7, A13, Th9;

            K // K9 by A7, A15, A16, AFF_4: 40;

            hence Y '||' X by A7, A11, A14, A15, AFF_4: 40;

          end;

          now

            assume that

             A17: ( LDir Y) in the carrier of AS and ( LDir Y) in K;

            a in ( Dir_of_Lines AS) by A1, A3, Th14;

            then (the carrier of AS /\ ( Dir_of_Lines AS)) <> {} by A1, A17, XBOOLE_0:def 4;

            then the carrier of AS meets ( Dir_of_Lines AS) by XBOOLE_0:def 7;

            hence contradiction by Th16;

          end;

          hence Y '||' X by A9, A12;

        end;

        assume a on A;

        then

         A18: [a, A] in the Inc of ( IncProjSp_of AS) by INCSP_1:def 1;

         not ex K, X9 st K is being_line & X9 is being_plane & ( LDir Y) = ( LDir K) & [X, 1] = [( PDir X9), 2] & K '||' X9 by XTUPLE_0: 1;

        hence Y '||' X by A1, A2, A18, A6, Def11;

      end;

      now

        assume Y '||' X;

        then

         A19: X in ( LDir Y) by A3, A4, Th9;

        

         A20: ( LDir X) = ( Class (( LinesParallelity AS),X));

        Y in ( AfLines AS) by A3;

        then ( Class (( LinesParallelity AS),X)) = ( Class (( LinesParallelity AS),Y)) by A19, EQREL_1: 23;

        then [a, A] in ( Proj_Inc AS) by A1, A2, A4, A20, Def11;

        hence a on A by INCSP_1:def 1;

      end;

      hence thesis by A5;

    end;

    theorem :: AFPROJ:29

    

     Th29: a = ( LDir Y) & A = [( PDir X), 2] & Y is being_line & X is being_plane implies (a on A iff Y '||' X)

    proof

      assume that

       A1: a = ( LDir Y) and

       A2: A = [( PDir X), 2] and

       A3: Y is being_line and

       A4: X is being_plane;

       A5:

      now

         A6:

        now

          given K, X9 such that

           A7: K is being_line and

           A8: X9 is being_plane and

           A9: ( LDir Y) = ( LDir K) and

           A10: [( PDir X), 2] = [( PDir X9), 2] and

           A11: K '||' X9;

          

           A12: X9 in ( AfPlanes AS) by A8;

          

           A13: ( Class (( PlanesParallelity AS),X9)) = ( PDir X9);

          ( PDir X) = ( PDir X9) by A10, XTUPLE_0: 1;

          then X in ( Class (( PlanesParallelity AS),X9)) by A12, EQREL_1: 23;

          then

           A14: ex X99 be Subset of AS st X = X99 & X99 is being_plane & X9 '||' X99 by A8, A13, Th10;

          K in ( AfLines AS) by A7;

          then

           A15: Y in ( Class (( LinesParallelity AS),K)) by A9, EQREL_1: 23;

          ( Class (( LinesParallelity AS),K)) = ( LDir K);

          then

          consider K9 be Subset of AS such that

           A16: Y = K9 and

           A17: K9 is being_line and

           A18: K '||' K9 by A7, A15, Th9;

          K // K9 by A7, A17, A18, AFF_4: 40;

          then K9 '||' X9 by A11, AFF_4: 56;

          hence Y '||' X by A8, A16, A14, AFF_4: 59, AFF_4: 60;

        end;

        assume a on A;

        then

         A19: [a, A] in the Inc of ( IncProjSp_of AS) by INCSP_1:def 1;

        (ex K st K is being_line & [( PDir X), 2] = [K, 1] & (( LDir Y) in the carrier of AS & ( LDir Y) in K or ( LDir Y) = ( LDir K))) implies contradiction by XTUPLE_0: 1;

        hence Y '||' X by A1, A2, A19, A6, Def11;

      end;

      now

        assume Y '||' X;

        then [( LDir Y), [( PDir X), 2]] in ( Proj_Inc AS) by A3, A4, Def11;

        hence a on A by A1, A2, INCSP_1:def 1;

      end;

      hence thesis by A5;

    end;

    theorem :: AFPROJ:30

    

     Th30: X is being_line & a = ( LDir X) & A = [X, 1] implies a on A

    proof

      assume that

       A1: X is being_line and

       A2: a = ( LDir X) and

       A3: A = [X, 1];

      X // X by A1, AFF_1: 41;

      then X '||' X by A1, AFF_4: 40;

      hence thesis by A1, A2, A3, Th28;

    end;

    theorem :: AFPROJ:31

    

     Th31: X is being_line & Y is being_plane & X c= Y & a = ( LDir X) & A = [( PDir Y), 2] implies a on A

    proof

      assume that

       A1: X is being_line and

       A2: Y is being_plane and

       A3: X c= Y and

       A4: a = ( LDir X) and

       A5: A = [( PDir Y), 2];

      X '||' Y by A1, A2, A3, AFF_4: 42;

      hence thesis by A1, A2, A4, A5, Th29;

    end;

    theorem :: AFPROJ:32

    

     Th32: Y is being_plane & X c= Y & X9 // X & a = ( LDir X9) & A = [( PDir Y), 2] implies a on A

    proof

      assume that

       A1: Y is being_plane and

       A2: X c= Y and

       A3: X9 // X and

       A4: a = ( LDir X9) and

       A5: A = [( PDir Y), 2];

      X is being_line by A3, AFF_1: 36;

      then

       A6: X9 '||' Y by A1, A2, A3, AFF_4: 42, AFF_4: 56;

      X9 is being_line by A3, AFF_1: 36;

      hence thesis by A1, A4, A5, A6, Th29;

    end;

    theorem :: AFPROJ:33

    A = [( PDir X), 2] & X is being_plane & a on A implies not a is Element of AS by Th27;

    theorem :: AFPROJ:34

    

     Th34: A = [X, 1] & X is being_line & p on A & not p is Element of AS implies p = ( LDir X)

    proof

      assume that

       A1: A = [X, 1] and

       A2: X is being_line and

       A3: p on A and

       A4: not p is Element of AS;

      consider Xp be Subset of AS such that

       A5: p = ( LDir Xp) and

       A6: Xp is being_line by A4, Th20;

      Xp '||' X by A1, A2, A3, A5, A6, Th28;

      hence thesis by A2, A5, A6, Th12;

    end;

    theorem :: AFPROJ:35

    

     Th35: A = [X, 1] & X is being_line & p on A & a on A & a <> p & not p is Element of AS implies a is Element of AS

    proof

      assume that

       A1: A = [X, 1] and

       A2: X is being_line and

       A3: p on A and

       A4: a on A and

       A5: a <> p and

       A6: not p is Element of AS;

      assume not thesis;

      then a = ( LDir X) by A1, A2, A4, Th34;

      hence contradiction by A1, A2, A3, A5, A6, Th34;

    end;

    theorem :: AFPROJ:36

    

     Th36: for a be Element of the Points of ( ProjHorizon AS), A be Element of the Lines of ( ProjHorizon AS) st a = ( LDir X) & A = ( PDir Y) & X is being_line & Y is being_plane holds (a on A iff X '||' Y)

    proof

      let a be Element of the Points of ( ProjHorizon AS), A be Element of the Lines of ( ProjHorizon AS) such that

       A1: a = ( LDir X) and

       A2: A = ( PDir Y) and

       A3: X is being_line and

       A4: Y is being_plane;

       A5:

      now

        assume a on A;

        then [a, A] in the Inc of ( ProjHorizon AS) by INCSP_1:def 1;

        then

        consider X9, Y9 such that

         A6: a = ( LDir X9) and

         A7: A = ( PDir Y9) and

         A8: X9 is being_line and

         A9: Y9 is being_plane and

         A10: X9 '||' Y9 by Def12;

        X // X9 by A1, A3, A6, A8, Th11;

        then

         A11: X '||' Y9 by A10, AFF_4: 56;

        Y9 '||' Y by A2, A4, A7, A9, Th13;

        hence X '||' Y by A9, A11, AFF_4: 59, AFF_4: 60;

      end;

      now

        assume X '||' Y;

        then [a, A] in ( Inc_of_Dir AS) by A1, A2, A3, A4, Def12;

        hence a on A by INCSP_1:def 1;

      end;

      hence thesis by A5;

    end;

    theorem :: AFPROJ:37

    

     Th37: for a be Element of the Points of ( ProjHorizon AS), a9 be Element of the Points of ( IncProjSp_of AS), A be Element of the Lines of ( ProjHorizon AS), A9 be LINE of ( IncProjSp_of AS) st a9 = a & A9 = [A, 2] holds (a on A iff a9 on A9)

    proof

      let a be Element of the Points of ( ProjHorizon AS), a9 be Element of the Points of ( IncProjSp_of AS), A be Element of the Lines of ( ProjHorizon AS), A9 be LINE of ( IncProjSp_of AS) such that

       A1: a9 = a and

       A2: A9 = [A, 2];

      consider X such that

       A3: a = ( LDir X) and

       A4: X is being_line by Th14;

      consider Y such that

       A5: A = ( PDir Y) and

       A6: Y is being_plane by Th15;

       A7:

      now

        assume a9 on A9;

        then X '||' Y by A1, A2, A3, A4, A5, A6, Th29;

        hence a on A by A3, A4, A5, A6, Th36;

      end;

      now

        assume a on A;

        then X '||' Y by A3, A4, A5, A6, Th36;

        hence a9 on A9 by A1, A2, A3, A4, A5, A6, Th29;

      end;

      hence thesis by A7;

    end;

    reserve A,K,M,N,P,Q for LINE of ( IncProjSp_of AS);

    theorem :: AFPROJ:38

    

     Th38: for a,b be Element of the Points of ( ProjHorizon AS), A,K be Element of the Lines of ( ProjHorizon AS) st a on A & a on K & b on A & b on K holds a = b or A = K

    proof

      let a,b be Element of the Points of ( ProjHorizon AS), A,K be Element of the Lines of ( ProjHorizon AS) such that

       A1: a on A and

       A2: a on K and

       A3: b on A and

       A4: b on K;

      consider Y9 such that

       A5: b = ( LDir Y9) and

       A6: Y9 is being_line by Th14;

      consider X9 such that

       A7: K = ( PDir X9) and

       A8: X9 is being_plane by Th15;

      

       A9: Y9 '||' X9 by A4, A5, A6, A7, A8, Th36;

      consider Y such that

       A10: a = ( LDir Y) and

       A11: Y is being_line by Th14;

      assume a <> b;

      then

       A12: not Y // Y9 by A10, A11, A5, A6, Th11;

      consider X such that

       A13: A = ( PDir X) and

       A14: X is being_plane by Th15;

      

       A15: Y9 '||' X by A3, A5, A6, A13, A14, Th36;

      

       A16: Y '||' X9 by A2, A10, A11, A7, A8, Th36;

      Y '||' X by A1, A10, A11, A13, A14, Th36;

      then X '||' X9 by A11, A6, A14, A8, A12, A16, A15, A9, Th5;

      hence thesis by A13, A14, A7, A8, Th13;

    end;

    theorem :: AFPROJ:39

    

     Th39: for A be Element of the Lines of ( ProjHorizon AS) holds ex a,b,c be Element of the Points of ( ProjHorizon AS) st a on A & b on A & c on A & a <> b & b <> c & c <> a

    proof

      let A be Element of the Lines of ( ProjHorizon AS);

      consider X such that

       A1: A = ( PDir X) and

       A2: X is being_plane by Th15;

      consider x, y, z such that

       A3: x in X and

       A4: y in X and

       A5: z in X and

       A6: not LIN (x,y,z) by A2, AFF_4: 34;

      

       A7: y <> z by A6, AFF_1: 7;

      then

       A8: ( Line (y,z)) is being_line by AFF_1:def 3;

      then

       A9: ( Line (y,z)) '||' X by A2, A4, A5, A7, AFF_4: 19, AFF_4: 42;

      

       A10: z <> x by A6, AFF_1: 7;

      then

       A11: ( Line (x,z)) is being_line by AFF_1:def 3;

      then

       A12: ( Line (x,z)) '||' X by A2, A3, A5, A10, AFF_4: 19, AFF_4: 42;

      

       A13: x <> y by A6, AFF_1: 7;

      then

       A14: ( Line (x,y)) is being_line by AFF_1:def 3;

      then

      reconsider a = ( LDir ( Line (x,y))), b = ( LDir ( Line (y,z))), c = ( LDir ( Line (x,z))) as Element of the Points of ( ProjHorizon AS) by A8, A11, Th14;

      take a, b, c;

      ( Line (x,y)) '||' X by A2, A3, A4, A13, A14, AFF_4: 19, AFF_4: 42;

      hence a on A & b on A & c on A by A1, A2, A14, A8, A11, A9, A12, Th36;

      

       A15: x in ( Line (x,y)) by AFF_1: 15;

      

       A16: z in ( Line (y,z)) by AFF_1: 15;

      

       A17: y in ( Line (x,y)) by AFF_1: 15;

      

       A18: y in ( Line (y,z)) by AFF_1: 15;

      thus a <> b

      proof

        assume not thesis;

        then ( Line (x,y)) // ( Line (y,z)) by A14, A8, Th11;

        then z in ( Line (x,y)) by A17, A18, A16, AFF_1: 45;

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

      end;

      

       A19: z in ( Line (x,z)) by AFF_1: 15;

      

       A20: x in ( Line (x,z)) by AFF_1: 15;

      thus b <> c

      proof

        assume not thesis;

        then ( Line (y,z)) // ( Line (x,z)) by A8, A11, Th11;

        then x in ( Line (y,z)) by A16, A20, A19, AFF_1: 45;

        hence contradiction by A6, A8, A18, A16, AFF_1: 21;

      end;

      thus c <> a

      proof

        assume not thesis;

        then ( Line (x,y)) // ( Line (x,z)) by A14, A11, Th11;

        then z in ( Line (x,y)) by A15, A20, A19, AFF_1: 45;

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

      end;

    end;

    theorem :: AFPROJ:40

    

     Th40: for a,b be Element of the Points of ( ProjHorizon AS) holds ex A be Element of the Lines of ( ProjHorizon AS) st a on A & b on A

    proof

      let a,b be Element of the Points of ( ProjHorizon AS);

      consider X such that

       A1: a = ( LDir X) and

       A2: X is being_line by Th14;

      consider X9 such that

       A3: b = ( LDir X9) and

       A4: X9 is being_line by Th14;

      consider x,y be Element of AS such that

       A5: x in X9 and y in X9 and x <> y by A4, AFF_1: 19;

      

       A6: x in (x * X) by A2, AFF_4:def 3;

      (x * X) is being_line by A2, AFF_4: 27;

      then

      consider Z such that

       A7: X9 c= Z and

       A8: (x * X) c= Z and

       A9: Z is being_plane by A4, A5, A6, AFF_4: 38;

      

       A10: X9 '||' Z by A4, A7, A9, AFF_4: 42;

      reconsider A = ( PDir Z) as Element of the Lines of ( ProjHorizon AS) by A9, Th15;

      take A;

      X // (x * X) by A2, AFF_4:def 3;

      then X '||' Z by A2, A8, A9, AFF_4: 41;

      hence thesis by A1, A2, A3, A4, A9, A10, Th36;

    end;

    

     Lm1: not AS is AffinPlane implies ex a be Element of the Points of ( ProjHorizon AS), A be Element of the Lines of ( ProjHorizon AS) st not a on A

    proof

      set x = the Element of AS;

      consider X such that

       A1: x in X and x in X and x in X and

       A2: X is being_plane by AFF_4: 37;

      reconsider A = ( PDir X) as Element of the Lines of ( ProjHorizon AS) by A2, Th15;

      assume not AS is AffinPlane;

      then

      consider t such that

       A3: not t in X by A2, AFF_4: 48;

      set Y = ( Line (x,t));

      

       A4: Y is being_line by A1, A3, AFF_1:def 3;

      then

      reconsider a = ( LDir Y) as Element of the Points of ( ProjHorizon AS) by Th14;

      take a, A;

      

       A5: t in Y by AFF_1: 15;

      

       A6: x in Y by AFF_1: 15;

      thus not a on A

      proof

        assume not thesis;

        then Y '||' X by A2, A4, Th36;

        then Y c= X by A1, A2, A4, A6, AFF_4: 43;

        hence contradiction by A3, A5;

      end;

    end;

    

     Lm2: a on A & a on K & b on A & b on K implies a = b or A = K

    proof

      assume that

       A1: a on A and

       A2: a on K and

       A3: b on A and

       A4: b on K;

      consider X such that

       A5: A = [X, 1] & X is being_line or A = [( PDir X), 2] & X is being_plane by Th23;

      consider X9 such that

       A6: K = [X9, 1] & X9 is being_line or K = [( PDir X9), 2] & X9 is being_plane by Th23;

      assume

       A7: a <> b;

       A8:

      now

        given Y such that

         A9: a = ( LDir Y) and

         A10: Y is being_line;

         A11:

        now

          given Y9 such that

           A12: b = ( LDir Y9) and

           A13: Y9 is being_line;

          

           A14: not Y // Y9 by A7, A9, A10, A12, A13, Th11;

          

           A15: M = [Z, 1] & Z is being_line implies not (a on M & b on M)

          proof

            assume that

             A16: M = [Z, 1] and

             A17: Z is being_line;

            assume

             A18: not thesis;

            then Y9 '||' Z by A12, A13, A16, A17, Th28;

            then

             A19: Y9 // Z by A13, A17, AFF_4: 40;

            Y '||' Z by A9, A10, A16, A17, A18, Th28;

            then Y // Z by A10, A17, AFF_4: 40;

            then Y // Y9 by A19, AFF_1: 44;

            hence contradiction by A7, A9, A10, A12, A13, Th11;

          end;

          then

           A20: Y9 '||' X by A1, A3, A5, A12, A13, Th29;

          

           A21: Y9 '||' X9 by A2, A4, A6, A12, A13, A15, Th29;

          

           A22: Y '||' X9 by A2, A4, A6, A9, A10, A15, Th29;

          Y '||' X by A1, A3, A5, A9, A10, A15, Th29;

          then X '||' X9 by A1, A2, A3, A4, A5, A6, A10, A13, A15, A14, A22, A20, A21, Th5;

          hence thesis by A1, A2, A3, A4, A5, A6, A15, Th13;

        end;

        now

          assume b is Element of AS;

          then

          reconsider y = b as Element of AS;

          

           A23: y in X9 by A4, A6, Th26, Th27;

          

           A24: y = b;

          then Y '||' X9 by A2, A4, A6, A9, A10, Th27, Th28;

          then

           A25: Y // X9 by A4, A6, A10, A24, Th27, AFF_4: 40;

          Y '||' X by A1, A3, A5, A9, A10, A24, Th27, Th28;

          then Y // X by A3, A5, A10, A24, Th27, AFF_4: 40;

          then

           A26: X // X9 by A25, AFF_1: 44;

          y in X by A3, A5, Th26, Th27;

          hence thesis by A3, A4, A5, A6, A23, A26, Th27, AFF_1: 45;

        end;

        hence thesis by A11, Th20;

      end;

      now

        assume a is Element of AS;

        then

        reconsider x = a as Element of AS;

        

         A27: x = a;

        

         A28: x in X9 by A2, A6, Th26, Th27;

        

         A29: x in X by A1, A5, Th26, Th27;

         A30:

        now

          given Y such that

           A31: b = ( LDir Y) and

           A32: Y is being_line;

          Y '||' X9 by A2, A4, A6, A27, A31, A32, Th27, Th28;

          then

           A33: Y // X9 by A2, A6, A27, A32, Th27, AFF_4: 40;

          Y '||' X by A1, A3, A5, A27, A31, A32, Th27, Th28;

          then Y // X by A1, A5, A27, A32, Th27, AFF_4: 40;

          then X // X9 by A33, AFF_1: 44;

          hence thesis by A1, A2, A5, A6, A29, A28, Th27, AFF_1: 45;

        end;

        now

          assume b is Element of AS;

          then

          reconsider y = b as Element of AS;

          

           A34: y in X9 by A4, A6, Th26, Th27;

          y in X by A3, A5, Th26, Th27;

          hence thesis by A1, A2, A7, A5, A6, A29, A28, A34, Th27, AFF_1: 18;

        end;

        hence thesis by A30, Th20;

      end;

      hence thesis by A8, Th20;

    end;

    

     Lm3: ex a, b, c st a on A & b on A & c on A & a <> b & b <> c & c <> a

    proof

      consider X such that

       A1: A = [X, 1] & X is being_line or A = [( PDir X), 2] & X is being_plane by Th23;

       A2:

      now

        assume that

         A3: A = [( PDir X), 2] and

         A4: X is being_plane;

        consider x, y, z such that

         A5: x in X and

         A6: y in X and

         A7: z in X and

         A8: not LIN (x,y,z) by A4, AFF_4: 34;

        

         A9: y <> z by A8, AFF_1: 7;

        then

         A10: ( Line (y,z)) is being_line by AFF_1:def 3;

        then

         A11: ( Line (y,z)) '||' X by A4, A6, A7, A9, AFF_4: 19, AFF_4: 42;

        

         A12: z <> x by A8, AFF_1: 7;

        then

         A13: ( Line (x,z)) is being_line by AFF_1:def 3;

        then

         A14: ( Line (x,z)) '||' X by A4, A5, A7, A12, AFF_4: 19, AFF_4: 42;

        

         A15: x <> y by A8, AFF_1: 7;

        then

         A16: ( Line (x,y)) is being_line by AFF_1:def 3;

        then

        reconsider a = ( LDir ( Line (x,y))), b = ( LDir ( Line (y,z))), c = ( LDir ( Line (x,z))) as POINT of ( IncProjSp_of AS) by A10, A13, Th20;

        take a, b, c;

        ( Line (x,y)) '||' X by A4, A5, A6, A15, A16, AFF_4: 19, AFF_4: 42;

        hence a on A & b on A & c on A by A3, A4, A16, A10, A13, A11, A14, Th29;

        

         A17: x in ( Line (x,y)) by AFF_1: 15;

        

         A18: z in ( Line (y,z)) by AFF_1: 15;

        

         A19: y in ( Line (x,y)) by AFF_1: 15;

        

         A20: y in ( Line (y,z)) by AFF_1: 15;

        thus a <> b

        proof

          assume not thesis;

          then ( Line (x,y)) // ( Line (y,z)) by A16, A10, Th11;

          then z in ( Line (x,y)) by A19, A20, A18, AFF_1: 45;

          hence contradiction by A8, A16, A17, A19, AFF_1: 21;

        end;

        

         A21: z in ( Line (x,z)) by AFF_1: 15;

        

         A22: x in ( Line (x,z)) by AFF_1: 15;

        thus b <> c

        proof

          assume not thesis;

          then ( Line (y,z)) // ( Line (x,z)) by A10, A13, Th11;

          then x in ( Line (y,z)) by A18, A22, A21, AFF_1: 45;

          hence contradiction by A8, A10, A20, A18, AFF_1: 21;

        end;

        thus c <> a

        proof

          assume not thesis;

          then ( Line (x,y)) // ( Line (x,z)) by A16, A13, Th11;

          then z in ( Line (x,y)) by A17, A22, A21, AFF_1: 45;

          hence contradiction by A8, A16, A17, A19, AFF_1: 21;

        end;

      end;

      now

        assume that

         A23: A = [X, 1] and

         A24: X is being_line;

        reconsider c = ( LDir X) as POINT of ( IncProjSp_of AS) by A24, Th20;

        consider x, y such that

         A25: x in X and

         A26: y in X and

         A27: x <> y by A24, AFF_1: 19;

        reconsider a = x, b = y as Element of the Points of ( IncProjSp_of AS) by Th20;

        take a, b, c;

        X // X by A24, AFF_1: 41;

        then X '||' X by A24, AFF_4: 40;

        hence a on A & b on A & c on A by A23, A24, A25, A26, Th26, Th28;

        thus a <> b by A27;

        thus b <> c & c <> a

        proof

          assume

           A28: not thesis;

          c in ( Dir_of_Lines AS) by A24, Th14;

          then (the carrier of AS /\ ( Dir_of_Lines AS)) <> {} by A28, XBOOLE_0:def 4;

          then the carrier of AS meets ( Dir_of_Lines AS) by XBOOLE_0:def 7;

          hence contradiction by Th16;

        end;

      end;

      hence thesis by A1, A2;

    end;

    

     Lm4: ex A st a on A & b on A

    proof

       A1:

      now

        given X such that

         A2: a = ( LDir X) and

         A3: X is being_line;

         A4:

        now

          given X9 such that

           A5: b = ( LDir X9) and

           A6: X9 is being_line;

          consider x,y be Element of AS such that

           A7: x in X9 and y in X9 and x <> y by A6, AFF_1: 19;

          

           A8: x in (x * X) by A3, AFF_4:def 3;

          (x * X) is being_line by A3, AFF_4: 27;

          then

          consider Z such that

           A9: X9 c= Z and

           A10: (x * X) c= Z and

           A11: Z is being_plane by A6, A7, A8, AFF_4: 38;

          

           A12: X9 '||' Z by A6, A9, A11, AFF_4: 42;

          reconsider A = [( PDir Z), 2] as LINE of ( IncProjSp_of AS) by A11, Th23;

          take A;

          X // (x * X) by A3, AFF_4:def 3;

          then X '||' Z by A3, A10, A11, AFF_4: 41;

          hence a on A & b on A by A2, A3, A5, A6, A11, A12, Th29;

        end;

        now

          assume b is Element of AS;

          then

          reconsider y = b as Element of AS;

          

           A13: (y * X) is being_line by A3, AFF_4: 27;

          then

          reconsider A = [(y * X), 1] as LINE of ( IncProjSp_of AS) by Th23;

          take A;

          X // (y * X) by A3, AFF_4:def 3;

          then X '||' (y * X) by A3, A13, AFF_4: 40;

          hence a on A by A2, A3, A13, Th28;

          y in (y * X) by A3, AFF_4:def 3;

          hence b on A by A13, Th26;

        end;

        hence thesis by A4, Th20;

      end;

      now

        assume a is Element of AS;

        then

        reconsider x = a as Element of AS;

         A14:

        now

          given X9 such that

           A15: b = ( LDir X9) and

           A16: X9 is being_line;

          

           A17: (x * X9) is being_line by A16, AFF_4: 27;

          then

          reconsider A = [(x * X9), 1] as LINE of ( IncProjSp_of AS) by Th23;

          take A;

          x in (x * X9) by A16, AFF_4:def 3;

          hence a on A by A17, Th26;

          X9 // (x * X9) by A16, AFF_4:def 3;

          then X9 '||' (x * X9) by A16, A17, AFF_4: 40;

          hence b on A by A15, A16, A17, Th28;

        end;

        now

          assume b is Element of AS;

          then

          reconsider y = b as Element of AS;

          consider Y such that

           A18: x in Y and

           A19: y in Y and

           A20: Y is being_line by AFF_4: 11;

          reconsider A = [Y, 1] as LINE of ( IncProjSp_of AS) by A20, Th23;

          take A;

          thus a on A & b on A by A18, A19, A20, Th26;

        end;

        hence thesis by A14, Th20;

      end;

      hence thesis by A1, Th20;

    end;

    

     Lm5: AS is AffinPlane implies ex a st a on A & a on K

    proof

      consider X such that

       A1: A = [X, 1] & X is being_line or A = [( PDir X), 2] & X is being_plane by Th23;

      consider X9 such that

       A2: K = [X9, 1] & X9 is being_line or K = [( PDir X9), 2] & X9 is being_plane by Th23;

      assume

       A3: AS is AffinPlane;

       A4:

      now

        assume that

         A5: A = [X, 1] and

         A6: X is being_line;

         A7:

        now

          assume that

           A8: K = [X9, 1] and

           A9: X9 is being_line;

           A10:

          now

            reconsider a = ( LDir X), b = ( LDir X9) as Element of the Points of ( IncProjSp_of AS) by A6, A9, Th20;

            X9 // X9 by A9, AFF_1: 41;

            then

             A11: X9 '||' X9 by A9, AFF_4: 40;

            assume X // X9;

            then

             A12: a = b by A6, A9, Th11;

            take a;

            X // X by A6, AFF_1: 41;

            then X '||' X by A6, AFF_4: 40;

            hence a on A & a on K by A5, A6, A8, A9, A12, A11, Th28;

          end;

          now

            assume not X // X9;

            then

            consider x such that

             A13: x in X and

             A14: x in X9 by A3, A6, A9, AFF_1: 58;

            reconsider a = x as Element of the Points of ( IncProjSp_of AS) by Th20;

            take a;

            thus a on A & a on K by A5, A6, A8, A9, A13, A14, Th26;

          end;

          hence thesis by A10;

        end;

        now

          X // X by A6, AFF_1: 41;

          then

           A15: X '||' X by A6, AFF_4: 40;

          reconsider a = ( LDir X) as Element of the Points of ( IncProjSp_of AS) by A6, Th20;

          assume that

           A16: K = [( PDir X9), 2] and

           A17: X9 is being_plane;

          take a;

          X9 = the carrier of AS by A3, A17, Th2;

          then X '||' X9 by A6, A17, AFF_4: 42;

          hence a on A & a on K by A5, A6, A16, A17, A15, Th28, Th29;

        end;

        hence thesis by A2, A7;

      end;

      now

        assume that

         A18: A = [( PDir X), 2] and

         A19: X is being_plane;

        

         A20: X = the carrier of AS by A3, A19, Th2;

         A21:

        now

          assume that

           A22: K = [X9, 1] and

           A23: X9 is being_line;

          X9 // X9 by A23, AFF_1: 41;

          then

           A24: X9 '||' X9 by A23, AFF_4: 40;

          reconsider a = ( LDir X9) as POINT of ( IncProjSp_of AS) by A23, Th20;

          take a;

          X9 '||' X by A19, A20, A23, AFF_4: 42;

          hence a on A & a on K by A18, A19, A22, A23, A24, Th28, Th29;

        end;

        now

          consider a, b, c such that

           A25: a on A and b on A and c on A and a <> b and b <> c and c <> a by Lm3;

          assume that

           A26: K = [( PDir X9), 2] and

           A27: X9 is being_plane;

          take a;

          thus a on A & a on K by A3, A18, A19, A26, A27, A25, Th3;

        end;

        hence thesis by A2, A21;

      end;

      hence thesis by A1, A4;

    end;

    

     Lm6: ex a, A st not a on A

    proof

      consider x, y, z such that

       A1: not LIN (x,y,z) by AFF_1: 12;

      y <> z by A1, AFF_1: 7;

      then

       A2: ( Line (y,z)) is being_line by AFF_1:def 3;

      then

      reconsider A = [( Line (y,z)), 1] as LINE of ( IncProjSp_of AS) by Th23;

      reconsider a = x as POINT of ( IncProjSp_of AS) by Th20;

      take a, A;

      thus not a on A

      proof

        assume not thesis;

        then

         A3: x in ( Line (y,z)) by Th26;

        

         A4: z in ( Line (y,z)) by AFF_1: 15;

        y in ( Line (y,z)) by AFF_1: 15;

        hence contradiction by A1, A2, A3, A4, AFF_1: 21;

      end;

    end;

    theorem :: AFPROJ:41

    

     Th41: for x,y be Element of the Points of ( ProjHorizon AS), X be Element of the Lines of ( IncProjSp_of AS) st x <> y & [x, X] in the Inc of ( IncProjSp_of AS) & [y, X] in the Inc of ( IncProjSp_of AS) holds ex Y be Element of the Lines of ( ProjHorizon AS) st X = [Y, 2]

    proof

      let x,y be Element of the Points of ( ProjHorizon AS), X be Element of the Lines of ( IncProjSp_of AS);

      reconsider a = x, b = y as POINT of ( IncProjSp_of AS) by Th22;

      assume that

       A1: x <> y and

       A2: [x, X] in the Inc of ( IncProjSp_of AS) and

       A3: [y, X] in the Inc of ( IncProjSp_of AS);

      

       A4: b on X by A3, INCSP_1:def 1;

      consider Y be Element of the Lines of ( ProjHorizon AS) such that

       A5: x on Y and

       A6: y on Y by Th40;

      reconsider A = [Y, 2] as LINE of ( IncProjSp_of AS) by Th25;

      consider Z be Subset of AS such that

       A7: Y = ( PDir Z) and

       A8: Z is being_plane by Th15;

      consider X2 be Subset of AS such that

       A9: y = ( LDir X2) and

       A10: X2 is being_line by Th14;

      X2 '||' Z by A9, A10, A6, A7, A8, Th36;

      then

       A11: b on A by A9, A10, A7, A8, Th29;

      take Y;

      consider X1 be Subset of AS such that

       A12: x = ( LDir X1) and

       A13: X1 is being_line by Th14;

      X1 '||' Z by A12, A13, A5, A7, A8, Th36;

      then

       A14: a on A by A12, A13, A7, A8, Th29;

      a on X by A2, INCSP_1:def 1;

      hence thesis by A1, A4, A14, A11, Lm2;

    end;

    theorem :: AFPROJ:42

    

     Th42: for x be POINT of ( IncProjSp_of AS), X be Element of the Lines of ( ProjHorizon AS) st [x, [X, 2]] in the Inc of ( IncProjSp_of AS) holds x is Element of the Points of ( ProjHorizon AS)

    proof

      let x be POINT of ( IncProjSp_of AS), X be Element of the Lines of ( ProjHorizon AS) such that

       A1: [x, [X, 2]] in the Inc of ( IncProjSp_of AS);

      reconsider A = [X, 2] as LINE of ( IncProjSp_of AS) by Th25;

      

       A2: ex Y st X = ( PDir Y) & Y is being_plane by Th15;

       not x is Element of AS

      proof

        assume not thesis;

        then

        reconsider a = x as Element of AS;

        

         A3: a = x;

        x on A by A1, INCSP_1:def 1;

        hence contradiction by A2, A3, Th27;

      end;

      then ex Y9 st x = ( LDir Y9) & Y9 is being_line by Th20;

      hence thesis by Th14;

    end;

    

     Lm7: X is being_line & X9 is being_line & Y is being_plane & X c= Y & X9 c= Y & A = [X, 1] & K = [X9, 1] & b on A & c on K & b on M & c on M & b <> c & M = [Y9, 1] & Y9 is being_line implies Y9 c= Y

    proof

      assume that

       A1: X is being_line and

       A2: X9 is being_line and

       A3: Y is being_plane and

       A4: X c= Y and

       A5: X9 c= Y and

       A6: A = [X, 1] and

       A7: K = [X9, 1] and

       A8: b on A and

       A9: c on K and

       A10: b on M and

       A11: c on M and

       A12: b <> c and

       A13: M = [Y9, 1] and

       A14: Y9 is being_line;

       A15:

      now

        assume b is Element of AS;

        then

        reconsider y = b as Element of AS;

         A16:

        now

          given Xc be Subset of AS such that

           A17: c = ( LDir Xc) and

           A18: Xc is being_line;

          Xc '||' X9 by A2, A7, A9, A17, A18, Th28;

          then

           A19: Xc // X9 by A2, A18, AFF_4: 40;

          Xc '||' Y9 by A11, A13, A14, A17, A18, Th28;

          then Xc // Y9 by A14, A18, AFF_4: 40;

          then

           A20: X9 // Y9 by A19, AFF_1: 44;

          y in Y9 by A10, A13, Th26;

          then

           A21: Y9 = (y * X9) by A2, A20, AFF_4:def 3;

          y in X by A6, A8, Th26;

          hence thesis by A2, A3, A4, A5, A21, AFF_4: 28;

        end;

        now

          assume c is Element of AS;

          then

          reconsider z = c as Element of AS;

          

           A22: z in Y9 by A11, A13, Th26;

          y in Y9 by A10, A13, Th26;

          then

           A23: Y9 = ( Line (y,z)) by A12, A14, A22, AFF_1: 57;

          

           A24: z in X9 by A7, A9, Th26;

          y in X by A6, A8, Th26;

          hence thesis by A3, A4, A5, A12, A24, A23, AFF_4: 19;

        end;

        hence thesis by A16, Th20;

      end;

      now

        given Xb be Subset of AS such that

         A25: b = ( LDir Xb) and

         A26: Xb is being_line;

         A27:

        now

          assume c is Element of AS;

          then

          reconsider y = c as Element of AS;

          Xb '||' X by A1, A6, A8, A25, A26, Th28;

          then

           A28: Xb // X by A1, A26, AFF_4: 40;

          Xb '||' Y9 by A10, A13, A14, A25, A26, Th28;

          then Xb // Y9 by A14, A26, AFF_4: 40;

          then

           A29: X // Y9 by A28, AFF_1: 44;

          y in Y9 by A11, A13, Th26;

          then

           A30: Y9 = (y * X) by A1, A29, AFF_4:def 3;

          y in X9 by A7, A9, Th26;

          hence thesis by A1, A3, A4, A5, A30, AFF_4: 28;

        end;

        now

          Xb '||' Y9 by A10, A13, A14, A25, A26, Th28;

          then

           A31: Xb // Y9 by A14, A26, AFF_4: 40;

          given Xc be Subset of AS such that

           A32: c = ( LDir Xc) and

           A33: Xc is being_line;

          Xc '||' Y9 by A11, A13, A14, A32, A33, Th28;

          then Xc // Y9 by A14, A33, AFF_4: 40;

          then Xc // Xb by A31, AFF_1: 44;

          hence contradiction by A12, A25, A26, A32, A33, Th11;

        end;

        hence thesis by A27, Th20;

      end;

      hence thesis by A15, Th20;

    end;

    

     Lm8: X is being_line & X9 is being_line & Y is being_plane & X c= Y & X9 c= Y & A = [X, 1] & K = [X9, 1] & b on A & c on K & b on M & c on M & b <> c & M = [( PDir Y9), 2] & Y9 is being_plane implies Y9 '||' Y & Y '||' Y9

    proof

      assume that

       A1: X is being_line and

       A2: X9 is being_line and

       A3: Y is being_plane and

       A4: X c= Y and

       A5: X9 c= Y and

       A6: A = [X, 1] and

       A7: K = [X9, 1] and

       A8: b on A and

       A9: c on K and

       A10: b on M and

       A11: c on M and

       A12: b <> c and

       A13: M = [( PDir Y9), 2] and

       A14: Y9 is being_plane;

      b is Element of AS or ex Xb be Subset of AS st b = ( LDir Xb) & Xb is being_line by Th20;

      then

      consider Xb be Subset of AS such that

       A15: b = ( LDir Xb) and

       A16: Xb is being_line by A10, A13, Th27;

      

       A17: Xb '||' Y9 by A10, A13, A14, A15, A16, Th29;

      Xb '||' X by A1, A6, A8, A15, A16, Th28;

      then Xb // X by A1, A16, AFF_4: 40;

      then

       A18: Xb '||' Y by A1, A3, A4, AFF_4: 42, AFF_4: 56;

      c is Element of AS or ex Xc be Subset of AS st c = ( LDir Xc) & Xc is being_line by Th20;

      then

      consider Xc be Subset of AS such that

       A19: c = ( LDir Xc) and

       A20: Xc is being_line by A11, A13, Th27;

      

       A21: Xc '||' Y9 by A11, A13, A14, A19, A20, Th29;

      Xc '||' X9 by A2, A7, A9, A19, A20, Th28;

      then Xc // X9 by A2, A20, AFF_4: 40;

      then

       A22: Xc '||' Y by A2, A3, A5, AFF_4: 42, AFF_4: 56;

       not Xb // Xc by A12, A15, A16, A19, A20, Th11;

      hence thesis by A3, A14, A16, A20, A17, A21, A18, A22, Th5;

    end;

    theorem :: AFPROJ:43

    

     Th43: Y is being_plane & X is being_line & X9 is being_line & X c= Y & X9 c= Y & P = [X, 1] & Q = [X9, 1] implies ex q st q on P & q on Q

    proof

      assume that

       A1: Y is being_plane and

       A2: X is being_line and

       A3: X9 is being_line and

       A4: X c= Y and

       A5: X9 c= Y and

       A6: P = [X, 1] and

       A7: Q = [X9, 1];

       A8:

      now

        reconsider q = ( LDir X) as POINT of ( IncProjSp_of AS) by A2, Th20;

        assume

         A9: X // X9;

        take q;

        ( LDir X) = ( LDir X9) by A2, A3, A9, Th11;

        hence q on P & q on Q by A2, A3, A6, A7, Th30;

      end;

      now

        given y such that

         A10: y in X and

         A11: y in X9;

        reconsider q = y as Element of the Points of ( IncProjSp_of AS) by Th20;

        take q;

        thus q on P & q on Q by A2, A3, A6, A7, A10, A11, Th26;

      end;

      hence thesis by A1, A2, A3, A4, A5, A8, AFF_4: 22;

    end;

    

     Lm9: a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N & p is Element of AS implies ex q st q on P & q on Q

    proof

      assume that

       A1: a on M and

       A2: b on M and

       A3: c on N and

       A4: d on N and

       A5: p on M and

       A6: p on N and

       A7: a on P and

       A8: c on P and

       A9: b on Q and

       A10: d on Q and

       A11: not p on P and

       A12: not p on Q and

       A13: M <> N and

       A14: p is Element of AS;

      

       A15: b <> d by A2, A4, A5, A6, A9, A12, A13, Lm2;

      reconsider x = p as Element of AS by A14;

      consider XM be Subset of AS such that

       A16: M = [XM, 1] & XM is being_line or M = [( PDir XM), 2] & XM is being_plane by Th23;

      consider XQ be Subset of AS such that

       A17: Q = [XQ, 1] & XQ is being_line or Q = [( PDir XQ), 2] & XQ is being_plane by Th23;

      consider XP be Subset of AS such that

       A18: P = [XP, 1] & XP is being_line or P = [( PDir XP), 2] & XP is being_plane by Th23;

      consider XN be Subset of AS such that

       A19: N = [XN, 1] & XN is being_line or N = [( PDir XN), 2] & XN is being_plane by Th23;

      

       A20: x in XM by A5, A16, Th26, Th27;

      x in XN by A6, A19, Th26, Th27;

      then

      consider Y such that

       A21: XM c= Y and

       A22: XN c= Y and

       A23: Y is being_plane by A5, A6, A16, A19, A20, Th27, AFF_4: 38;

      

       A24: a <> c by A1, A3, A5, A6, A7, A11, A13, Lm2;

       A25:

      now

        assume that

         A26: P = [( PDir XP), 2] and

         A27: XP is being_plane;

        

         A28: Y '||' XP by A1, A3, A5, A6, A7, A8, A24, A16, A19, A20, A21, A22, A23, A26, A27, Lm8, Th27;

         A29:

        now

          assume that

           A30: Q = [XQ, 1] and

           A31: XQ is being_line;

          reconsider q = ( LDir XQ) as POINT of ( IncProjSp_of AS) by A31, Th20;

          take q;

          XQ c= Y by A2, A4, A5, A6, A9, A10, A15, A16, A19, A20, A21, A22, A23, A30, A31, Lm7, Th27;

          then XQ '||' Y by A23, A31, AFF_4: 42;

          then XQ '||' XP by A23, A28, AFF_4: 59, AFF_4: 60;

          hence q on P by A26, A27, A31, Th29;

          thus q on Q by A30, A31, Th30;

        end;

        now

          consider q, r, p9 such that

           A32: q on P and r on P and p9 on P and q <> r and r <> p9 and p9 <> q by Lm3;

          assume that

           A33: Q = [( PDir XQ), 2] and

           A34: XQ is being_plane;

          take q;

          thus q on P by A32;

          Y '||' XQ by A2, A4, A5, A6, A9, A10, A15, A16, A19, A20, A21, A22, A23, A33, A34, Lm8, Th27;

          then XP '||' XQ by A23, A27, A28, A34, AFF_4: 61;

          hence q on Q by A26, A27, A33, A34, A32, Th13;

        end;

        hence thesis by A17, A29;

      end;

      now

        assume that

         A35: P = [XP, 1] and

         A36: XP is being_line;

        

         A37: XP c= Y by A1, A3, A5, A6, A7, A8, A24, A16, A19, A20, A21, A22, A23, A35, A36, Lm7, Th27;

         A38:

        now

          

           A39: XP '||' Y by A23, A36, A37, AFF_4: 42;

          reconsider q = ( LDir XP) as POINT of ( IncProjSp_of AS) by A36, Th20;

          assume that

           A40: Q = [( PDir XQ), 2] and

           A41: XQ is being_plane;

          take q;

          thus q on P by A35, A36, Th30;

          Y '||' XQ by A2, A4, A5, A6, A9, A10, A15, A16, A19, A20, A21, A22, A23, A40, A41, Lm8, Th27;

          then XP '||' XQ by A23, A39, AFF_4: 59, AFF_4: 60;

          hence q on Q by A36, A40, A41, Th29;

        end;

        now

          assume that

           A42: Q = [XQ, 1] and

           A43: XQ is being_line;

          XQ c= Y by A2, A4, A5, A6, A9, A10, A15, A16, A19, A20, A21, A22, A23, A42, A43, Lm7, Th27;

          hence thesis by A23, A35, A36, A37, A42, A43, Th43;

        end;

        hence thesis by A17, A38;

      end;

      hence thesis by A18, A25;

    end;

    

     Lm10: a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N & not p is Element of AS & a is Element of AS implies ex q st q on P & q on Q

    proof

      assume that

       A1: a on M and

       A2: b on M and

       A3: c on N and

       A4: d on N and

       A5: p on M and

       A6: p on N and

       A7: a on P and

       A8: c on P and

       A9: b on Q and

       A10: d on Q and

       A11: not p on P and

       A12: not p on Q and

       A13: M <> N and

       A14: not p is Element of AS and

       A15: a is Element of AS;

      reconsider x = a as Element of AS by A15;

      consider XM be Subset of AS such that

       A16: M = [XM, 1] & XM is being_line or M = [( PDir XM), 2] & XM is being_plane by Th23;

      

       A17: x in XM by A1, A16, Th26, Th27;

      

       A18: b <> d by A2, A4, A5, A6, A9, A12, A13, Lm2;

      consider XN be Subset of AS such that

       A19: N = [XN, 1] & XN is being_line or N = [( PDir XN), 2] & XN is being_plane by Th23;

      consider XP be Subset of AS such that

       A20: P = [XP, 1] & XP is being_line or P = [( PDir XP), 2] & XP is being_plane by Th23;

      

       A21: x = a;

      then

      reconsider y = b as Element of AS by A1, A2, A5, A9, A12, A14, A16, Th27, Th35;

      

       A22: y in XM by A2, A16, Th26, Th27;

      consider X such that

       A23: p = ( LDir X) and

       A24: X is being_line by A14, Th20;

      consider XQ be Subset of AS such that

       A25: Q = [XQ, 1] & XQ is being_line or Q = [( PDir XQ), 2] & XQ is being_plane by Th23;

      

       A26: x in XP by A7, A20, Th26, Th27;

      then

      consider Y such that

       A27: XM c= Y and

       A28: XP c= Y and

       A29: Y is being_plane by A1, A7, A16, A20, A17, Th27, AFF_4: 38;

      

       A30: y = b;

      

       A31: X '||' XM by A1, A5, A23, A24, A16, A21, Th27, Th28;

      then

       A32: X // XM by A1, A24, A16, A21, Th27, AFF_4: 40;

      

       A33: y in XQ by A9, A25, Th26, Th27;

      

       A34: not XM // XP by A1, A5, A7, A11, A16, A20, A17, A26, Th27, AFF_1: 45;

       A35:

      now

        

         A36: X // XM by A1, A24, A16, A21, A31, Th27, AFF_4: 40;

        assume that

         A37: N = [XN, 1] and

         A38: XN is being_line;

        X '||' XN by A6, A23, A24, A37, A38, Th28;

        then X // XN by A24, A38, AFF_4: 40;

        then

         A39: XM // XN by A36, AFF_1: 44;

        c is Element of AS

        proof

          assume not thesis;

          then c = ( LDir XN) by A3, A37, A38, Th34;

          then XN '||' XP by A7, A8, A20, A21, A38, Th27, Th28;

          then XN // XP by A7, A20, A21, A38, Th27, AFF_4: 40;

          hence contradiction by A34, A39, AFF_1: 44;

        end;

        then

        reconsider z = c as Element of AS;

        z in XN by A3, A37, Th26;

        then

         A40: XN = (z * XM) by A1, A16, A21, A39, Th27, AFF_4:def 3;

        

         A41: not XN // XQ

        proof

          assume XN // XQ;

          then XM // XQ by A39, AFF_1: 44;

          hence contradiction by A2, A5, A9, A12, A16, A25, A33, A22, Th27, AFF_1: 45;

        end;

        now

          assume not d is Element of AS;

          then

          consider Xd be Subset of AS such that

           A42: d = ( LDir Xd) and

           A43: Xd is being_line by Th20;

          Xd '||' XN by A4, A37, A38, A42, A43, Th28;

          then

           A44: Xd // XN by A38, A43, AFF_4: 40;

          Xd '||' XQ by A9, A10, A25, A30, A42, A43, Th27, Th28;

          then Xd // XQ by A9, A25, A30, A43, Th27, AFF_4: 40;

          hence contradiction by A41, A44, AFF_1: 44;

        end;

        then

        reconsider w = d as Element of AS;

        w in XQ by A10, A25, Th26, Th27;

        then

         A45: XQ = ( Line (y,w)) by A9, A18, A25, A33, Th27, AFF_1: 57;

        z in XP by A8, A20, Th26, Th27;

        then

         A46: XN c= Y by A1, A16, A21, A27, A28, A29, A40, Th27, AFF_4: 28;

        w in XN by A4, A37, Th26;

        then XQ c= Y by A18, A27, A29, A22, A46, A45, AFF_4: 19;

        hence thesis by A7, A9, A20, A25, A21, A28, A29, A30, Th27, Th43;

      end;

      

       A47: XP '||' Y by A7, A20, A21, A28, A29, Th27, AFF_4: 42;

      

       A48: XM '||' Y by A1, A16, A21, A27, A29, Th27, AFF_4: 42;

      now

        assume that

         A49: N = [( PDir XN), 2] and

         A50: XN is being_plane;

         not c is Element of AS by A3, A49, Th27;

        then c = ( LDir XP) by A7, A8, A20, A21, Th27, Th34;

        then

         A51: XP '||' XN by A3, A7, A20, A21, A49, A50, Th27, Th29;

         not d is Element of AS by A4, A49, Th27;

        then d = ( LDir XQ) by A9, A10, A25, A30, Th27, Th34;

        then

         A52: XQ '||' XN by A4, A9, A25, A30, A49, A50, Th27, Th29;

        X '||' XN by A6, A23, A24, A49, A50, Th29;

        then XM '||' XN by A32, AFF_4: 56;

        then XN '||' Y by A1, A5, A7, A11, A16, A20, A17, A26, A29, A48, A47, A50, A51, Th5, Th27, AFF_1: 45;

        then XQ '||' Y by A50, A52, AFF_4: 59, AFF_4: 60;

        then XQ c= Y by A9, A25, A27, A29, A33, A22, Th27, AFF_4: 43;

        hence thesis by A7, A9, A20, A25, A21, A28, A29, A30, Th27, Th43;

      end;

      hence thesis by A19, A35;

    end;

    

     Lm11: a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N & not p is Element of AS & (a is Element of AS or b is Element of AS or c is Element of AS or d is Element of AS) implies ex q st q on P & q on Q

    proof

      assume that

       A1: a on M and

       A2: b on M and

       A3: c on N and

       A4: d on N and

       A5: p on M and

       A6: p on N and

       A7: a on P and

       A8: c on P and

       A9: b on Q and

       A10: d on Q and

       A11: not p on P and

       A12: not p on Q and

       A13: M <> N and

       A14: not p is Element of AS and

       A15: a is Element of AS or b is Element of AS or c is Element of AS or d is Element of AS;

      now

        assume b is Element of AS or d is Element of AS;

        then ex q st q on Q & q on P by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13, A14, Lm10;

        hence thesis;

      end;

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

    end;

    

     Lm12: a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N implies ex q st q on P & q on Q

    proof

      assume that

       A1: a on M and

       A2: b on M and

       A3: c on N and

       A4: d on N and

       A5: p on M and

       A6: p on N and

       A7: a on P and

       A8: c on P and

       A9: b on Q and

       A10: d on Q and

       A11: not p on P and

       A12: not p on Q and

       A13: M <> N;

      now

        assume

         A14: not p is Element of AS;

        now

          

           A15: b <> d by A2, A4, A5, A6, A9, A12, A13, Lm2;

          set x = the Element of AS;

          assume that

           A16: not a is Element of AS and

           A17: not b is Element of AS and

           A18: not c is Element of AS and

           A19: not d is Element of AS;

          consider Xa be Subset of AS such that

           A20: a = ( LDir Xa) and

           A21: Xa is being_line by A16, Th20;

          consider Xc be Subset of AS such that

           A22: c = ( LDir Xc) and

           A23: Xc is being_line by A18, Th20;

          consider Xb be Subset of AS such that

           A24: b = ( LDir Xb) and

           A25: Xb is being_line by A17, Th20;

          consider Xd be Subset of AS such that

           A26: d = ( LDir Xd) and

           A27: Xd is being_line by A19, Th20;

          consider Xp be Subset of AS such that

           A28: p = ( LDir Xp) and

           A29: Xp is being_line by A14, Th20;

          set Xa9 = (x * Xa), Xb9 = (x * Xb), Xc9 = (x * Xc), Xd9 = (x * Xd), Xp9 = (x * Xp);

          consider y such that

           A30: x <> y and

           A31: y in Xa9 by A21, AFF_1: 20, AFF_4: 27;

          

           A32: Xp // Xp9 by A29, AFF_4:def 3;

          consider t such that

           A33: x <> t and

           A34: t in Xc9 by A23, AFF_1: 20, AFF_4: 27;

          set Y1 = (y * Xp9), Y2 = (t * Xp9);

          

           A35: Xp9 is being_line by A29, AFF_4: 27;

          then

           A36: Y1 is being_line by AFF_4: 27;

          

           A37: Y2 is being_line by A35, AFF_4: 27;

          

           A38: Xb // Xb9 by A25, AFF_4:def 3;

          

           A39: Xd9 is being_line by A27, AFF_4: 27;

          

           A40: Xd // Xd9 by A27, AFF_4:def 3;

          

           A41: x in Xc9 by A23, AFF_4:def 3;

          

           A42: x in Xb9 by A25, AFF_4:def 3;

          

           A43: Xb9 is being_line by A25, AFF_4: 27;

          

           A44: x in Xd9 by A27, AFF_4:def 3;

          then

          consider XQ be Subset of AS such that

           A45: Xb9 c= XQ and

           A46: Xd9 c= XQ and

           A47: XQ is being_plane by A43, A39, A42, AFF_4: 38;

          

           A48: Xa9 is being_line by A21, AFF_4: 27;

          

           A49: Xp9 // Y2 by A35, AFF_4:def 3;

          

           A50: not Xd9 // Y2

          proof

            assume Xd9 // Y2;

            then Xd // Y2 by A40, AFF_1: 44;

            then Xd // Xp9 by A49, AFF_1: 44;

            then Xd // Xp by A32, AFF_1: 44;

            hence contradiction by A10, A12, A28, A29, A26, A27, Th11;

          end;

          

           A51: Xp9 // Y1 by A35, AFF_4:def 3;

          

           A52: not Xb9 // Y1

          proof

            assume Xb9 // Y1;

            then Xb // Y1 by A38, AFF_1: 44;

            then Xb // Xp9 by A51, AFF_1: 44;

            then Xb // Xp by A32, AFF_1: 44;

            hence contradiction by A9, A12, A28, A29, A24, A25, Th11;

          end;

          

           A53: x in Xa9 by A21, AFF_4:def 3;

          

           A54: Xc9 is being_line by A23, AFF_4: 27;

          then

          consider XP be Subset of AS such that

           A55: Xa9 c= XP and

           A56: Xc9 c= XP and

           A57: XP is being_plane by A48, A53, A41, AFF_4: 38;

          

           A58: x in Xp9 by A29, AFF_4:def 3;

          then

          consider X2 be Subset of AS such that

           A59: Xc9 c= X2 and

           A60: Xp9 c= X2 and

           A61: X2 is being_plane by A54, A35, A41, AFF_4: 38;

          

           A62: Xc // Xc9 by A23, AFF_4:def 3;

          N = [( PDir X2), 2]

          proof

            reconsider N9 = [( PDir X2), 2] as Element of the Lines of ( IncProjSp_of AS) by A61, Th23;

            

             A63: c on N9 by A22, A62, A59, A61, Th32;

            p on N9 by A28, A32, A60, A61, Th32;

            hence thesis by A3, A6, A8, A11, A63, Lm2;

          end;

          then Xd '||' X2 by A4, A26, A27, A61, Th29;

          then

           A64: Xd9 c= X2 by A39, A41, A44, A40, A59, A61, AFF_4: 43, AFF_4: 56;

          consider X1 be Subset of the carrier of AS such that

           A65: Xa9 c= X1 and

           A66: Xp9 c= X1 and

           A67: X1 is being_plane by A48, A35, A53, A58, AFF_4: 38;

          

           A68: Xa // Xa9 by A21, AFF_4:def 3;

          M = [( PDir X1), 2]

          proof

            reconsider M9 = [( PDir X1), 2] as Element of the Lines of ( IncProjSp_of AS) by A67, Th23;

            

             A69: a on M9 by A20, A68, A65, A67, Th32;

            p on M9 by A28, A32, A66, A67, Th32;

            hence thesis by A1, A5, A7, A11, A69, Lm2;

          end;

          then Xb '||' X1 by A2, A24, A25, A67, Th29;

          then

           A70: Xb9 c= X1 by A43, A53, A42, A38, A65, A67, AFF_4: 43, AFF_4: 56;

          Y1 c= X1 by A29, A31, A65, A66, A67, AFF_4: 27, AFF_4: 28;

          then

          consider z such that

           A71: z in Xb9 and

           A72: z in Y1 by A43, A36, A67, A70, A52, AFF_4: 22;

          Y2 c= X2 by A29, A34, A59, A60, A61, AFF_4: 27, AFF_4: 28;

          then

          consider u such that

           A73: u in Xd9 and

           A74: u in Y2 by A39, A37, A61, A64, A50, AFF_4: 22;

          set AC = ( Line (y,t)), BD = ( Line (z,u));

          

           A75: y in AC by AFF_1: 15;

          

           A76: y in Y1 by A35, AFF_4:def 3;

          

           A77: x <> z

          proof

            assume

             A78: not thesis;

            a = ( LDir Xa9) by A20, A21, A48, A68, Th11

            .= ( LDir Y1) by A48, A53, A30, A31, A36, A76, A72, A78, AFF_1: 18

            .= ( LDir Xp9) by A35, A36, A51, Th11

            .= p by A28, A29, A35, A32, Th11;

            hence contradiction by A7, A11;

          end;

          

           A79: z <> u

          proof

            assume

             A80: not thesis;

            b = ( LDir Xb9) by A24, A25, A43, A38, Th11

            .= ( LDir Xd9) by A43, A39, A42, A44, A71, A73, A77, A80, AFF_1: 18

            .= d by A26, A27, A39, A40, Th11;

            hence contradiction by A2, A4, A5, A6, A9, A12, A13, Lm2;

          end;

          then

           A81: BD is being_line by AFF_1:def 3;

          

           A82: Xa9 <> Xc9

          proof

            assume Xa9 = Xc9;

            

            then a = ( LDir Xc9) by A20, A21, A48, A68, Th11

            .= c by A22, A23, A54, A62, Th11;

            hence contradiction by A1, A3, A5, A6, A7, A11, A13, Lm2;

          end;

          then

           A83: y <> t by A48, A54, A53, A41, A30, A31, A34, AFF_1: 18;

          then

           A84: AC is being_line by AFF_1:def 3;

          

           A85: BD c= XQ by A71, A73, A79, A45, A46, A47, AFF_4: 19;

          

           A86: t in AC by AFF_1: 15;

          Y1 // Y2 by A51, A49, AFF_1: 44;

          then

          consider X3 be Subset of AS such that

           A87: Y1 c= X3 and

           A88: Y2 c= X3 and

           A89: X3 is being_plane by AFF_4: 39;

          

           A90: BD c= X3 by A87, A88, A89, A72, A74, A79, AFF_4: 19;

          

           A91: a <> c by A1, A3, A5, A6, A7, A11, A13, Lm2;

          

           A92: P = [( PDir XP), 2] & Q = [( PDir XQ), 2]

          proof

            reconsider P9 = [( PDir XP), 2], Q9 = [( PDir XQ), 2] as LINE of ( IncProjSp_of AS) by A57, A47, Th23;

            

             A93: c on P9 by A22, A62, A56, A57, Th32;

            

             A94: b on Q9 by A24, A38, A45, A47, Th32;

            

             A95: d on Q9 by A26, A40, A46, A47, Th32;

            a on P9 by A20, A68, A55, A57, Th32;

            hence thesis by A7, A8, A9, A10, A91, A15, A93, A94, A95, Lm2;

          end;

           A96:

          now

            reconsider q = ( LDir AC), q9 = ( LDir BD) as Element of the Points of ( IncProjSp_of AS) by A84, A81, Th20;

            assume

             A97: AC // BD;

            take q;

            q = q9 by A84, A81, A97, Th11;

            hence q on P & q on Q by A31, A34, A71, A73, A83, A79, A84, A81, A55, A56, A57, A45, A46, A47, A92, Th31, AFF_4: 19;

          end;

          

           A98: AC c= XP by A31, A34, A83, A55, A56, A57, AFF_4: 19;

           A99:

          now

            given w such that

             A100: w in AC and

             A101: w in BD;

            set R = ( Line (x,w));

            

             A102: x <> w

            proof

              assume

               A103: x = w;

              then Xa9 = AC by A48, A53, A30, A31, A84, A75, A100, AFF_1: 18;

              hence contradiction by A54, A41, A33, A34, A82, A84, A86, A100, A103, AFF_1: 18;

            end;

            then

             A104: R is being_line by AFF_1:def 3;

            then

            reconsider q = ( LDir R) as POINT of ( IncProjSp_of AS) by Th20;

            take q;

            thus q on P & q on Q by A53, A42, A55, A57, A45, A47, A92, A98, A85, A100, A101, A102, A104, Th31, AFF_4: 19;

          end;

          t in Y2 by A35, AFF_4:def 3;

          then AC c= X3 by A76, A87, A88, A89, A83, AFF_4: 19;

          hence thesis by A89, A84, A81, A90, A96, A99, AFF_4: 22;

        end;

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

      end;

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

    end;

    theorem :: AFPROJ:44

    

     Th44: for a,b,c,d,p be Element of the Points of ( ProjHorizon AS), M,N,P,Q be Element of the Lines of ( ProjHorizon AS) st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N holds ex q be Element of the Points of ( ProjHorizon AS) st q on P & q on Q

    proof

      let a,b,c,d,p be Element of the Points of ( ProjHorizon AS), M,N,P,Q be Element of the Lines of ( ProjHorizon AS) such that

       A1: a on M and

       A2: b on M and

       A3: c on N and

       A4: d on N and

       A5: p on M and

       A6: p on N and

       A7: a on P and

       A8: c on P and

       A9: b on Q and

       A10: d on Q and

       A11: not p on P and

       A12: not p on Q and

       A13: M <> N;

      reconsider M9 = [M, 2], N9 = [N, 2], P9 = [P, 2], Q9 = [Q, 2] as LINE of ( IncProjSp_of AS) by Th25;

      reconsider a9 = a, b9 = b, c9 = c, d9 = d, p9 = p as POINT of ( IncProjSp_of AS) by Th22;

      

       A14: b9 on M9 by A2, Th37;

      

       A15: M9 <> N9

      proof

        assume M9 = N9;

        

        then M = ( [N, 2] `1 )

        .= N;

        hence contradiction by A13;

      end;

      

       A16: d9 on N9 by A4, Th37;

      

       A17: c9 on N9 by A3, Th37;

      

       A18: c9 on P9 by A8, Th37;

      

       A19: a9 on P9 by A7, Th37;

      

       A20: p9 on N9 by A6, Th37;

      

       A21: p9 on M9 by A5, Th37;

      

       A22: not p9 on Q9 by A12, Th37;

      

       A23: not p9 on P9 by A11, Th37;

      

       A24: d9 on Q9 by A10, Th37;

      

       A25: b9 on Q9 by A9, Th37;

      a9 on M9 by A1, Th37;

      then

      consider q9 be POINT of ( IncProjSp_of AS) such that

       A26: q9 on P9 and

       A27: q9 on Q9 by A14, A17, A16, A21, A20, A19, A18, A25, A24, A23, A22, A15, Lm12;

       [q9, [P, 2]] in the Inc of ( IncProjSp_of AS) by A26, INCSP_1:def 1;

      then

      reconsider q = q9 as Element of the Points of ( ProjHorizon AS) by Th42;

      take q;

      thus thesis by A26, A27, Th37;

    end;

    registration

      let AS;

      cluster ( IncProjSp_of AS) -> partial linear up-2-dimensional up-3-rank Vebleian;

      correctness

      proof

        set XX = ( IncProjSp_of AS);

        

         A1: for a,b be POINT of XX holds ex A be LINE of XX st a on A & b on A by Lm4;

        

         A2: ex a be POINT of XX, A be LINE of XX st not a on A by Lm6;

        

         A3: for A be LINE of XX holds ex a,b,c be POINT of XX st a <> b & b <> c & c <> a & a on A & b on A & c on A

        proof

          let A be LINE of XX;

          consider a,b,c be POINT of XX such that

           A4: a on A and

           A5: b on A and

           A6: c on A and

           A7: a <> b and

           A8: b <> c and

           A9: c <> a by Lm3;

          take a, b, c;

          thus thesis by A4, A5, A6, A7, A8, A9;

        end;

        

         A10: for a,b,c,d,p,q be POINT of XX, M,N,P,Q be LINE of XX st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N holds ex q be POINT of XX st q on P & q on Q by Lm12;

        for a,b be POINT of XX, A,K be LINE of XX st a on A & b on A & a on K & b on K holds a = b or A = K by Lm2;

        hence thesis by A1, A2, A3, A10, INCPROJ:def 4, INCPROJ:def 5, INCPROJ:def 6, INCPROJ:def 7, INCPROJ:def 8;

      end;

    end

    registration

      cluster strict 2-dimensional for IncProjSp;

      existence

      proof

        set AS = the AffinPlane;

        set XX = ( IncProjSp_of AS);

        for A,K be LINE of XX holds ex a be POINT of XX st a on A & a on K by Lm5;

        then XX is 2-dimensional IncProjSp by INCPROJ:def 9;

        hence thesis;

      end;

    end

    registration

      let AS be AffinPlane;

      cluster ( IncProjSp_of AS) -> 2-dimensional;

      correctness

      proof

        set XX = ( IncProjSp_of AS);

        for A,K be LINE of XX holds ex a be Element of the Points of XX st a on A & a on K by Lm5;

        hence thesis by INCPROJ:def 9;

      end;

    end

    theorem :: AFPROJ:45

    ( IncProjSp_of AS) is 2-dimensional implies AS is AffinPlane

    proof

      set x = the Element of AS;

      assume

       A1: ( IncProjSp_of AS) is 2-dimensional;

      consider X such that

       A2: x in X and x in X and x in X and

       A3: X is being_plane by AFF_4: 37;

      assume not AS is AffinPlane;

      then

      consider z such that

       A4: not z in X by A3, AFF_4: 48;

      set Y = ( Line (x,z));

      

       A5: Y is being_line by A2, A4, AFF_1:def 3;

      then

      reconsider A = [( PDir X), 2], K = [Y, 1] as LINE of ( IncProjSp_of AS) by A3, Th23;

      consider a be POINT of ( IncProjSp_of AS) such that

       A6: a on A and

       A7: a on K by A1, INCPROJ:def 9;

       not a is Element of AS by A6, Th27;

      then

      consider Y9 such that

       A8: a = ( LDir Y9) and

       A9: Y9 is being_line by Th20;

      Y9 '||' Y by A5, A7, A8, A9, Th28;

      then

       A10: Y9 // Y by A5, A9, AFF_4: 40;

      

       A11: z in Y by AFF_1: 15;

      

       A12: x in Y by AFF_1: 15;

      Y9 '||' X by A3, A6, A8, A9, Th29;

      then Y c= X by A2, A3, A5, A12, A10, AFF_4: 43, AFF_4: 56;

      hence contradiction by A4, A11;

    end;

    theorem :: AFPROJ:46

     not AS is AffinPlane implies ( ProjHorizon AS) is IncProjSp

    proof

      set XX = ( ProjHorizon AS);

      

       A1: for a,b be Element of the Points of XX holds ex A be Element of the Lines of XX st a on A & b on A by Th40;

      

       A2: for A be Element of the Lines of XX holds ex a,b,c be Element of the Points of XX st a <> b & b <> c & c <> a & a on A & b on A & c on A

      proof

        let A be Element of the Lines of XX;

        consider a,b,c be Element of the Points of XX such that

         A3: a on A and

         A4: b on A and

         A5: c on A and

         A6: a <> b and

         A7: b <> c and

         A8: c <> a by Th39;

        take a, b, c;

        thus thesis by A3, A4, A5, A6, A7, A8;

      end;

      assume not AS is AffinPlane;

      then

       A9: ex a be Element of the Points of XX, A be Element of the Lines of XX st not a on A by Lm1;

      

       A10: for a,b,c,d,p,q be Element of the Points of XX, M,N,P,Q be Element of the Lines of XX st a on M & b on M & c on N & d on N & p on M & p on N & a on P & c on P & b on Q & d on Q & not p on P & not p on Q & M <> N holds ex q be Element of the Points of XX st q on P & q on Q by Th44;

      for a,b be Element of the Points of XX, A,K be Element of the Lines of XX st a on A & b on A & a on K & b on K holds a = b or A = K by Th38;

      hence thesis by A1, A9, A2, A10, INCPROJ:def 4, INCPROJ:def 5, INCPROJ:def 6, INCPROJ:def 7, INCPROJ:def 8;

    end;

    theorem :: AFPROJ:47

    ( ProjHorizon AS) is IncProjSp implies not AS is AffinPlane

    proof

      set XX = ( ProjHorizon AS);

      assume ( ProjHorizon AS) is IncProjSp;

      then

      consider a be Element of the Points of XX, A be Element of the Lines of XX such that

       A1: not a on A by INCPROJ:def 6;

      consider X such that

       A2: a = ( LDir X) and

       A3: X is being_line by Th14;

      consider Y such that

       A4: A = ( PDir Y) and

       A5: Y is being_plane by Th15;

      assume AS is AffinPlane;

      then Y = the carrier of AS by A5, Th2;

      then X '||' Y by A3, A5, AFF_4: 42;

      hence contradiction by A1, A2, A3, A4, A5, Th36;

    end;

    theorem :: AFPROJ:48

    

     Th48: 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 <> b & o <> b9 & o <> c9 & b in M & c in M & a9 in N & b9 in N & c9 in N & (a,b9) // (b,a9) & (b,c9) // (c,b9) & (a = b or b = c or a = c) 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

       A1: M is being_line and

       A2: N is being_line and

       A3: M <> N and

       A4: o in M and

       A5: o in N and

       A6: o <> b and

       A7: o <> b9 and

       A8: o <> c9 and

       A9: b in M and

       A10: c in M and

       A11: a9 in N and

       A12: b9 in N and

       A13: c9 in N and

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

       A15: (b,c9) // (c,b9) and

       A16: a = b or b = c or a = c;

      

       A17: c <> b9 by A1, A2, A3, A4, A5, A7, A10, A12, AFF_1: 18;

      now

        assume

         A18: a = c;

        then (b,c9) // (b,a9) by A14, A15, A17, AFF_1: 5;

        then a9 = c9 by A1, A2, A3, A4, A5, A6, A8, A9, A11, A13, AFF_4: 9;

        hence thesis by A18, AFF_1: 2;

      end;

      hence thesis by A1, A2, A3, A4, A5, A6, A7, A8, A9, A11, A12, A13, A14, A15, A16, AFF_4: 9;

    end;

    theorem :: AFPROJ:49

    ( IncProjSp_of AS) is Pappian implies AS is Pappian

    proof

      set XX = ( IncProjSp_of AS);

      assume

       A1: ( IncProjSp_of AS) is Pappian;

      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

         A10: o <> b9 and

         A11: o <> c and

         A12: o <> c9 and

         A13: a in M and

         A14: b in M and

         A15: c in M and

         A16: a9 in N and

         A17: b9 in N and

         A18: c9 in N and

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

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

        

         A21: b <> c9 by A2, A3, A4, A5, A6, A9, A14, A18, AFF_1: 18;

        then

         A22: ( Line (b,c9)) is being_line by AFF_1:def 3;

        c <> a9 by A2, A3, A4, A5, A6, A8, A15, A16, AFF_1: 18;

        then

         A23: ( Line (c,a9)) is being_line by AFF_1:def 3;

        

         A24: b <> a9 by A2, A3, A4, A5, A6, A8, A14, A16, AFF_1: 18;

        then

         A25: ( Line (b,a9)) is being_line by AFF_1:def 3;

        

         A26: c <> b9 by A2, A3, A4, A5, A6, A10, A15, A17, AFF_1: 18;

        then

         A27: ( Line (c,b9)) is being_line by AFF_1:def 3;

        reconsider A3 = [M, 1], B3 = [N, 1] as Element of the Lines of XX by A2, A3, Th23;

        reconsider p = o, a1 = a9, a2 = c9, a3 = b9, b1 = a, b2 = c, b3 = b as Element of the Points of XX by Th20;

        

         A28: p on A3 by A2, A5, Th26;

        

         A29: a <> b9 by A2, A3, A4, A5, A6, A7, A13, A17, AFF_1: 18;

        then

         A30: ( Line (a,b9)) is being_line by AFF_1:def 3;

        then

        reconsider c1 = ( LDir ( Line (b,c9))), c2 = ( LDir ( Line (a,b9))) as Element of the Points of XX by A22, Th20;

        

         A31: b1 on A3 by A2, A13, Th26;

        a <> c9 by A2, A3, A4, A5, A6, A7, A13, A18, AFF_1: 18;

        then

         A32: ( Line (a,c9)) is being_line by AFF_1:def 3;

        then

        reconsider A1 = [( Line (b,c9)), 1], A2 = [( Line (b,a9)), 1], B1 = [( Line (a,b9)), 1], B2 = [( Line (c,b9)), 1], C1 = [( Line (c,a9)), 1], C2 = [( Line (a,c9)), 1] as Element of the Lines of XX by A30, A25, A22, A27, A23, Th23;

        

         A33: c2 on B1 by A30, Th30;

        

         A34: b3 on A3 by A2, A14, Th26;

        

         A35: b2 on A3 by A2, A15, Th26;

        consider Y such that

         A36: M c= Y and

         A37: N c= Y and

         A38: Y is being_plane by A2, A3, A5, A6, AFF_4: 38;

        reconsider C39 = [( PDir Y), 2] as Element of the Lines of XX by A38, Th23;

        

         A39: c1 on C39 by A14, A18, A36, A37, A38, A21, A22, Th31, AFF_4: 19;

        

         A40: c2 on C39 by A13, A17, A36, A37, A38, A29, A30, Th31, AFF_4: 19;

        

         A41: a1 on B3 by A3, A16, Th26;

        

         A42: a3 on B3 by A3, A17, Th26;

        

         A43: p on B3 by A3, A6, Th26;

        b9 in ( Line (a,b9)) by AFF_1: 15;

        then

         A44: a3 on B1 by A30, Th26;

        a in ( Line (a,b9)) by AFF_1: 15;

        then

         A45: b1 on B1 by A30, Th26;

        

         A46: c in ( Line (c,a9)) by AFF_1: 15;

        then

         A47: b2 on C1 by A23, Th26;

        ( Line (b,c9)) // ( Line (c,b9)) by A20, A21, A26, AFF_1: 37;

        then ( Line (b,c9)) '||' ( Line (c,b9)) by A22, A27, AFF_4: 40;

        then

         A48: c1 on B2 by A22, A27, Th28;

        

         A49: c9 in ( Line (a,c9)) by AFF_1: 15;

        then

         A50: a2 on C2 by A32, Th26;

        b9 in ( Line (c,b9)) by AFF_1: 15;

        then

         A51: a3 on B2 by A27, Th26;

        c in ( Line (c,b9)) by AFF_1: 15;

        then

         A52: b2 on B2 by A27, Th26;

        c9 in ( Line (b,c9)) by AFF_1: 15;

        then

         A53: a2 on A1 by A22, Th26;

        b in ( Line (b,c9)) by AFF_1: 15;

        then

         A54: b3 on A1 by A22, Th26;

        

         A55: a2 on B3 by A3, A18, Th26;

        ( Line (a,b9)) // ( Line (b,a9)) by A19, A29, A24, AFF_1: 37;

        then ( Line (a,b9)) '||' ( Line (b,a9)) by A30, A25, AFF_4: 40;

        then

         A56: c2 on A2 by A30, A25, Th28;

        

         A57: a in ( Line (a,c9)) by AFF_1: 15;

        then

         A58: b1 on C2 by A32, Th26;

        a9 in ( Line (b,a9)) by AFF_1: 15;

        then

         A59: a1 on A2 by A25, Th26;

        b in ( Line (b,a9)) by AFF_1: 15;

        then

         A60: b3 on A2 by A25, Th26;

        

         A61: a9 in ( Line (c,a9)) by AFF_1: 15;

        then

         A62: a1 on C1 by A23, Th26;

        

         A63: c1 on A1 by A22, Th30;

        now

          

           A64: A3 <> B3

          proof

            assume A3 = B3;

            

            then M = ( [N, 1] `1 )

            .= N;

            hence contradiction by A4;

          end;

           not p on C1 & not p on C2

          proof

            assume p on C1 or p on C2;

            then a1 on A3 or a2 on A3 by A7, A11, A28, A31, A35, A58, A50, A47, A62, Lm2;

            hence contradiction by A8, A12, A28, A43, A41, A55, A64, INCPROJ:def 4;

          end;

          then

          consider c3 be Element of the Points of XX such that

           A65: c3 on C1 and

           A66: c3 on C2 by A28, A31, A35, A43, A41, A55, A58, A50, A47, A62, A64, INCPROJ:def 8;

          

           A67: {a2, b1, c3} on C2 by A58, A50, A66, INCSP_1: 2;

          

           A68: {a1, b3, c2} on A2 by A60, A59, A56, INCSP_1: 2;

          

           A69: {a3, b1, c2} on B1 by A45, A44, A33, INCSP_1: 2;

          assume that

           A70: b1 <> b2 and

           A71: b2 <> b3 and

           A72: b3 <> b1;

          

           A73: (p,b1,b2,b3) are_mutually_distinct by A7, A9, A11, A70, A71, A72, ZFMISC_1:def 6;

          a1 <> a2 & a2 <> a3 & a1 <> a3

          proof

             A74:

            now

              assume a9 = c9;

              then (a,b9) // (c,b9) by A19, A20, A24, AFF_1: 5;

              hence contradiction by A2, A3, A4, A5, A6, A7, A10, A13, A15, A17, A70, AFF_4: 9;

            end;

            assume not thesis;

            hence contradiction by A2, A3, A4, A5, A6, A7, A9, A10, A13, A14, A15, A17, A19, A20, A71, A72, A74, AFF_4: 9;

          end;

          then

           A75: (p,a1,a2,a3) are_mutually_distinct by A8, A10, A12, ZFMISC_1:def 6;

          

           A76: {a1, a2, a3} on B3 by A41, A55, A42, INCSP_1: 2;

          

           A77: {b1, b2, b3} on A3 by A31, A35, A34, INCSP_1: 2;

          

           A78: {a3, b2, c1} on B2 by A51, A52, A48, INCSP_1: 2;

          

           A79: {a2, b3, c1} on A1 by A53, A54, A63, INCSP_1: 2;

          

           A80: p on B3 by A3, A6, Th26;

          

           A81: p on A3 by A2, A5, Th26;

          

           A82: {c1, c2} on C39 by A39, A40, INCSP_1: 1;

           {a1, b2, c3} on C1 by A47, A62, A65, INCSP_1: 2;

          then c3 on C39 by A1, A75, A73, A64, A81, A80, A79, A69, A68, A78, A67, A77, A76, A82, INCPROJ:def 14;

          then not c3 is Element of AS by Th27;

          then

          consider Y such that

           A83: c3 = ( LDir Y) and

           A84: Y is being_line by Th20;

          Y '||' ( Line (c,a9)) by A23, A65, A83, A84, Th28;

          then

           A85: Y // ( Line (c,a9)) by A23, A84, AFF_4: 40;

          Y '||' ( Line (a,c9)) by A32, A66, A83, A84, Th28;

          then Y // ( Line (a,c9)) by A32, A84, AFF_4: 40;

          then ( Line (a,c9)) // ( Line (c,a9)) by A85, AFF_1: 44;

          hence thesis by A57, A49, A46, A61, AFF_1: 39;

        end;

        hence thesis by A2, A3, A4, A5, A6, A9, A10, A12, A14, A15, A16, A17, A18, A19, A20, Th48;

      end;

      hence thesis by AFF_2:def 2;

    end;

    theorem :: AFPROJ:50

    

     Th50: for A,P,C be Subset of AS, o,a,b,c,a9,b9,c9 be Element of AS st o in A & o in P & o in C & o <> a & o <> b & o <> c & a 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) & (o = a9 or a = a9) holds (b,c) // (b9,c9)

    proof

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

       A1: o in A and

       A2: o in P and

       A3: o in C and

       A4: o <> a and

       A5: o <> b and

       A6: o <> c and

       A7: a in A and

       A8: b in P and

       A9: b9 in P and

       A10: c in C and

       A11: c9 in C and

       A12: A is being_line and

       A13: P is being_line and

       A14: C is being_line and

       A15: A <> P and

       A16: A <> C and

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

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

       A19: o = a9 or a = a9;

       A20:

      now

        assume

         A21: a = a9;

        then

         A22: c = c9 by A1, A3, A4, A6, A7, A10, A11, A12, A14, A16, A18, AFF_4: 9;

        b = b9 by A1, A2, A4, A5, A7, A8, A9, A12, A13, A15, A17, A21, AFF_4: 9;

        hence thesis by A22, AFF_1: 2;

      end;

      now

        assume

         A23: o = a9;

        then

         A24: o = c9 by A1, A3, A4, A6, A7, A10, A11, A12, A14, A16, A18, AFF_4: 8;

        o = b9 by A1, A2, A4, A5, A7, A8, A9, A12, A13, A15, A17, A23, AFF_4: 8;

        hence thesis by A24, AFF_1: 3;

      end;

      hence thesis by A19, A20;

    end;

    theorem :: AFPROJ:51

    ( IncProjSp_of AS) is Desarguesian implies AS is Desarguesian

    proof

      set XX = ( IncProjSp_of AS);

      assume

       A1: ( IncProjSp_of AS) is Desarguesian;

      for A,P,C be Subset of AS, o,a,b,c,a9,b9,c9 be Element of AS 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 AS, o,a,b,c,a9,b9,c9 be Element of AS such that

         A2: o in A and

         A3: o in P and

         A4: o in C and

         A5: o <> a and

         A6: o <> b and

         A7: o <> c and

         A8: a in A and

         A9: a9 in A and

         A10: b in P and

         A11: b9 in P and

         A12: c in C and

         A13: c9 in C and

         A14: A is being_line and

         A15: P is being_line and

         A16: C is being_line and

         A17: A <> P and

         A18: A <> C and

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

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

        now

          assume

           A21: P <> C;

          now

            reconsider p = o, a1 = a, b1 = a9, a2 = b, b2 = b9, a3 = c, b3 = c9 as Element of the Points of XX by Th20;

            reconsider C1 = [A, 1], C2 = [P, 1], C39 = [C, 1] as Element of the Lines of XX by A14, A15, A16, Th23;

            assume that

             A22: a <> a9 and

             A23: o <> a9;

            

             A24: o <> c9 by A2, A4, A5, A7, A8, A9, A12, A14, A16, A18, A20, A23, AFF_4: 8;

            

             A25: a9 <> c9 by A2, A4, A9, A13, A14, A16, A18, A23, AFF_1: 18;

            then

             A26: ( Line (a9,c9)) is being_line by AFF_1:def 3;

            

             A27: o <> b9 by A2, A3, A5, A6, A8, A9, A10, A14, A15, A17, A19, A23, AFF_4: 8;

            then b9 <> c9 by A3, A4, A11, A13, A15, A16, A21, AFF_1: 18;

            then

             A28: ( Line (b9,c9)) is being_line by AFF_1:def 3;

            b <> c by A3, A4, A6, A10, A12, A15, A16, A21, AFF_1: 18;

            then

             A29: ( Line (b,c)) is being_line by AFF_1:def 3;

            

             A30: a <> c by A2, A4, A5, A8, A12, A14, A16, A18, AFF_1: 18;

            then

             A31: ( Line (a,c)) is being_line by AFF_1:def 3;

            

             A32: a <> b by A2, A3, A5, A8, A10, A14, A15, A17, AFF_1: 18;

            then

             A33: ( Line (a,b)) is being_line by AFF_1:def 3;

            then

            reconsider s = ( LDir ( Line (a,b))), r = ( LDir ( Line (a,c))) as Element of the Points of XX by A31, Th20;

            

             A34: p on C2 by A3, A15, Th26;

            

             A35: a9 <> b9 by A2, A3, A9, A11, A14, A15, A17, A23, AFF_1: 18;

            then

             A36: ( Line (a9,b9)) is being_line by AFF_1:def 3;

            then

            reconsider A1 = [( Line (b,c)), 1], A2 = [( Line (a,c)), 1], A3 = [( Line (a,b)), 1], B1 = [( Line (b9,c9)), 1], B2 = [( Line (a9,c9)), 1], B3 = [( Line (a9,b9)), 1] as Element of the Lines of XX by A33, A29, A31, A28, A26, Th23;

            

             A37: r on A2 by A31, Th30;

            

             A38: c in ( Line (b,c)) by AFF_1: 15;

            then

             A39: a3 on A1 by A29, Th26;

            

             A40: a3 on A1 by A29, A38, Th26;

            

             A41: c9 in ( Line (a9,c9)) by AFF_1: 15;

            then

             A42: b3 on B2 by A26, Th26;

            

             A43: a9 in ( Line (a9,c9)) by AFF_1: 15;

            then

             A44: b1 on B2 by A26, Th26;

            

             A45: ( Line (a,c)) // ( Line (a9,c9)) by A20, A30, A25, AFF_1: 37;

            then ( Line (a,c)) '||' ( Line (a9,c9)) by A31, A26, AFF_4: 40;

            then r on B2 by A31, A26, Th28;

            then

             A46: {b1, r, b3} on B2 by A44, A42, INCSP_1: 2;

            

             A47: c <> c9 by A2, A4, A5, A7, A8, A9, A12, A14, A16, A18, A20, A22, AFF_4: 9;

            

             A48: b1 on C1 by A9, A14, Th26;

            

             A49: a3 on C39 by A12, A16, Th26;

            

             A50: b9 in ( Line (a9,b9)) by AFF_1: 15;

            then

             A51: b2 on B3 by A36, Th26;

            

             A52: a9 in ( Line (a9,b9)) by AFF_1: 15;

            then

             A53: b1 on B3 by A36, Th26;

            

             A54: ( Line (a,b)) // ( Line (a9,b9)) by A19, A32, A35, AFF_1: 37;

            then ( Line (a,b)) '||' ( Line (a9,b9)) by A33, A36, AFF_4: 40;

            then s on B3 by A33, A36, Th28;

            then

             A55: {b1, s, b2} on B3 by A53, A51, INCSP_1: 2;

             A56:

            now

              assume C2 = C39;

              

              then P = ( [C, 1] `1 )

              .= C;

              hence contradiction by A21;

            end;

             A57:

            now

              assume C1 = C39;

              

              then A = ( [C, 1] `1 )

              .= C;

              hence contradiction by A18;

            end;

            now

              assume C1 = C2;

              

              then A = ( [P, 1] `1 )

              .= P;

              hence contradiction by A17;

            end;

            then

             A58: (C1,C2,C39) are_mutually_distinct by A56, A57, ZFMISC_1:def 5;

            

             A59: a1 on C1 by A8, A14, Th26;

            

             A60: b3 on C39 by A13, A16, Th26;

            

             A61: p on C39 by A4, A16, Th26;

            then

             A62: {p, a3, b3} on C39 by A49, A60, INCSP_1: 2;

            p on C1 by A2, A14, Th26;

            then

             A63: {p, b1, a1} on C1 by A48, A59, INCSP_1: 2;

            

             A64: b2 on C2 by A11, A15, Th26;

            

             A65: a in ( Line (a,c)) by AFF_1: 15;

            then

             A66: a1 on A2 by A31, Th26;

            

             A67: c in ( Line (a,c)) by AFF_1: 15;

            then a3 on A2 by A31, Th26;

            then

             A68: {a3, r, a1} on A2 by A37, A66, INCSP_1: 2;

            

             A69: b9 in ( Line (b9,c9)) by AFF_1: 15;

            then

             A70: b2 on B1 by A28, Th26;

            

             A71: c9 in ( Line (b9,c9)) by AFF_1: 15;

            then

             A72: b3 on B1 by A28, Th26;

            

             A73: b3 on B1 by A28, A71, Th26;

            

             A74: a2 on C2 by A10, A15, Th26;

            then

             A75: {p, a2, b2} on C2 by A34, A64, INCSP_1: 2;

            

             A76: b in ( Line (b,c)) by AFF_1: 15;

            then

             A77: a2 on A1 by A29, Th26;

             not p on A1 & not p on B1

            proof

              assume p on A1 or p on B1;

              then a3 on C2 or b3 on C2 by A6, A27, A34, A74, A64, A77, A40, A70, A73, INCPROJ:def 4;

              hence contradiction by A7, A24, A34, A61, A49, A60, A56, INCPROJ:def 4;

            end;

            then

            consider t be Element of the Points of XX such that

             A78: t on A1 and

             A79: t on B1 by A34, A61, A74, A64, A49, A60, A77, A40, A70, A73, A56, INCPROJ:def 8;

            a2 on A1 by A29, A76, Th26;

            then

             A80: {a3, a2, t} on A1 by A78, A39, INCSP_1: 2;

            b2 on B1 by A28, A69, Th26;

            then

             A81: {t, b2, b3} on B1 by A79, A72, INCSP_1: 2;

            

             A82: a in ( Line (a,b)) by AFF_1: 15;

            then

             A83: a1 on A3 by A33, Th26;

            

             A84: s on A3 by A33, Th30;

            

             A85: b in ( Line (a,b)) by AFF_1: 15;

            then a2 on A3 by A33, Th26;

            then

             A86: {a2, s, a1} on A3 by A84, A83, INCSP_1: 2;

            b <> b9 by A2, A3, A5, A6, A8, A9, A10, A14, A15, A17, A19, A22, AFF_4: 9;

            then

            consider O be Element of the Lines of XX such that

             A87: {r, s, t} on O by A1, A5, A6, A7, A22, A23, A27, A24, A47, A63, A75, A62, A80, A68, A86, A81, A46, A55, A58, INCPROJ:def 13;

            

             A88: t on O by A87, INCSP_1: 2;

            

             A89: s on O by A87, INCSP_1: 2;

            

             A90: r on O by A87, INCSP_1: 2;

             A91:

            now

              assume

               A92: r <> s;

              ex X st O = [( PDir X), 2] & X is being_plane

              proof

                reconsider x = ( LDir ( Line (a,b))), y = ( LDir ( Line (a,c))) as Element of the Points of ( ProjHorizon AS) by A33, A31, Th14;

                

                 A93: [y, O] in the Inc of ( IncProjSp_of AS) by A90, INCSP_1:def 1;

                 [x, O] in the Inc of ( IncProjSp_of AS) by A89, INCSP_1:def 1;

                then

                consider Z9 be Element of the Lines of ( ProjHorizon AS) such that

                 A94: O = [Z9, 2] by A92, A93, Th41;

                consider X such that

                 A95: Z9 = ( PDir X) and

                 A96: X is being_plane by Th15;

                take X;

                thus thesis by A94, A95, A96;

              end;

              then not t is Element of AS by A88, Th27;

              then

              consider Y such that

               A97: t = ( LDir Y) and

               A98: Y is being_line by Th20;

              Y '||' ( Line (b9,c9)) by A28, A79, A97, A98, Th28;

              then

               A99: Y // ( Line (b9,c9)) by A28, A98, AFF_4: 40;

              Y '||' ( Line (b,c)) by A29, A78, A97, A98, Th28;

              then Y // ( Line (b,c)) by A29, A98, AFF_4: 40;

              then ( Line (b,c)) // ( Line (b9,c9)) by A99, AFF_1: 44;

              hence thesis by A76, A38, A69, A71, AFF_1: 39;

            end;

            now

              assume r = s;

              then

               A100: ( Line (a,b)) // ( Line (a,c)) by A33, A31, Th11;

              then ( Line (a,b)) // ( Line (a9,c9)) by A45, AFF_1: 44;

              then ( Line (a9,b9)) // ( Line (a9,c9)) by A54, AFF_1: 44;

              then

               A101: c9 in ( Line (a9,b9)) by A52, A43, A41, AFF_1: 45;

              c in ( Line (a,b)) by A82, A65, A67, A100, AFF_1: 45;

              hence thesis by A85, A50, A54, A101, AFF_1: 39;

            end;

            hence thesis by A91;

          end;

          hence thesis by A2, A3, A4, A5, A6, A7, A8, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, Th50;

        end;

        hence thesis by A10, A11, A12, A13, A15, AFF_1: 51;

      end;

      hence thesis by AFF_2:def 4;

    end;

    theorem :: AFPROJ:52

    ( IncProjSp_of AS) is Fanoian implies AS is Fanoian

    proof

      set XX = ( IncProjSp_of AS);

      assume

       A1: ( IncProjSp_of AS) is Fanoian;

      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

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

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

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

        assume

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

        then

         A6: a <> d by A2, AFF_1: 4;

        then

         A7: ( Line (a,d)) is being_line by AFF_1:def 3;

         A8:

        now

          assume b = d;

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

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

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

          hence contradiction by A5, AFF_1:def 1;

        end;

        then

         A9: ( Line (b,d)) is being_line by AFF_1:def 3;

         A10:

        now

          assume c = d;

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

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

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

          hence contradiction by A5, AFF_1:def 1;

        end;

        then

         A11: ( Line (c,d)) is being_line by AFF_1:def 3;

        

         A12: a <> c by A5, AFF_1: 3;

        then

         A13: ( Line (a,c)) is being_line by AFF_1:def 3;

        

         A14: a <> b by A5, AFF_1: 3;

        then

         A15: ( Line (a,b)) is being_line by AFF_1:def 3;

        then

        reconsider a9 = ( LDir ( Line (a,b))), b9 = ( LDir ( Line (a,c))), c9 = ( LDir ( Line (a,d))) as Element of the Points of XX by A13, A7, Th20;

        

         A16: b <> c by A5, AFF_1: 2;

        then

         A17: ( Line (b,c)) is being_line by AFF_1:def 3;

        then

        reconsider L1 = [( Line (a,b)), 1], Q1 = [( Line (c,d)), 1], R1 = [( Line (b,d)), 1], S1 = [( Line (a,c)), 1], A1 = [( Line (a,d)), 1], B1 = [( Line (b,c)), 1] as Element of the Lines of XX by A15, A11, A9, A13, A7, Th23;

        reconsider p = a, q = d, r = c, s = b as Element of the Points of XX by Th20;

        

         A18: a9 on L1 by A15, Th30;

        c in ( Line (b,c)) by AFF_1: 15;

        then

         A19: r on B1 by A17, Th26;

        b in ( Line (b,c)) by AFF_1: 15;

        then

         A20: s on B1 by A17, Th26;

        ( Line (a,d)) // ( Line (b,c)) by A4, A16, A6, AFF_1: 37;

        then ( Line (a,d)) '||' ( Line (b,c)) by A7, A17, AFF_4: 40;

        then c9 on B1 by A7, A17, Th28;

        then

         A21: {c9, r, s} on B1 by A19, A20, INCSP_1: 2;

        

         A22: d in ( Line (b,d)) by AFF_1: 15;

        then

         A23: q on R1 by A9, Th26;

        

         A24: c in ( Line (a,c)) by AFF_1: 15;

        then

         A25: r on S1 by A13, Th26;

        

         A26: b9 on S1 by A13, Th30;

        

         A27: a in ( Line (a,c)) by AFF_1: 15;

        then p on S1 by A13, Th26;

        then

         A28: {b9, p, r} on S1 by A25, A26, INCSP_1: 2;

        

         A29: ( Line (a,c)) // ( Line (b,d)) by A3, A12, A8, AFF_1: 37;

        then ( Line (a,c)) '||' ( Line (b,d)) by A9, A13, AFF_4: 40;

        then

         A30: b9 on R1 by A9, A13, Th28;

        

         A31: b in ( Line (b,d)) by AFF_1: 15;

        then s on R1 by A9, Th26;

        then

         A32: {b9, q, s} on R1 by A23, A30, INCSP_1: 2;

         A33:

        now

          assume ( Line (a,c)) = ( Line (b,d));

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

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

          hence contradiction by A5, AFF_1:def 1;

        end;

         A34:

        now

          assume q on S1 or s on S1;

          then d in ( Line (a,c)) or b in ( Line (a,c)) by Th26;

          hence contradiction by A31, A22, A33, A29, AFF_1: 45;

        end;

         A35:

        now

          assume p on R1 or r on R1;

          then a in ( Line (b,d)) or c in ( Line (b,d)) by Th26;

          hence contradiction by A27, A24, A33, A29, AFF_1: 45;

        end;

        

         A36: a in ( Line (a,b)) by AFF_1: 15;

        then

        consider Y such that

         A37: ( Line (a,b)) c= Y and

         A38: ( Line (a,c)) c= Y and

         A39: Y is being_plane by A27, A15, A13, AFF_4: 38;

        reconsider C1 = [( PDir Y), 2] as Element of the Lines of XX by A39, Th23;

        

         A40: b9 on C1 by A13, A38, A39, Th31;

        

         A41: ( Line (a,b)) // ( Line (c,d)) by A2, A14, A10, AFF_1: 37;

        then ( Line (a,b)) '||' ( Line (c,d)) by A15, A11, AFF_4: 40;

        then

         A42: a9 on Q1 by A15, A11, Th28;

        d in ( Line (a,d)) by AFF_1: 15;

        then

         A43: q on A1 by A7, Th26;

        a in ( Line (a,d)) by AFF_1: 15;

        then

         A44: p on A1 by A7, Th26;

        c9 on A1 by A7, Th30;

        then

         A45: {c9, p, q} on A1 by A44, A43, INCSP_1: 2;

        

         A46: b in ( Line (a,b)) by AFF_1: 15;

        then

         A47: s on L1 by A15, Th26;

        a9 on C1 by A15, A37, A39, Th31;

        then

         A48: {a9, b9} on C1 by A40, INCSP_1: 1;

        

         A49: d in ( Line (c,d)) by AFF_1: 15;

        then

         A50: q on Q1 by A11, Th26;

        

         A51: c in ( Line (c,d)) by AFF_1: 15;

        then r on Q1 by A11, Th26;

        then

         A52: {a9, q, r} on Q1 by A50, A42, INCSP_1: 2;

         A53:

        now

          assume ( Line (a,b)) = ( Line (c,d));

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

          hence contradiction by A5, AFF_1:def 1;

        end;

         A54:

        now

          assume q on L1 or r on L1;

          then d in ( Line (a,b)) or c in ( Line (a,b)) by Th26;

          hence contradiction by A51, A49, A53, A41, AFF_1: 45;

        end;

         A55:

        now

          assume p on Q1 or s on Q1;

          then a in ( Line (c,d)) or b in ( Line (c,d)) by Th26;

          hence contradiction by A36, A46, A53, A41, AFF_1: 45;

        end;

        ( Line (b,d)) = (b * ( Line (a,c))) by A31, A13, A29, AFF_4:def 3;

        then ( Line (b,d)) c= Y by A46, A13, A37, A38, A39, AFF_4: 28;

        then

         A56: c9 on C1 by A36, A22, A6, A7, A37, A39, Th31, AFF_4: 19;

        p on L1 by A36, A15, Th26;

        then {a9, p, s} on L1 by A47, A18, INCSP_1: 2;

        hence contradiction by A1, A56, A54, A34, A55, A35, A52, A32, A28, A45, A21, A48, INCPROJ:def 12;

      end;

      hence thesis by PAPDESAF:def 1;

    end;