projred2.miz



    begin

    reserve IPS for IncProjSp,

z for POINT of IPS;

    definition

      let IPS;

      let A,B,C be LINE of IPS;

      :: PROJRED2:def1

      pred A,B,C are_concurrent means ex o be Element of the Points of IPS st o on A & o on B & o on C;

    end

    definition

      let IPS;

      let Z be LINE of IPS;

      :: PROJRED2:def2

      func CHAIN (Z) -> Subset of the Points of IPS equals { z : z on Z };

      correctness

      proof

        set X = { z : z on Z };

        now

          let x be object;

          assume x in X;

          then ex z st z = x & z on Z;

          hence x in the Points of IPS;

        end;

        hence thesis by TARSKI:def 3;

      end;

    end

    reserve IPP for Desarguesian 2-dimensional IncProjSp,

a,b,c,d,p,pp9,q,o,o9,o99,oo9 for POINT of IPP,

r,s,x,y,o1,o2 for POINT of IPP,

O1,O2,O3,O4,A,B,C,O,Q,Q1,Q2,Q3,R,S,X for LINE of IPP;

    definition

      let IPP;

      :: PROJRED2:def3

      mode Projection of IPP -> PartFunc of the Points of IPP, the Points of IPP means

      : Def3: ex a, A, B st not a on A & not a on B & it = ( IncProj (A,a,B));

      existence

      proof

        set A = the LINE of IPP;

        consider a such that

         A1: ( not a on A) & not a on A by PROJRED1: 6;

        take ( IncProj (A,a,A));

        thus thesis by A1;

      end;

    end

    theorem :: PROJRED2:1

    

     Th1: A = B or B = C or C = A implies (A,B,C) are_concurrent

    proof

      

       A1: (ex a st a on B & a on C) & ex b st b on C & b on A by INCPROJ:def 9;

      assume A = B or B = C or C = A;

      hence thesis by A1;

    end;

    theorem :: PROJRED2:2

    (A,B,C) are_concurrent implies (A,C,B) are_concurrent & (B,A,C) are_concurrent & (B,C,A) are_concurrent & (C,A,B) are_concurrent & (C,B,A) are_concurrent ;

    theorem :: PROJRED2:3

    

     Th3: not o on A & not o on B & y on B implies ex x st x on A & (( IncProj (A,o,B)) . x) = y

    proof

      consider X such that

       A1: o on X & y on X by INCPROJ:def 5;

      consider x such that

       A2: x on X and

       A3: x on A by INCPROJ:def 9;

      assume ( not o on A) & not o on B & y on B;

      then (( IncProj (A,o,B)) . x) = y by A1, A2, A3, PROJRED1:def 1;

      hence thesis by A3;

    end;

    theorem :: PROJRED2:4

    

     Th4: not o on A & not o on B implies ( dom ( IncProj (A,o,B))) = ( CHAIN A)

    proof

      assume

       A1: ( not o on A) & not o on B;

       A2:

      now

        let x be object;

        assume

         A3: x in ( dom ( IncProj (A,o,B)));

        then

        reconsider x9 = x as POINT of IPP;

        x9 on A by A1, A3, PROJRED1:def 1;

        hence x in ( CHAIN A);

      end;

      now

        let x be object;

        assume x in ( CHAIN A);

        then ex b st b = x & b on A;

        hence x in ( dom ( IncProj (A,o,B))) by A1, PROJRED1:def 1;

      end;

      hence thesis by A2, TARSKI: 2;

    end;

    theorem :: PROJRED2:5

    

     Th5: not o on A & not o on B implies ( rng ( IncProj (A,o,B))) = ( CHAIN B)

    proof

      assume

       A1: ( not o on A) & not o on B;

       A2:

      now

        let x be object;

        assume

         A3: x in ( CHAIN B);

        then

        reconsider x9 = x as Element of the Points of IPP;

        ex b st b = x & b on B by A3;

        then

        consider y such that

         A4: y on A and

         A5: (( IncProj (A,o,B)) . y) = x9 by A1, Th3;

        y in ( CHAIN A) by A4;

        then y in ( dom ( IncProj (A,o,B))) by A1, Th4;

        hence x in ( rng ( IncProj (A,o,B))) by A5, FUNCT_1:def 3;

      end;

      now

        let x be object such that

         A6: x in ( rng ( IncProj (A,o,B)));

        ( rng ( IncProj (A,o,B))) c= the Points of IPP by RELAT_1:def 19;

        then

        reconsider x9 = x as POINT of IPP by A6;

        x9 on B by A1, A6, PROJRED1: 21;

        hence x in ( CHAIN B);

      end;

      hence thesis by A2, TARSKI: 2;

    end;

    theorem :: PROJRED2:6

    for x be set holds x in ( CHAIN A) iff ex a st x = a & a on A;

    theorem :: PROJRED2:7

    

     Th7: not o on A & not o on B implies ( IncProj (A,o,B)) is one-to-one

    proof

      set f = ( IncProj (A,o,B));

      assume

       A1: ( not o on A) & not o on B;

      now

        let x1,x2 be object;

        assume that

         A2: x1 in ( dom f) and

         A3: x2 in ( dom f) and

         A4: (f . x1) = (f . x2);

        x1 in ( CHAIN A) by A1, A2, Th4;

        then

        consider a such that

         A5: x1 = a and

         A6: a on A;

        x2 in ( CHAIN A) by A1, A3, Th4;

        then

        consider b such that

         A7: x2 = b and

         A8: b on A;

        reconsider x = (f . a), y = (f . b) as POINT of IPP by A1, A6, A8, PROJRED1: 19;

        x = y by A4, A5, A7;

        hence x1 = x2 by A1, A5, A6, A7, A8, PROJRED1: 23;

      end;

      hence thesis by FUNCT_1:def 4;

    end;

    theorem :: PROJRED2:8

    

     Th8: not o on A & not o on B implies (( IncProj (A,o,B)) " ) = ( IncProj (B,o,A))

    proof

      set f = ( IncProj (A,o,B)), g = ( IncProj (B,o,A));

      assume

       A1: ( not o on A) & not o on B;

      then

       A2: ( rng f) = ( CHAIN B) by Th5;

      

       A3: ( dom f) = ( CHAIN A) by A1, Th4;

       A4:

      now

        let y,x be object;

         A5:

        now

          assume that

           A6: x in ( dom f) and

           A7: y = (f . x);

          consider x9 be POINT of IPP such that

           A8: x = x9 & x9 on A by A3, A6;

          reconsider y9 = y as POINT of IPP by A1, A7, A8, PROJRED1: 19;

          

           A9: y9 on B by A1, A7, A8, PROJRED1: 20;

          then

           A10: y in ( CHAIN B);

          ex O st o on O & x9 on O & y9 on O by A1, A7, A8, A9, PROJRED1:def 1;

          hence y in ( rng f) & x = (g . y) by A1, A8, A9, A10, Th5, PROJRED1:def 1;

        end;

        now

          assume that

           A11: y in ( rng f) and

           A12: x = (g . y);

          consider y9 be POINT of IPP such that

           A13: y = y9 & y9 on B by A2, A11;

          reconsider x9 = x as POINT of IPP by A1, A12, A13, PROJRED1: 19;

          

           A14: x9 on A by A1, A12, A13, PROJRED1: 20;

          then ex O st o on O & y9 on O & x9 on O by A1, A12, A13, PROJRED1:def 1;

          hence x in ( dom f) & y = (f . x) by A1, A13, A14, PROJRED1:def 1;

        end;

        hence y in ( rng f) & x = (g . y) iff x in ( dom f) & y = (f . x) by A5;

      end;

      

       A15: f is one-to-one by A1, Th7;

      ( dom g) = ( CHAIN B) by A1, Th4

      .= ( rng f) by A1, Th5;

      hence thesis by A15, A4, FUNCT_1: 32;

    end;

    theorem :: PROJRED2:9

    for f be Projection of IPP holds (f " ) is Projection of IPP

    proof

      let f be Projection of IPP;

      consider a, A, B such that

       A1: ( not a on A) & not a on B and

       A2: f = ( IncProj (A,a,B)) by Def3;

      (f " ) = ( IncProj (B,a,A)) by A1, A2, Th8;

      hence thesis by A1, Def3;

    end;

    theorem :: PROJRED2:10

    

     Th10: not o on A implies ( IncProj (A,o,A)) = ( id ( CHAIN A))

    proof

      set f = ( IncProj (A,o,A));

      assume

       A1: not o on A;

      

       A2: for x be object st x in ( CHAIN A) holds (f . x) = x

      proof

        let x be object;

        assume x in ( CHAIN A);

        then ex x9 be Element of the Points of IPP st x = x9 & x9 on A;

        hence thesis by A1, PROJRED1: 24;

      end;

      ( dom f) = ( CHAIN A) by A1, Th4;

      hence thesis by A2, FUNCT_1: 17;

    end;

    theorem :: PROJRED2:11

    ( id ( CHAIN A)) is Projection of IPP

    proof

      consider o such that

       A1: not o on A by PROJRED1: 1;

      ( id ( CHAIN A)) = ( IncProj (A,o,A)) by A1, Th10;

      hence thesis by A1, Def3;

    end;

    theorem :: PROJRED2:12

     not o on A & not o on B & not o on C implies (( IncProj (C,o,B)) * ( IncProj (A,o,C))) = ( IncProj (A,o,B))

    proof

      assume that

       A1: not o on A and

       A2: not o on B and

       A3: not o on C;

      set f = ( IncProj (A,o,B)), g = ( IncProj (C,o,B)), h = ( IncProj (A,o,C));

      

       A4: ( dom f) = ( CHAIN A) by A1, A2, Th4;

      set X = ( CHAIN A);

      

       A5: ( dom h) = ( CHAIN A) by A1, A3, Th4;

      

       A6: for x st x on A holds (( IncProj (A,o,B)) . x) = ((( IncProj (C,o,B)) * ( IncProj (A,o,C))) . x)

      proof

        let x such that

         A7: x on A;

        consider Q1 such that

         A8: o on Q1 and

         A9: x on Q1 by INCPROJ:def 5;

        consider x9 be POINT of IPP such that

         A10: x9 on Q1 & x9 on C by INCPROJ:def 9;

        

         A11: (h . x) = x9 by A1, A3, A7, A8, A9, A10, PROJRED1:def 1;

        consider y be POINT of IPP such that

         A12: y on Q1 & y on B by INCPROJ:def 9;

        

         A13: (f . x) = y by A1, A2, A7, A8, A9, A12, PROJRED1:def 1;

        x in ( dom h) by A5, A7;

        

        then ((g * h) . x) = (g . (h . x)) by FUNCT_1: 13

        .= (f . x) by A2, A3, A8, A10, A12, A13, A11, PROJRED1:def 1;

        hence thesis;

      end;

       A14:

      now

        let y be object;

        assume y in X;

        then ex x st y = x & x on A;

        hence ((g * h) . y) = (f . y) by A6;

      end;

      ( dom (g * h)) = X by A1, A2, A3, A5, PROJRED1: 22;

      hence thesis by A4, A14, FUNCT_1: 2;

    end;

    theorem :: PROJRED2:13

     not o1 on O1 & not o1 on O2 & not o2 on O2 & not o2 on O3 & (O1,O2,O3) are_concurrent & O1 <> O3 implies ex o st not o on O1 & not o on O3 & (( IncProj (O2,o2,O3)) * ( IncProj (O1,o1,O2))) = ( IncProj (O1,o,O3)) by PROJRED1: 25;

    theorem :: PROJRED2:14

    

     Th14: not a on A & not b on B & not a on C & not b on C & not (A,B,C) are_concurrent & c on A & c on C & c on Q & not b on Q & A <> Q & a on O & b on O & not (B,C,O) are_concurrent & d on C & d on B & a on O1 & d on O1 & p on A & p on O1 & q on O & q on O2 & p on O2 & pp9 on O2 & d on O3 & b on O3 & pp9 on O3 & pp9 on Q & q <> a & not q on A & not q on Q implies (( IncProj (C,b,B)) * ( IncProj (A,a,C))) = (( IncProj (Q,b,B)) * ( IncProj (A,q,Q)))

    proof

      assume that

       A1: not a on A and

       A2: not b on B and

       A3: not a on C and

       A4: not b on C and

       A5: not (A,B,C) are_concurrent and

       A6: c on A and

       A7: c on C and

       A8: c on Q and

       A9: not b on Q and

       A10: A <> Q and

       A11: a on O and

       A12: b on O and

       A13: not (B,C,O) are_concurrent and

       A14: d on C and

       A15: d on B and

       A16: a on O1 and

       A17: d on O1 and

       A18: p on A and

       A19: p on O1 and

       A20: q on O and

       A21: q on O2 and

       A22: p on O2 & pp9 on O2 and

       A23: d on O3 & b on O3 and

       A24: pp9 on O3 and

       A25: pp9 on Q and

       A26: q <> a and

       A27: not q on A and

       A28: not q on Q;

      set f = ( IncProj (A,a,C)), g = ( IncProj (C,b,B)), g1 = ( IncProj (Q,b,B)), f1 = ( IncProj (A,q,Q));

      

       A29: ( dom f) = ( CHAIN A) by A1, A3, Th4;

      set X = ( CHAIN A);

      

       A30: ( dom f1) = ( CHAIN A) by A27, A28, Th4;

      then

       A31: ( dom (g1 * f1)) = X by A2, A9, A27, A28, PROJRED1: 22;

      

       A32: O1 <> O2

      proof

        assume not thesis;

        then d on O by A11, A16, A17, A20, A21, A26, INCPROJ:def 4;

        hence contradiction by A13, A14, A15;

      end;

      c <> d by A5, A6, A7, A15;

      then p <> c by A3, A7, A14, A16, A17, A19, INCPROJ:def 4;

      then

       A33: pp9 <> p by A6, A8, A10, A18, A25, INCPROJ:def 4;

      

       A34: for x st x on A holds ((( IncProj (C,b,B)) * ( IncProj (A,a,C))) . x) = ((( IncProj (Q,b,B)) * ( IncProj (A,q,Q))) . x)

      proof

        let x such that

         A35: x on A;

        consider Q3 such that

         A36: q on Q3 & x on Q3 by INCPROJ:def 5;

        consider Q1 such that

         A37: a on Q1 & x on Q1 by INCPROJ:def 5;

        consider y be POINT of IPP such that

         A38: y on Q3 and

         A39: y on Q by INCPROJ:def 9;

        consider x9 be POINT of IPP such that

         A40: x9 on Q1 and

         A41: x9 on C by INCPROJ:def 9;

         A42:

        now

          

           A43: {pp9, y, c} on Q & {d, x9, c} on C by A7, A8, A14, A25, A41, A39, INCSP_1: 2;

          

           A44: {p, pp9, q} on O2 & {pp9, d, b} on O3 by A21, A22, A23, A24, INCSP_1: 2;

          

           A45: {b, a, q} on O & {x, y, q} on Q3 by A11, A12, A20, A36, A38, INCSP_1: 2;

          

           A46: {p, x, c} on A & {p, d, a} on O1 by A6, A16, A17, A18, A19, A35, INCSP_1: 2;

          assume

           A47: p <> x;

           {x, x9, a} on Q1 & (A,O1,O2) are_mutually_distinct by A1, A16, A21, A27, A32, A37, A40, INCSP_1: 2, ZFMISC_1:def 5;

          then

          consider R such that

           A48: {y, x9, b} on R by A1, A3, A14, A18, A33, A47, A46, A44, A43, A45, PROJRED1: 12;

          

           A49: b on R by A48, INCSP_1: 2;

          consider x99 be POINT of IPP such that

           A50: x99 on R & x99 on B by INCPROJ:def 9;

          x9 on R by A48, INCSP_1: 2;

          then

           A51: (g . x9) = x99 by A2, A4, A41, A50, A49, PROJRED1:def 1;

          

           A52: x in ( dom f1) by A30, A35;

          y on R by A48, INCSP_1: 2;

          then

           A53: (g1 . y) = x99 by A2, A9, A39, A50, A49, PROJRED1:def 1;

          

           A54: x in ( dom f) by A29, A35;

          (f . x) = x9 & (f1 . x) = y by A1, A3, A27, A28, A35, A37, A40, A41, A36, A38, A39, PROJRED1:def 1;

          

          then ((g * f) . x) = (g1 . (f1 . x)) by A51, A53, A54, FUNCT_1: 13

          .= ((g1 * f1) . x) by A52, FUNCT_1: 13;

          hence thesis;

        end;

        now

          

           A55: (f1 . p) = pp9 & (g1 . pp9) = d by A2, A9, A15, A18, A21, A22, A23, A24, A25, A27, A28, PROJRED1:def 1;

          assume

           A56: p = x;

          

           A57: x in ( dom f1) by A30, A35;

          

           A58: x in ( dom f) by A29, A35;

          (f . p) = d & (g . d) = d by A1, A2, A3, A4, A14, A15, A16, A17, A18, A19, A23, PROJRED1:def 1;

          

          then ((g * f) . x) = (g1 . (f1 . x)) by A56, A55, A58, FUNCT_1: 13

          .= ((g1 * f1) . x) by A57, FUNCT_1: 13;

          hence thesis;

        end;

        hence thesis by A42;

      end;

       A59:

      now

        let y be object;

        assume y in X;

        then ex x st y = x & x on A;

        hence ((g * f) . y) = ((g1 * f1) . y) by A34;

      end;

      ( dom (g * f)) = X by A1, A2, A3, A4, A29, PROJRED1: 22;

      hence thesis by A31, A59, FUNCT_1: 2;

    end;

    theorem :: PROJRED2:15

    

     Th15: not a on A & not a on C & not b on B & not b on C & not b on Q & not (A,B,C) are_concurrent & a <> b & b <> q & A <> Q & {c, o} on A & {o, o99, d} on B & {c, d, o9} on C & {a, b, d} on O & {c, oo9} on Q & {a, o, o9} on O1 & {b, o9, oo9} on O2 & {o, oo9, q} on O3 & q on O implies (( IncProj (C,b,B)) * ( IncProj (A,a,C))) = (( IncProj (Q,b,B)) * ( IncProj (A,q,Q)))

    proof

      assume that

       A1: not a on A and

       A2: not a on C and

       A3: not b on B and

       A4: not b on C and

       A5: not b on Q and

       A6: not (A,B,C) are_concurrent and

       A7: a <> b and

       A8: b <> q and

       A9: A <> Q and

       A10: {c, o} on A and

       A11: {o, o99, d} on B and

       A12: {c, d, o9} on C and

       A13: {a, b, d} on O and

       A14: {c, oo9} on Q and

       A15: {a, o, o9} on O1 and

       A16: {b, o9, oo9} on O2 and

       A17: {o, oo9, q} on O3 and

       A18: q on O;

      

       A19: o on A by A10, INCSP_1: 1;

      

       A20: c on A & c on Q by A10, A14, INCSP_1: 1;

      

       A21: o9 on C by A12, INCSP_1: 2;

      

       A22: oo9 on O2 by A16, INCSP_1: 2;

      

       A23: b on O by A13, INCSP_1: 2;

      

       A24: q on O3 by A17, INCSP_1: 2;

      

       A25: o on O3 & oo9 on O3 by A17, INCSP_1: 2;

      set X = ( CHAIN A);

      set f = ( IncProj (A,a,C)), g = ( IncProj (C,b,B)), f1 = ( IncProj (A,q,Q)), g1 = ( IncProj (Q,b,B));

      

       A26: o on B by A11, INCSP_1: 2;

      

       A27: ( dom f) = ( CHAIN A) by A1, A2, Th4;

      

       A28: o9 on O2 by A16, INCSP_1: 2;

      

       A29: q on O3 by A17, INCSP_1: 2;

      

       A30: b on O2 by A16, INCSP_1: 2;

      

       A31: o on B by A11, INCSP_1: 2;

      

       A32: d on C by A12, INCSP_1: 2;

      then

       A33: o <> d by A6, A19, A31;

      

       A34: d on O by A13, INCSP_1: 2;

      

       A35: o on O3 & oo9 on O3 by A17, INCSP_1: 2;

      

       A36: o9 on O1 by A15, INCSP_1: 2;

      

       A37: o on A by A10, INCSP_1: 1;

      

       A38: a on O1 by A15, INCSP_1: 2;

      

       A39: d on B by A11, INCSP_1: 2;

      then

       A40: q <> o by A3, A18, A31, A23, A34, A33, INCPROJ:def 4;

      

       A41: c on C by A12, INCSP_1: 2;

      

       A42: oo9 on Q by A14, INCSP_1: 1;

      

       A43: o on O1 by A15, INCSP_1: 2;

      

       A44: c on A by A10, INCSP_1: 1;

      then

       A45: o <> c by A6, A31, A41;

      then

       A46: o9 <> c by A1, A44, A19, A38, A43, A36, INCPROJ:def 4;

      then

       A47: c <> oo9 by A4, A41, A21, A30, A28, A22, INCPROJ:def 4;

      

       A48: not q on A

      proof

        assume not thesis;

        then oo9 on A by A37, A35, A29, A40, INCPROJ:def 4;

        hence contradiction by A9, A20, A42, A47, INCPROJ:def 4;

      end;

      

       A49: a on O by A13, INCSP_1: 2;

      o9 <> d

      proof

        assume not thesis;

        then O1 = O by A2, A32, A49, A34, A38, A36, INCPROJ:def 4;

        hence contradiction by A3, A31, A39, A23, A34, A43, A33, INCPROJ:def 4;

      end;

      then O <> O2 by A2, A32, A21, A49, A34, A28, INCPROJ:def 4;

      then

       A50: q <> oo9 by A8, A18, A23, A30, A22, INCPROJ:def 4;

      

       A51: not q on Q

      proof

        assume not thesis;

        then o on Q by A42, A35, A29, A50, INCPROJ:def 4;

        hence contradiction by A9, A20, A37, A45, INCPROJ:def 4;

      end;

      then

       A52: ( dom f1) = ( CHAIN A) by A48, Th4;

      then

       A53: ( dom (g1 * f1)) = X by A3, A5, A48, A51, PROJRED1: 22;

      

       A54: d on B & d on O by A11, A13, INCSP_1: 2;

      

       A55: O1 <> O2

      proof

        assume not thesis;

        then o on O by A7, A49, A23, A38, A43, A30, INCPROJ:def 4;

        then O = B by A54, A26, A33, INCPROJ:def 4;

        hence contradiction by A3, A13, INCSP_1: 2;

      end;

      

       A56: c on Q & oo9 on Q by A14, INCSP_1: 1;

      

       A57: for x st x on A holds ((( IncProj (C,b,B)) * ( IncProj (A,a,C))) . x) = ((( IncProj (Q,b,B)) * ( IncProj (A,q,Q))) . x)

      proof

        

         A58: {o9, b, oo9} on O2 & {o9, o, a} on O1 by A38, A43, A36, A30, A28, A22, INCSP_1: 2;

        

         A59: {o, q, oo9} on O3 & {b, q, a} on O by A18, A49, A23, A25, A24, INCSP_1: 2;

        

         A60: (O2,O1,C) are_mutually_distinct by A2, A4, A38, A30, A55, ZFMISC_1:def 5;

        let x such that

         A61: x on A;

        

         A62: {c, o, x} on A by A44, A19, A61, INCSP_1: 2;

        

         A63: x in ( dom f1) by A52, A61;

        

         A64: x in ( dom f) by A27, A61;

        consider Q1 such that

         A65: a on Q1 & x on Q1 by INCPROJ:def 5;

        consider x9 be POINT of IPP such that

         A66: x9 on Q1 and

         A67: x9 on C by INCPROJ:def 9;

        

         A68: {x, a, x9} on Q1 by A65, A66, INCSP_1: 2;

        

         A69: {o9, c, x9} on C by A41, A21, A67, INCSP_1: 2;

        consider Q2 such that

         A70: x9 on Q2 and

         A71: b on Q2 by INCPROJ:def 5;

        consider y such that

         A72: y on Q and

         A73: y on Q2 by INCPROJ:def 9;

        

         A74: {c, y, oo9} on Q by A56, A72, INCSP_1: 2;

         {b, y, x9} on Q2 by A70, A71, A73, INCSP_1: 2;

        then

        consider R such that

         A75: {y, q, x} on R by A1, A2, A4, A19, A21, A46, A58, A69, A62, A74, A68, A59, A60, PROJRED1: 12;

        

         A76: x on R by A75, INCSP_1: 2;

        y on R & q on R by A75, INCSP_1: 2;

        then

         A77: (f1 . x) = y by A48, A51, A61, A72, A76, PROJRED1:def 1;

        consider x99 be POINT of IPP such that

         A78: x99 on Q2 & x99 on B by INCPROJ:def 9;

        

         A79: (g1 . y) = x99 by A3, A5, A71, A78, A72, A73, PROJRED1:def 1;

        

         A80: (g . x9) = x99 by A3, A4, A67, A70, A71, A78, PROJRED1:def 1;

        (f . x) = x9 by A1, A2, A61, A65, A66, A67, PROJRED1:def 1;

        

        then ((g * f) . x) = (g1 . (f1 . x)) by A80, A77, A79, A64, FUNCT_1: 13

        .= ((g1 * f1) . x) by A63, FUNCT_1: 13;

        hence thesis;

      end;

       A81:

      now

        let y be object;

        assume y in X;

        then ex x st y = x & x on A;

        hence ((g * f) . y) = ((g1 * f1) . y) by A57;

      end;

      ( dom (g * f)) = X by A1, A2, A3, A4, A27, PROJRED1: 22;

      hence thesis by A53, A81, FUNCT_1: 2;

    end;

    theorem :: PROJRED2:16

    

     Th16: not a on A & not a on C & not b on C & not b on Q & not (A,B,C) are_concurrent & not (B,C,O) are_concurrent & A <> Q & Q <> C & a <> b & {c, p} on A & d on B & {c, d} on C & {a, b, q} on O & {c, pp9} on Q & {a, d, p} on O1 & {q, p, pp9} on O2 & {b, d, pp9} on O3 implies q <> a & q <> b & not q on A & not q on Q

    proof

      assume that

       A1: not a on A and

       A2: not a on C and

       A3: not b on C and

       A4: not b on Q and

       A5: not (A,B,C) are_concurrent and

       A6: not (B,C,O) are_concurrent and

       A7: A <> Q and

       A8: Q <> C and

       A9: a <> b and

       A10: {c, p} on A and

       A11: d on B and

       A12: {c, d} on C and

       A13: {a, b, q} on O and

       A14: {c, pp9} on Q and

       A15: {a, d, p} on O1 and

       A16: {q, p, pp9} on O2 and

       A17: {b, d, pp9} on O3;

      

       A18: d on C by A12, INCSP_1: 1;

      

       A19: c on C by A12, INCSP_1: 1;

      

       A20: c on A by A10, INCSP_1: 1;

      then

       A21: c <> d by A5, A11, A19;

      

       A22: d on O1 by A15, INCSP_1: 2;

      

       A23: pp9 on Q by A14, INCSP_1: 1;

      

       A24: pp9 on O3 by A17, INCSP_1: 2;

      

       A25: pp9 on O2 by A16, INCSP_1: 2;

      

       A26: a on O1 by A15, INCSP_1: 2;

      

       A27: b on O3 by A17, INCSP_1: 2;

      

       A28: d on O3 by A17, INCSP_1: 2;

      

       A29: q on O by A13, INCSP_1: 2;

      

       A30: b on O by A13, INCSP_1: 2;

      

       A31: q <> pp9

      proof

        assume not thesis;

        then O3 = O by A4, A30, A29, A27, A24, A23, INCPROJ:def 4;

        hence contradiction by A6, A11, A18, A28;

      end;

      

       A32: pp9 on O2 & q on O2 by A16, INCSP_1: 2;

      

       A33: pp9 on Q & p on O2 by A14, A16, INCSP_1: 1, INCSP_1: 2;

      

       A34: p on A by A10, INCSP_1: 1;

      

       A35: c on Q by A14, INCSP_1: 1;

      then

       A36: pp9 <> d by A8, A19, A18, A23, A21, INCPROJ:def 4;

      

       A37: O1 <> O2

      proof

        assume not thesis;

        then

         A38: a on O3 by A26, A22, A25, A28, A24, A36, INCPROJ:def 4;

        a on O & b on O by A13, INCSP_1: 2;

        then d on O by A9, A28, A27, A38, INCPROJ:def 4;

        hence contradiction by A6, A11, A18;

      end;

      

       A39: p on O1 by A15, INCSP_1: 2;

      then

       A40: p <> c by A2, A19, A18, A26, A22, A21, INCPROJ:def 4;

      

       A41: not q on Q

      proof

        assume not thesis;

        then p on Q by A33, A32, A31, INCPROJ:def 4;

        hence contradiction by A7, A20, A35, A34, A40, INCPROJ:def 4;

      end;

      

       A42: a on O by A13, INCSP_1: 2;

      

       A43: q <> p

      proof

        assume not thesis;

        then O = O1 by A1, A42, A26, A34, A39, A29, INCPROJ:def 4;

        hence contradiction by A6, A11, A18, A22;

      end;

      

       A44: p on O2 by A16, INCSP_1: 2;

      pp9 <> c by A3, A19, A18, A28, A27, A24, A21, INCPROJ:def 4;

      then

       A45: A <> O2 by A7, A20, A35, A25, A23, INCPROJ:def 4;

      

       A46: q on O2 by A16, INCSP_1: 2;

      

       A47: p <> d by A5, A11, A18, A34;

      q <> b

      proof

        assume not thesis;

        then O2 = O3 by A4, A46, A25, A27, A24, A23, INCPROJ:def 4;

        hence contradiction by A22, A39, A44, A28, A47, A37, INCPROJ:def 4;

      end;

      hence thesis by A26, A34, A39, A46, A44, A45, A37, A43, A41, INCPROJ:def 4;

    end;

    theorem :: PROJRED2:17

    

     Th17: not a on A & not a on C & not b on B & not b on C & not b on Q & not (A,B,C) are_concurrent & a <> b & A <> Q & {c, o} on A & {o, o99, d} on B & {c, d, o9} on C & {a, b, d} on O & {c, oo9} on Q & {a, o, o9} on O1 & {b, o9, oo9} on O2 & {o, oo9, q} on O3 & q on O implies not q on A & not q on Q & b <> q

    proof

      assume that

       A1: not a on A and

       A2: not a on C and

       A3: not b on B and

       A4: not b on C and

       A5: not b on Q and

       A6: not (A,B,C) are_concurrent and

       A7: a <> b and

       A8: A <> Q and

       A9: {c, o} on A and

       A10: {o, o99, d} on B and

       A11: {c, d, o9} on C and

       A12: {a, b, d} on O and

       A13: {c, oo9} on Q and

       A14: {a, o, o9} on O1 and

       A15: {b, o9, oo9} on O2 and

       A16: {o, oo9, q} on O3 and

       A17: q on O;

      

       A18: o on B by A10, INCSP_1: 2;

      

       A19: c on A & c on Q by A9, A13, INCSP_1: 1;

      

       A20: o on A by A9, INCSP_1: 1;

      

       A21: oo9 on O2 by A15, INCSP_1: 2;

      

       A22: b on O2 & oo9 on O2 by A15, INCSP_1: 2;

      

       A23: oo9 on Q by A13, INCSP_1: 1;

      

       A24: b on O2 by A15, INCSP_1: 2;

      

       A25: o on O1 by A14, INCSP_1: 2;

      

       A26: o on A by A9, INCSP_1: 1;

      

       A27: d on C by A11, INCSP_1: 2;

      then

       A28: o <> d by A6, A26, A18;

      

       A29: d on B by A10, INCSP_1: 2;

      

       A30: b on O by A12, INCSP_1: 2;

      

       A31: oo9 on Q by A13, INCSP_1: 1;

      

       A32: o9 on O2 by A15, INCSP_1: 2;

      

       A33: q on O3 by A16, INCSP_1: 2;

      

       A34: a on O1 by A14, INCSP_1: 2;

      

       A35: d on O by A12, INCSP_1: 2;

      

       A36: a on O by A12, INCSP_1: 2;

      

       A37: O1 <> O2

      proof

        assume not thesis;

        then o on O by A7, A36, A30, A34, A25, A24, INCPROJ:def 4;

        hence contradiction by A3, A18, A29, A30, A35, A28, INCPROJ:def 4;

      end;

      

       A38: o on O3 & oo9 on O3 by A16, INCSP_1: 2;

      

       A39: o9 on C by A11, INCSP_1: 2;

      then

       A40: o <> o9 by A6, A26, A18;

      

       A41: b <> q

      proof

        assume not thesis;

        then

         A42: o on O2 by A5, A23, A22, A38, A33, INCPROJ:def 4;

        

         A43: o9 on O2 by A15, INCSP_1: 2;

        o on O1 & o9 on O1 by A14, INCSP_1: 2;

        hence contradiction by A37, A40, A42, A43, INCPROJ:def 4;

      end;

      

       A44: c on A by A9, INCSP_1: 1;

      

       A45: c on C by A11, INCSP_1: 2;

      then

       A46: o <> c by A6, A44, A18;

      

       A47: o9 on O1 by A14, INCSP_1: 2;

      then o9 <> c by A1, A44, A26, A34, A25, A46, INCPROJ:def 4;

      then

       A48: c <> oo9 by A4, A45, A39, A24, A32, A21, INCPROJ:def 4;

      o9 <> d

      proof

        assume not thesis;

        then O1 = O by A2, A27, A36, A35, A34, A47, INCPROJ:def 4;

        hence contradiction by A3, A18, A29, A30, A35, A25, A28, INCPROJ:def 4;

      end;

      then O <> O2 by A2, A27, A39, A36, A35, A32, INCPROJ:def 4;

      then

       A49: q <> oo9 by A5, A17, A30, A31, A24, A21, INCPROJ:def 4;

      

       A50: c on Q by A13, INCSP_1: 1;

      

       A51: not q on Q

      proof

        assume not thesis;

        then o on Q by A23, A38, A33, A49, INCPROJ:def 4;

        hence contradiction by A8, A44, A26, A50, A46, INCPROJ:def 4;

      end;

      

       A52: q <> o by A3, A17, A18, A29, A30, A35, A28, INCPROJ:def 4;

       not q on A

      proof

        assume not thesis;

        then oo9 on A by A20, A38, A33, A52, INCPROJ:def 4;

        hence contradiction by A8, A19, A23, A48, INCPROJ:def 4;

      end;

      hence thesis by A51, A41;

    end;

    theorem :: PROJRED2:18

    

     Th18: not a on A & not a on C & not b on C & not q on A & not (A,B,C) are_concurrent & not (B,C,O) are_concurrent & a <> b & b <> q & q <> a & {c, p} on A & d on B & {c, d} on C & {a, b, q} on O & {c, pp9} on Q & {a, d, p} on O1 & {q, p, pp9} on O2 & {b, d, pp9} on O3 implies Q <> A & Q <> C & not q on Q & not b on Q

    proof

      assume that

       A1: not a on A and

       A2: not a on C and

       A3: not b on C and

       A4: not q on A and

       A5: not (A,B,C) are_concurrent and

       A6: not (B,C,O) are_concurrent and

       A7: a <> b and

       A8: b <> q and

       A9: q <> a and

       A10: {c, p} on A and

       A11: d on B and

       A12: {c, d} on C and

       A13: {a, b, q} on O and

       A14: {c, pp9} on Q and

       A15: {a, d, p} on O1 and

       A16: {q, p, pp9} on O2 and

       A17: {b, d, pp9} on O3;

      

       A18: d on C by A12, INCSP_1: 1;

      

       A19: c on C by A12, INCSP_1: 1;

      

       A20: c on A by A10, INCSP_1: 1;

      then

       A21: c <> d by A5, A11, A19;

      

       A22: pp9 on O3 by A17, INCSP_1: 2;

      

       A23: p on O2 by A16, INCSP_1: 2;

      

       A24: pp9 on Q by A14, INCSP_1: 1;

      

       A25: q on O by A13, INCSP_1: 2;

      

       A26: a on O by A13, INCSP_1: 2;

      

       A27: b on O3 by A17, INCSP_1: 2;

      

       A28: d on O1 by A15, INCSP_1: 2;

      then

       A29: O <> O1 by A6, A11, A18;

      

       A30: p on O1 by A15, INCSP_1: 2;

      

       A31: p on O2 by A16, INCSP_1: 2;

      

       A32: a on O1 by A15, INCSP_1: 2;

      

       A33: pp9 on O2 by A16, INCSP_1: 2;

      

       A34: q on O2 by A16, INCSP_1: 2;

      

       A35: p on A by A10, INCSP_1: 1;

      then

       A36: p <> d by A5, A11, A18;

      

       A37: pp9 <> d

      proof

        assume not thesis;

        then

         A38: q on O1 by A28, A30, A34, A31, A33, A36, INCPROJ:def 4;

        a on O & q on O by A13, INCSP_1: 2;

        hence contradiction by A9, A32, A29, A38, INCPROJ:def 4;

      end;

      

       A39: d on O3 by A17, INCSP_1: 2;

      

       A40: b on O by A13, INCSP_1: 2;

      

       A41: p <> pp9

      proof

        assume not thesis;

        then O1 = O3 by A28, A30, A39, A22, A36, INCPROJ:def 4;

        hence contradiction by A7, A26, A40, A32, A27, A29, INCPROJ:def 4;

      end;

      

       A42: c on Q by A14, INCSP_1: 1;

      then

       A43: O3 <> Q by A3, A19, A18, A39, A27, A21, INCPROJ:def 4;

      

       A44: not b on Q

      proof

        assume not thesis;

        then

         A45: b on O2 by A33, A27, A22, A24, A43, INCPROJ:def 4;

        

         A46: q on O by A13, INCSP_1: 2;

        q on O2 & b on O by A13, A16, INCSP_1: 2;

        then p on O by A8, A23, A45, A46, INCPROJ:def 4;

        hence contradiction by A1, A26, A32, A35, A30, A29, INCPROJ:def 4;

      end;

      p <> c by A2, A19, A18, A32, A28, A30, A21, INCPROJ:def 4;

      then

       A47: O2 <> Q by A4, A20, A42, A35, A34, A31, INCPROJ:def 4;

      

       A48: O <> O3 by A6, A11, A18, A39;

       not q on Q

      proof

        assume not thesis;

        then q = pp9 by A34, A33, A24, A47, INCPROJ:def 4;

        hence contradiction by A8, A40, A25, A27, A22, A48, INCPROJ:def 4;

      end;

      hence thesis by A18, A35, A34, A31, A33, A39, A27, A22, A24, A41, A37, A44, INCPROJ:def 4;

    end;

    theorem :: PROJRED2:19

    

     Th19: not a on A & not a on C & not b on B & not b on C & not q on A & not (A,B,C) are_concurrent & a <> b & b <> q & {c, o} on A & {o, o99, d} on B & {c, d, o9} on C & {a, b, d} on O & {c, oo9} on Q & {a, o, o9} on O1 & {b, o9, oo9} on O2 & {o, oo9, q} on O3 & q on O implies not b on Q & not q on Q & A <> Q

    proof

      assume that

       A1: not a on A and

       A2: not a on C and

       A3: not b on B and

       A4: not b on C and

       A5: not q on A and

       A6: not (A,B,C) are_concurrent and

       A7: a <> b and

       A8: b <> q and

       A9: {c, o} on A and

       A10: {o, o99, d} on B and

       A11: {c, d, o9} on C and

       A12: {a, b, d} on O and

       A13: {c, oo9} on Q and

       A14: {a, o, o9} on O1 and

       A15: {b, o9, oo9} on O2 and

       A16: {o, oo9, q} on O3 and

       A17: q on O;

      

       A18: o on A by A9, INCSP_1: 1;

      

       A19: d on B & d on O by A10, A12, INCSP_1: 2;

      

       A20: o on B by A10, INCSP_1: 2;

      

       A21: o on B by A10, INCSP_1: 2;

      

       A22: d on C by A11, INCSP_1: 2;

      then

       A23: o <> d by A6, A18, A21;

      

       A24: o on O3 by A16, INCSP_1: 2;

      

       A25: b <> oo9

      proof

        assume not thesis;

        then

         A26: b on O3 by A16, INCSP_1: 2;

        q on O3 & b on O by A12, A16, INCSP_1: 2;

        then o on O by A8, A17, A24, A26, INCPROJ:def 4;

        then O = B by A19, A20, A23, INCPROJ:def 4;

        hence contradiction by A3, A12, INCSP_1: 2;

      end;

      

       A27: oo9 on O2 by A15, INCSP_1: 2;

      

       A28: C <> O2 by A4, A15, INCSP_1: 2;

      

       A29: o9 on O1 by A14, INCSP_1: 2;

      

       A30: oo9 on O2 by A15, INCSP_1: 2;

      

       A31: oo9 on Q by A13, INCSP_1: 1;

      

       A32: c on Q & b on O2 by A13, A15, INCSP_1: 1, INCSP_1: 2;

      

       A33: c on A by A9, INCSP_1: 1;

      

       A34: a on O1 by A14, INCSP_1: 2;

      

       A35: b on O by A12, INCSP_1: 2;

      

       A36: o on O1 by A14, INCSP_1: 2;

      c on C by A11, INCSP_1: 2;

      then

       A37: o <> c by A6, A33, A21;

      then

       A38: o9 <> c by A1, A33, A18, A34, A36, A29, INCPROJ:def 4;

      

       A39: not b on Q

      proof

        assume not thesis;

        then

         A40: c on O2 by A32, A31, A30, A25, INCPROJ:def 4;

        

         A41: o9 on O2 by A15, INCSP_1: 2;

        o9 on C & c on C by A11, INCSP_1: 2;

        hence contradiction by A38, A28, A41, A40, INCPROJ:def 4;

      end;

      

       A42: c on Q by A13, INCSP_1: 1;

      

       A43: o9 on C by A11, INCSP_1: 2;

      

       A44: a on O by A12, INCSP_1: 2;

      

       A45: b on O2 by A15, INCSP_1: 2;

      

       A46: O1 <> O2

      proof

        assume not thesis;

        then o on O by A7, A44, A35, A34, A36, A45, INCPROJ:def 4;

        then O = B by A19, A20, A23, INCPROJ:def 4;

        hence contradiction by A3, A12, INCSP_1: 2;

      end;

      

       A47: o on O3 & q on O3 by A16, INCSP_1: 2;

      

       A48: oo9 on Q & oo9 on O3 by A13, A16, INCSP_1: 1, INCSP_1: 2;

      

       A49: o9 on O2 by A15, INCSP_1: 2;

      

       A50: oo9 on O3 & q on O3 by A16, INCSP_1: 2;

      

       A51: d on O by A12, INCSP_1: 2;

      

       A52: d on B by A10, INCSP_1: 2;

      o9 <> d

      proof

        assume not thesis;

        then O1 = O by A2, A22, A44, A51, A34, A29, INCPROJ:def 4;

        hence contradiction by A3, A21, A52, A35, A51, A36, A23, INCPROJ:def 4;

      end;

      then O <> O2 by A2, A22, A43, A44, A51, A49, INCPROJ:def 4;

      then

       A53: q <> oo9 by A8, A17, A35, A45, A27, INCPROJ:def 4;

      

       A54: not q on Q

      proof

        assume not thesis;

        then Q = O3 by A31, A50, A53, INCPROJ:def 4;

        hence contradiction by A5, A33, A18, A42, A47, A37, INCPROJ:def 4;

      end;

      o <> o9 by A6, A18, A21, A43;

      then o <> oo9 by A36, A29, A49, A27, A46, INCPROJ:def 4;

      hence thesis by A18, A48, A47, A39, A54, INCPROJ:def 4;

    end;

    

     Lm1: not a on A & not b on B & not a on C & not b on C & not (A,B,C) are_concurrent & (A,C,Q) are_concurrent & not b on Q & A <> Q & a <> b & a on O & b on O & not (B,C,O) are_concurrent implies ex q st q on O & not q on A & not q on Q & (( IncProj (C,b,B)) * ( IncProj (A,a,C))) = (( IncProj (Q,b,B)) * ( IncProj (A,q,Q)))

    proof

      assume that

       A1: not a on A and

       A2: not b on B and

       A3: not a on C and

       A4: ( not b on C) & not (A,B,C) are_concurrent and

       A5: (A,C,Q) are_concurrent and

       A6: ( not b on Q) & A <> Q and

       A7: a <> b and

       A8: a on O and

       A9: b on O and

       A10: not (B,C,O) are_concurrent ;

      consider c such that

       A11: c on A & c on C and

       A12: c on Q by A5;

      consider d such that

       A13: d on C and

       A14: d on B by INCPROJ:def 9;

      consider O1 such that

       A15: a on O1 & d on O1 by INCPROJ:def 5;

      consider O3 such that

       A16: b on O3 & d on O3 by INCPROJ:def 5;

      consider pp9 be POINT of IPP such that

       A17: pp9 on O3 and

       A18: pp9 on Q by INCPROJ:def 9;

      consider p such that

       A19: p on A and

       A20: p on O1 by INCPROJ:def 9;

      consider O2 such that

       A21: p on O2 & pp9 on O2 by INCPROJ:def 5;

      consider q such that

       A22: q on O and

       A23: q on O2 by INCPROJ:def 9;

      now

        assume

         A24: Q <> C;

        take q;

        

         A25: {b, d, pp9} on O3 by A16, A17, INCSP_1: 2;

        

         A26: {a, d, p} on O1 & {q, p, pp9} on O2 by A15, A20, A21, A23, INCSP_1: 2;

        

         A27: {c, p} on A & {c, d} on C by A11, A13, A19, INCSP_1: 1;

        

         A28: {a, b, q} on O & {c, pp9} on Q by A8, A9, A12, A18, A22, INCSP_1: 1, INCSP_1: 2;

        then

         A29: ( not q on A) & not q on Q by A1, A3, A4, A6, A7, A10, A14, A24, A27, A26, A25, Th16;

        q <> a by A1, A3, A4, A6, A7, A10, A14, A24, A27, A28, A26, A25, Th16;

        then (( IncProj (C,b,B)) * ( IncProj (A,a,C))) = (( IncProj (Q,b,B)) * ( IncProj (A,q,Q))) by A1, A2, A3, A4, A6, A8, A9, A10, A11, A12, A13, A14, A15, A16, A19, A20, A17, A18, A21, A22, A23, A29, Th14;

        hence thesis by A22, A29;

      end;

      hence thesis by A1, A3, A8;

    end;

    

     Lm2: not a on A & not b on B & not a on C & not b on C & not (A,B,C) are_concurrent & (A,C,Q) are_concurrent & not b on Q & A <> Q & a <> b & a on O & b on O & (B,C,O) are_concurrent implies ex q st q on O & not q on A & not q on Q & (( IncProj (C,b,B)) * ( IncProj (A,a,C))) = (( IncProj (Q,b,B)) * ( IncProj (A,q,Q)))

    proof

      assume that

       A1: ( not a on A) & not b on B & ( not a on C) & not b on C & not (A,B,C) are_concurrent and

       A2: (A,C,Q) are_concurrent and

       A3: ( not b on Q) & A <> Q & a <> b and

       A4: a on O & b on O and

       A5: (B,C,O) are_concurrent ;

      consider d such that

       A6: d on B and

       A7: d on C and

       A8: d on O by A5;

      

       A9: {a, b, d} on O by A4, A8, INCSP_1: 2;

      consider o such that

       A10: o on A and

       A11: o on B by INCPROJ:def 9;

      consider O1 such that

       A12: o on O1 & a on O1 by INCPROJ:def 5;

      consider o9 be POINT of IPP such that

       A13: o9 on C and

       A14: o9 on O1 by INCPROJ:def 9;

      

       A15: {a, o, o9} on O1 by A12, A14, INCSP_1: 2;

      consider c such that

       A16: c on A and

       A17: c on C and

       A18: c on Q by A2;

      

       A19: {c, o} on A by A16, A10, INCSP_1: 1;

      

       A20: {c, d, o9} on C by A17, A7, A13, INCSP_1: 2;

      

       A21: {c, o} on A by A16, A10, INCSP_1: 1;

      

       A22: {c, d, o9} on C by A17, A7, A13, INCSP_1: 2;

      consider O2 such that

       A23: b on O2 & o9 on O2 by INCPROJ:def 5;

      consider oo9 be POINT of IPP such that

       A24: oo9 on Q and

       A25: oo9 on O2 by INCPROJ:def 9;

      

       A26: {b, o9, oo9} on O2 by A23, A25, INCSP_1: 2;

      consider o99 be POINT of IPP such that

       A27: o99 on B and o99 on O2 by INCPROJ:def 9;

      consider O3 such that

       A28: o on O3 & oo9 on O3 by INCPROJ:def 5;

      

       A29: {o, o99, d} on B by A6, A11, A27, INCSP_1: 2;

      

       A30: {b, o9, oo9} on O2 by A23, A25, INCSP_1: 2;

      

       A31: {a, o, o9} on O1 by A12, A14, INCSP_1: 2;

      

       A32: {a, b, d} on O by A4, A8, INCSP_1: 2;

      consider q such that

       A33: q on O3 and

       A34: q on O by INCPROJ:def 9;

      

       A35: {o, oo9, q} on O3 by A28, A33, INCSP_1: 2;

      

       A36: {c, oo9} on Q by A18, A24, INCSP_1: 1;

      

       A37: {o, o99, d} on B by A6, A11, A27, INCSP_1: 2;

      then

       A38: ( not q on A) & not q on Q by A1, A3, A34, A19, A22, A9, A36, A15, A26, A35, Th17;

      

       A39: {o, oo9, q} on O3 by A28, A33, INCSP_1: 2;

      

       A40: {c, oo9} on Q by A18, A24, INCSP_1: 1;

      b <> q by A1, A3, A34, A19, A37, A22, A9, A36, A15, A26, A35, Th17;

      then (( IncProj (C,b,B)) * ( IncProj (A,a,C))) = (( IncProj (Q,b,B)) * ( IncProj (A,q,Q))) by A1, A3, A34, A21, A29, A20, A32, A40, A31, A30, A39, Th15;

      hence thesis by A34, A38;

    end;

    theorem :: PROJRED2:20

    

     Th20: not a on A & not b on B & not a on C & not b on C & not (A,B,C) are_concurrent & (A,C,Q) are_concurrent & not b on Q & A <> Q & a <> b & a on O & b on O implies ex q st q on O & not q on A & not q on Q & (( IncProj (C,b,B)) * ( IncProj (A,a,C))) = (( IncProj (Q,b,B)) * ( IncProj (A,q,Q)))

    proof

      assume

       A1: ( not a on A) & not b on B & ( not a on C) & not b on C & ( not (A,B,C) are_concurrent ) & (A,C,Q) are_concurrent & ( not b on Q) & A <> Q & a <> b & a on O & b on O;

      then not (B,C,O) are_concurrent implies thesis by Lm1;

      hence thesis by A1, Lm2;

    end;

    theorem :: PROJRED2:21

     not a on A & not b on B & not a on C & not b on C & not (A,B,C) are_concurrent & (B,C,Q) are_concurrent & not a on Q & B <> Q & a <> b & a on O & b on O implies ex q st q on O & not q on B & not q on Q & (( IncProj (C,b,B)) * ( IncProj (A,a,C))) = (( IncProj (Q,q,B)) * ( IncProj (A,a,Q)))

    proof

      assume that

       A1: not a on A and

       A2: not b on B and

       A3: not a on C and

       A4: not b on C and

       A5: not (A,B,C) are_concurrent and

       A6: (B,C,Q) are_concurrent and

       A7: not a on Q and

       A8: B <> Q & a <> b & a on O & b on O;

      

       A9: ( IncProj (B,b,C)) is one-to-one & ( IncProj (C,a,A)) is one-to-one by A1, A2, A3, A4, Th7;

       not (B,A,C) are_concurrent by A5;

      then

      consider q such that

       A10: q on O and

       A11: ( not q on B) & not q on Q and

       A12: (( IncProj (C,a,A)) * ( IncProj (B,b,C))) = (( IncProj (Q,a,A)) * ( IncProj (B,q,Q))) by A1, A2, A3, A4, A6, A7, A8, Th20;

      take q;

      thus q on O & not q on B & not q on Q by A10, A11;

      

       A13: ( IncProj (B,q,Q)) is one-to-one by A11, Th7;

      

       A14: ( IncProj (Q,a,A)) is one-to-one by A1, A7, Th7;

      

      thus (( IncProj (C,b,B)) * ( IncProj (A,a,C))) = ((( IncProj (B,b,C)) " ) * ( IncProj (A,a,C))) by A2, A4, Th8

      .= ((( IncProj (B,b,C)) " ) * (( IncProj (C,a,A)) " )) by A1, A3, Th8

      .= ((( IncProj (Q,a,A)) * ( IncProj (B,q,Q))) " ) by A12, A9, FUNCT_1: 44

      .= ((( IncProj (B,q,Q)) " ) * (( IncProj (Q,a,A)) " )) by A13, A14, FUNCT_1: 44

      .= (( IncProj (Q,q,B)) * (( IncProj (Q,a,A)) " )) by A11, Th8

      .= (( IncProj (Q,q,B)) * ( IncProj (A,a,Q))) by A1, A7, Th8;

    end;

    theorem :: PROJRED2:22

     not a on A & not b on B & not a on C & not b on C & not a on B & not b on A & c on A & c on C & d on B & d on C & a on S & d on S & c on R & b on R & s on A & s on S & r on B & r on R & s on Q & r on Q & not (A,B,C) are_concurrent implies (( IncProj (C,b,B)) * ( IncProj (A,a,C))) = (( IncProj (Q,a,B)) * ( IncProj (A,b,Q)))

    proof

      assume that

       A1: not a on A and

       A2: not b on B and

       A3: not a on C and

       A4: not b on C and

       A5: not a on B and

       A6: not b on A and

       A7: c on A and

       A8: c on C and

       A9: d on B and

       A10: d on C and

       A11: a on S and

       A12: d on S and

       A13: c on R and

       A14: b on R and

       A15: s on A and

       A16: s on S and

       A17: r on B and

       A18: r on R and

       A19: s on Q and

       A20: r on Q and

       A21: not (A,B,C) are_concurrent ;

      

       A22: c <> d by A7, A8, A9, A21;

      then

       A23: c <> s by A3, A8, A10, A11, A12, A16, INCPROJ:def 4;

       A24:

      now

        assume b on Q;

        then R = Q by A2, A14, A17, A18, A20, INCPROJ:def 4;

        hence contradiction by A6, A7, A13, A14, A15, A19, A23, INCPROJ:def 4;

      end;

      

       A25: d <> r by A4, A8, A10, A13, A14, A18, A22, INCPROJ:def 4;

       A26:

      now

        assume a on Q;

        then S = Q by A1, A11, A15, A16, A19, INCPROJ:def 4;

        hence contradiction by A5, A9, A11, A12, A17, A20, A25, INCPROJ:def 4;

      end;

      set X = ( CHAIN A);

      set f = ( IncProj (A,a,C)), g = ( IncProj (C,b,B)), g1 = ( IncProj (Q,a,B)), f1 = ( IncProj (A,b,Q));

      

       A27: ( dom f) = ( CHAIN A) by A1, A3, Th4;

      

       A28: ( dom f1) = ( CHAIN A) by A6, A24, Th4;

      then

       A29: ( dom (g1 * f1)) = X by A5, A6, A26, A24, PROJRED1: 22;

      A <> C by A21, Th1;

      then

       A30: (C,A,R) are_mutually_distinct by A4, A6, A14, ZFMISC_1:def 5;

      

       A31: c <> d by A7, A8, A9, A21;

      

       A32: for x st x on A holds ((( IncProj (C,b,B)) * ( IncProj (A,a,C))) . x) = ((( IncProj (Q,a,B)) * ( IncProj (A,b,Q))) . x)

      proof

        let x;

        assume

         A33: x on A;

        then

        reconsider x9 = (f . x), y = (f1 . x) as POINT of IPP by A1, A3, A6, A24, PROJRED1: 19;

        

         A34: x in ( dom f1) by A28, A33;

        

         A35: x9 on C by A1, A3, A33, PROJRED1: 20;

        then

        reconsider x99 = (g . x9) as POINT of IPP by A2, A4, PROJRED1: 19;

        consider O1 such that

         A36: a on O1 & x on O1 & x9 on O1 by A1, A3, A33, A35, PROJRED1:def 1;

        

         A37: y on Q by A6, A24, A33, PROJRED1: 20;

        then

        consider O3 such that

         A38: b on O3 & x on O3 & y on O3 by A6, A24, A33, PROJRED1:def 1;

        

         A39: x99 on B by A2, A4, A35, PROJRED1: 20;

        then

        consider O2 such that

         A40: b on O2 & x9 on O2 & x99 on O2 by A2, A4, A35, PROJRED1:def 1;

         A41:

        now

          

           A42: {y, s, r} on Q & {d, x99, r} on B by A9, A17, A19, A20, A37, A39, INCSP_1: 2;

          assume

           A43: s <> x;

          

           A44: {d, a, s} on S by A11, A12, A16, INCSP_1: 2;

          

           A45: {c, b, r} on R & {b, x, y} on O3 by A13, A14, A18, A38, INCSP_1: 2;

          

           A46: {b, x99, x9} on O2 & {x, a, x9} on O1 by A36, A40, INCSP_1: 2;

           {c, d, x9} on C & {c, x, s} on A by A7, A8, A10, A15, A33, A35, INCSP_1: 2;

          then

          consider O4 such that

           A47: {x99, a, y} on O4 by A6, A7, A31, A23, A30, A43, A45, A46, A42, A44, PROJRED1: 12;

          

           A48: y on O4 by A47, INCSP_1: 2;

          x99 on O4 & a on O4 by A47, INCSP_1: 2;

          hence (g . (f . x)) = (g1 . (f1 . x)) by A5, A26, A37, A39, A48, PROJRED1:def 1;

        end;

         A49:

        now

          assume

           A50: s = x;

          then x9 = d by A1, A3, A10, A11, A12, A15, A16, PROJRED1:def 1;

          then

           A51: x99 = d by A2, A4, A9, A10, PROJRED1: 24;

          y = s by A6, A15, A19, A24, A50, PROJRED1: 24;

          hence (g . (f . x)) = (g1 . (f1 . x)) by A5, A9, A11, A12, A16, A19, A26, A51, PROJRED1:def 1;

        end;

        x in ( dom f) by A27, A33;

        

        then ((g * f) . x) = (g1 . (f1 . x)) by A49, A41, FUNCT_1: 13

        .= ((g1 * f1) . x) by A34, FUNCT_1: 13;

        hence thesis;

      end;

       A52:

      now

        let y be object;

        assume y in X;

        then ex x st y = x & x on A;

        hence ((g * f) . y) = ((g1 * f1) . y) by A32;

      end;

      ( dom (g * f)) = X by A1, A2, A3, A4, A27, PROJRED1: 22;

      hence thesis by A29, A52, FUNCT_1: 2;

    end;

    

     Lm3: not a on A & not b on B & not a on C & not b on C & c on A & c on C & a <> b & a on O & b on O & q on O & not q on A & q <> b & not (A,B,C) are_concurrent & not (B,C,O) are_concurrent implies ex Q st c on Q & not b on Q & not q on Q & (( IncProj (C,b,B)) * ( IncProj (A,a,C))) = (( IncProj (Q,b,B)) * ( IncProj (A,q,Q)))

    proof

      assume that

       A1: not a on A and

       A2: not b on B and

       A3: ( not a on C) & not b on C and

       A4: c on A and

       A5: c on C and

       A6: a <> b and

       A7: a on O & b on O & q on O and

       A8: not q on A and

       A9: q <> b and

       A10: ( not (A,B,C) are_concurrent ) & not (B,C,O) are_concurrent ;

      consider d such that

       A11: d on C and

       A12: d on B by INCPROJ:def 9;

      consider O1 such that

       A13: a on O1 & d on O1 by INCPROJ:def 5;

      consider O3 such that

       A14: b on O3 & d on O3 by INCPROJ:def 5;

      consider p such that

       A15: p on A and

       A16: p on O1 by INCPROJ:def 9;

      consider O2 such that

       A17: q on O2 & p on O2 by INCPROJ:def 5;

      consider pp9 be POINT of IPP such that

       A18: pp9 on O3 and

       A19: pp9 on O2 by INCPROJ:def 9;

      consider Q such that

       A20: c on Q and

       A21: pp9 on Q by INCPROJ:def 5;

      now

        

         A22: {a, b, q} on O & {c, pp9} on Q by A7, A20, A21, INCSP_1: 1, INCSP_1: 2;

        

         A23: {b, d, pp9} on O3 by A14, A18, INCSP_1: 2;

        

         A24: {a, d, p} on O1 & {q, p, pp9} on O2 by A13, A16, A17, A19, INCSP_1: 2;

        assume

         A25: q <> a;

        

         A26: {c, p} on A & {c, d} on C by A4, A5, A11, A15, INCSP_1: 1;

        then

         A27: ( not q on Q) & not b on Q by A1, A3, A6, A8, A9, A10, A12, A25, A22, A24, A23, Th18;

        Q <> A by A1, A3, A6, A8, A9, A10, A12, A25, A26, A22, A24, A23, Th18;

        then (( IncProj (C,b,B)) * ( IncProj (A,a,C))) = (( IncProj (Q,b,B)) * ( IncProj (A,q,Q))) by A1, A2, A3, A4, A5, A7, A8, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, A21, A25, A27, Th14;

        hence thesis by A20, A27;

      end;

      hence thesis by A3, A5;

    end;

    

     Lm4: not a on A & not b on B & not a on C & not b on C & c on A & c on C & a <> b & a on O & b on O & q on O & not q on A & q <> b & not (A,B,C) are_concurrent & (B,C,O) are_concurrent implies ex Q st c on Q & not b on Q & not q on Q & (( IncProj (C,b,B)) * ( IncProj (A,a,C))) = (( IncProj (Q,b,B)) * ( IncProj (A,q,Q)))

    proof

      assume that

       A1: ( not a on A) & not b on B & ( not a on C) & not b on C and

       A2: c on A and

       A3: c on C and

       A4: a <> b and

       A5: a on O & b on O and

       A6: q on O and

       A7: not q on A and

       A8: q <> b & not (A,B,C) are_concurrent and

       A9: (B,C,O) are_concurrent ;

      consider d such that

       A10: d on B and

       A11: d on C and

       A12: d on O by A9;

      

       A13: {a, b, d} on O by A5, A12, INCSP_1: 2;

      consider o such that

       A14: o on A and

       A15: o on B by INCPROJ:def 9;

      consider O1 such that

       A16: o on O1 & a on O1 by INCPROJ:def 5;

      consider o9 be POINT of IPP such that

       A17: o9 on C and

       A18: o9 on O1 by INCPROJ:def 9;

      

       A19: {a, o, o9} on O1 by A16, A18, INCSP_1: 2;

      

       A20: {a, o, o9} on O1 by A16, A18, INCSP_1: 2;

      

       A21: {c, d, o9} on C by A3, A11, A17, INCSP_1: 2;

      

       A22: {c, d, o9} on C by A3, A11, A17, INCSP_1: 2;

      consider O2 such that

       A23: b on O2 & o9 on O2 by INCPROJ:def 5;

      

       A24: {a, b, d} on O by A5, A12, INCSP_1: 2;

      

       A25: {c, o} on A by A2, A14, INCSP_1: 1;

      

       A26: {c, o} on A by A2, A14, INCSP_1: 1;

      consider O3 such that

       A27: q on O3 & o on O3 by INCPROJ:def 5;

      consider o99 be POINT of IPP such that

       A28: o99 on B and o99 on O2 by INCPROJ:def 9;

      

       A29: {o, o99, d} on B by A10, A15, A28, INCSP_1: 2;

      consider oo9 be POINT of IPP such that

       A30: oo9 on O2 and

       A31: oo9 on O3 by INCPROJ:def 9;

      

       A32: {b, o9, oo9} on O2 by A23, A30, INCSP_1: 2;

      

       A33: {o, oo9, q} on O3 by A27, A31, INCSP_1: 2;

      

       A34: {o, oo9, q} on O3 by A27, A31, INCSP_1: 2;

      

       A35: {b, o9, oo9} on O2 by A23, A30, INCSP_1: 2;

      consider Q such that

       A36: c on Q and

       A37: oo9 on Q by INCPROJ:def 5;

      

       A38: {c, oo9} on Q by A36, A37, INCSP_1: 1;

      

       A39: {c, oo9} on Q by A36, A37, INCSP_1: 1;

      

       A40: {o, o99, d} on B by A10, A15, A28, INCSP_1: 2;

      then ( not b on Q) & A <> Q by A1, A4, A6, A7, A8, A25, A21, A13, A38, A19, A32, A34, Th19;

      then

       A41: (( IncProj (C,b,B)) * ( IncProj (A,a,C))) = (( IncProj (Q,b,B)) * ( IncProj (A,q,Q))) by A1, A4, A6, A8, A26, A29, A22, A24, A39, A20, A35, A33, Th15;

      ( not b on Q) & not q on Q by A1, A4, A6, A7, A8, A25, A40, A21, A13, A38, A19, A32, A34, Th19;

      hence thesis by A36, A41;

    end;

    theorem :: PROJRED2:23

    

     Th23: not a on A & not b on B & not a on C & not b on C & a <> b & a on O & b on O & q on O & not q on A & q <> b & not (A,B,C) are_concurrent implies ex Q st (A,C,Q) are_concurrent & not b on Q & not q on Q & (( IncProj (C,b,B)) * ( IncProj (A,a,C))) = (( IncProj (Q,b,B)) * ( IncProj (A,q,Q)))

    proof

      consider c such that

       A1: c on A & c on C by INCPROJ:def 9;

      assume

       A2: ( not a on A) & not b on B & ( not a on C) & not b on C & a <> b & a on O & b on O & q on O & ( not q on A) & q <> b & not (A,B,C) are_concurrent ;

       A3:

      now

        assume (B,C,O) are_concurrent ;

        then

        consider Q such that

         A4: c on Q and

         A5: ( not b on Q) & not q on Q & (( IncProj (C,b,B)) * ( IncProj (A,a,C))) = (( IncProj (Q,b,B)) * ( IncProj (A,q,Q))) by A2, A1, Lm4;

        take Q;

        thus (A,C,Q) are_concurrent by A1, A4;

        thus not b on Q & not q on Q & (( IncProj (C,b,B)) * ( IncProj (A,a,C))) = (( IncProj (Q,b,B)) * ( IncProj (A,q,Q))) by A5;

      end;

      now

        assume not (B,C,O) are_concurrent ;

        then

        consider Q such that

         A6: c on Q and

         A7: ( not b on Q) & not q on Q & (( IncProj (C,b,B)) * ( IncProj (A,a,C))) = (( IncProj (Q,b,B)) * ( IncProj (A,q,Q))) by A2, A1, Lm3;

        take Q;

        thus (A,C,Q) are_concurrent by A1, A6;

        thus not b on Q & not q on Q & (( IncProj (C,b,B)) * ( IncProj (A,a,C))) = (( IncProj (Q,b,B)) * ( IncProj (A,q,Q))) by A7;

      end;

      hence thesis by A3;

    end;

    theorem :: PROJRED2:24

     not a on A & not b on B & not a on C & not b on C & a <> b & a on O & b on O & q on O & not q on B & q <> a & not (A,B,C) are_concurrent implies ex Q st (B,C,Q) are_concurrent & not a on Q & not q on Q & (( IncProj (C,b,B)) * ( IncProj (A,a,C))) = (( IncProj (Q,q,B)) * ( IncProj (A,a,Q)))

    proof

      assume that

       A1: not a on A and

       A2: not b on B and

       A3: not a on C and

       A4: not b on C and

       A5: a <> b & a on O & b on O & q on O and

       A6: not q on B and

       A7: q <> a and

       A8: not (A,B,C) are_concurrent ;

      

       A9: ( IncProj (C,a,A)) is one-to-one & ( IncProj (B,b,C)) is one-to-one by A1, A2, A3, A4, Th7;

       not (B,A,C) are_concurrent by A8;

      then

      consider Q such that

       A10: (B,C,Q) are_concurrent and

       A11: not a on Q and

       A12: not q on Q and

       A13: (( IncProj (C,a,A)) * ( IncProj (B,b,C))) = (( IncProj (Q,a,A)) * ( IncProj (B,q,Q))) by A1, A2, A3, A4, A5, A6, A7, Th23;

      

       A14: ( IncProj (Q,a,A)) is one-to-one & ( IncProj (B,q,Q)) is one-to-one by A1, A6, A11, A12, Th7;

      take Q;

      thus (B,C,Q) are_concurrent & not a on Q & not q on Q by A10, A11, A12;

      

      thus (( IncProj (C,b,B)) * ( IncProj (A,a,C))) = ((( IncProj (B,b,C)) " ) * ( IncProj (A,a,C))) by A2, A4, Th8

      .= ((( IncProj (B,b,C)) " ) * (( IncProj (C,a,A)) " )) by A1, A3, Th8

      .= ((( IncProj (Q,a,A)) * ( IncProj (B,q,Q))) " ) by A13, A9, FUNCT_1: 44

      .= ((( IncProj (B,q,Q)) " ) * (( IncProj (Q,a,A)) " )) by A14, FUNCT_1: 44

      .= ((( IncProj (B,q,Q)) " ) * ( IncProj (A,a,Q))) by A1, A11, Th8

      .= (( IncProj (Q,q,B)) * ( IncProj (A,a,Q))) by A6, A12, Th8;

    end;