menelaus.miz



    begin

    reserve A,B,C,A1,B1,C1,A2,B2,C2,C3 for Point of ( TOP-REAL 2),

lambda,mu,nu,alpha,beta,gamma for Real,

X,Y,Z for Subset of ( TOP-REAL 2);

    notation

      let X, Y;

      synonym X is_parallel_to Y for X misses Y;

    end

    definition

      let X, Y, Z;

      :: MENELAUS:def1

      pred X,Y,Z are_concurrent means ((X is_parallel_to Y & Y is_parallel_to Z & Z is_parallel_to X) or ex A st (A in X & A in Y & A in Z));

    end

    theorem :: MENELAUS:1

    

     Th1: ((A + B) `1 ) = ((A `1 ) + (B `1 )) & ((A + B) `2 ) = ((A `2 ) + (B `2 ))

    proof

      (A + B) = |[((A `1 ) + (B `1 )), ((A `2 ) + (B `2 ))]| by EUCLID: 55;

      hence thesis by EUCLID: 52;

    end;

    theorem :: MENELAUS:2

    

     Th2: ((lambda * A) `1 ) = (lambda * (A `1 )) & ((lambda * A) `2 ) = (lambda * (A `2 ))

    proof

      (lambda * A) = |[(lambda * (A `1 )), (lambda * (A `2 ))]| by EUCLID: 57;

      hence thesis by EUCLID: 52;

    end;

    theorem :: MENELAUS:3

    

     Th3: (( - A) `1 ) = ( - (A `1 )) & (( - A) `2 ) = ( - (A `2 ))

    proof

      ( - A) = |[( - (A `1 )), ( - (A `2 ))]| by EUCLID: 59;

      hence thesis by EUCLID: 52;

    end;

    theorem :: MENELAUS:4

    

     Th4: (((lambda * A) + (mu * B)) `1 ) = ((lambda * (A `1 )) + (mu * (B `1 ))) & (((lambda * A) + (mu * B)) `2 ) = ((lambda * (A `2 )) + (mu * (B `2 )))

    proof

      (((lambda * A) + (mu * B)) `1 ) = (((lambda * A) `1 ) + ((mu * B) `1 )) by Th1

      .= ((lambda * (A `1 )) + ((mu * B) `1 )) by Th2;

      hence (((lambda * A) + (mu * B)) `1 ) = ((lambda * (A `1 )) + (mu * (B `1 ))) by Th2;

      (((lambda * A) + (mu * B)) `2 ) = (((lambda * A) `2 ) + ((mu * B) `2 )) by Th1

      .= ((lambda * (A `2 )) + ((mu * B) `2 )) by Th2;

      hence thesis by Th2;

    end;

    theorem :: MENELAUS:5

    ((( - lambda) * A) `1 ) = ( - (lambda * (A `1 ))) & ((( - lambda) * A) `2 ) = ( - (lambda * (A `2 )))

    proof

      ((( - lambda) * A) `1 ) = (( - (lambda * A)) `1 ) by RLVECT_1: 79

      .= ( - ((lambda * A) `1 )) by Th3;

      hence ((( - lambda) * A) `1 ) = ( - (lambda * (A `1 ))) by Th2;

      ((( - lambda) * A) `2 ) = (( - (lambda * A)) `2 ) by RLVECT_1: 79

      .= ( - ((lambda * A) `2 )) by Th3;

      hence thesis by Th2;

    end;

    theorem :: MENELAUS:6

    (((lambda * A) - (mu * B)) `1 ) = ((lambda * (A `1 )) - (mu * (B `1 ))) & (((lambda * A) - (mu * B)) `2 ) = ((lambda * (A `2 )) - (mu * (B `2 )))

    proof

      (((lambda * A) - (mu * B)) `1 ) = (((lambda * A) `1 ) - ((mu * B) `1 )) by EUCLID_6: 41

      .= ((lambda * (A `1 )) - ((mu * B) `1 )) by Th2;

      hence (((lambda * A) - (mu * B)) `1 ) = ((lambda * (A `1 )) - (mu * (B `1 ))) by Th2;

      (((lambda * A) - (mu * B)) `2 ) = (((lambda * A) `2 ) - ((mu * B) `2 )) by EUCLID_6: 41

      .= ((lambda * (A `2 )) - ((mu * B) `2 )) by Th2;

      hence thesis by Th2;

    end;

    theorem :: MENELAUS:7

    

     Th7: ( the_area_of_polygon3 ((((1 - lambda) * A) + (lambda * A1)),B,C)) = (((1 - lambda) * ( the_area_of_polygon3 (A,B,C))) + (lambda * ( the_area_of_polygon3 (A1,B,C))))

    proof

      ( the_area_of_polygon3 ((((1 - lambda) * A) + (lambda * A1)),B,C)) = ((((((((1 - lambda) * (A `1 )) + (lambda * (A1 `1 ))) * (B `2 )) - ((B `1 ) * ((((1 - lambda) * A) + (lambda * A1)) `2 ))) + (((B `1 ) * (C `2 )) - ((C `1 ) * (B `2 )))) + (((C `1 ) * ((((1 - lambda) * A) + (lambda * A1)) `2 )) - (((((1 - lambda) * A) + (lambda * A1)) `1 ) * (C `2 )))) / 2) by Th4

      .= ((((((((1 - lambda) * (A `1 )) + (lambda * (A1 `1 ))) * (B `2 )) - ((B `1 ) * (((1 - lambda) * (A `2 )) + (lambda * (A1 `2 ))))) + (((B `1 ) * (C `2 )) - ((C `1 ) * (B `2 )))) + (((C `1 ) * ((((1 - lambda) * A) + (lambda * A1)) `2 )) - (((((1 - lambda) * A) + (lambda * A1)) `1 ) * (C `2 )))) / 2) by Th4

      .= ((((((((1 - lambda) * (A `1 )) + (lambda * (A1 `1 ))) * (B `2 )) - ((B `1 ) * (((1 - lambda) * (A `2 )) + (lambda * (A1 `2 ))))) + (((B `1 ) * (C `2 )) - ((C `1 ) * (B `2 )))) + (((C `1 ) * (((1 - lambda) * (A `2 )) + (lambda * (A1 `2 )))) - (((((1 - lambda) * A) + (lambda * A1)) `1 ) * (C `2 )))) / 2) by Th4

      .= ((((((((1 - lambda) * (A `1 )) + (lambda * (A1 `1 ))) * (B `2 )) - ((B `1 ) * (((1 - lambda) * (A `2 )) + (lambda * (A1 `2 ))))) + (((B `1 ) * (C `2 )) - ((C `1 ) * (B `2 )))) + (((C `1 ) * (((1 - lambda) * (A `2 )) + (lambda * (A1 `2 )))) - ((((1 - lambda) * (A `1 )) + (lambda * (A1 `1 ))) * (C `2 )))) / 2) by Th4;

      hence thesis;

    end;

    theorem :: MENELAUS:8

    

     Th8: (( angle (A,B,C)) = 0 & (A,B,C) are_mutually_distinct ) implies (( angle (B,C,A)) = PI or ( angle (B,A,C)) = PI )

    proof

      set z1 = ( euc2cpx A);

      set z2 = ( euc2cpx B);

      set z3 = ( euc2cpx C);

      assume that

       A1: ( angle (A,B,C)) = 0 and

       A2: (A,B,C) are_mutually_distinct ;

      A <> B & A <> C & B <> C by A2, ZFMISC_1:def 5;

      then

       A3: z1 <> z2 & z1 <> z3 & z2 <> z3 by EUCLID_3: 4;

      per cases ;

        suppose ( angle (z2,z3,z1)) = 0 & ( angle (z3,z1,z2)) = PI ;

        hence thesis by COMPLEX2: 82;

      end;

        suppose not (( angle (z2,z3,z1)) = 0 & ( angle (z3,z1,z2)) = PI );

        hence thesis by A3, A1, COMPLEX2: 87;

      end;

    end;

    theorem :: MENELAUS:9

    

     Th9: (A,B,C) are_collinear iff ( the_area_of_polygon3 (A,B,C)) = 0

    proof

      hereby

        assume (A,B,C) are_collinear ;

        per cases by TOPREAL9: 67;

          suppose A in ( LSeg (B,C));

          then

          consider lambda such that

           A1: A = (((1 - lambda) * B) + (lambda * C)) & 0 <= lambda & lambda <= 1;

          ( the_area_of_polygon3 (A,B,C)) = (((1 - lambda) * ( the_area_of_polygon3 (B,B,C))) + (lambda * ( the_area_of_polygon3 (C,B,C)))) by Th7, A1;

          hence ( the_area_of_polygon3 (A,B,C)) = 0 ;

        end;

          suppose B in ( LSeg (C,A));

          then

          consider lambda such that

           A2: B = (((1 - lambda) * C) + (lambda * A)) & 0 <= lambda & lambda <= 1;

          ( the_area_of_polygon3 (A,B,C)) = ( - ( the_area_of_polygon3 ((((1 - lambda) * C) + (lambda * A)),A,C))) by A2

          .= (( - ((1 - lambda) * ( the_area_of_polygon3 (C,A,C)))) - (lambda * ( the_area_of_polygon3 (A,A,C)))) by Th7;

          hence ( the_area_of_polygon3 (A,B,C)) = 0 ;

        end;

          suppose C in ( LSeg (A,B));

          then

          consider lambda such that

           A3: C = (((1 - lambda) * A) + (lambda * B)) & 0 <= lambda & lambda <= 1;

          ( the_area_of_polygon3 (A,B,C)) = ( - ( the_area_of_polygon3 ((((1 - lambda) * A) + (lambda * B)),B,A))) by A3

          .= (( - ((1 - lambda) * ( the_area_of_polygon3 (A,B,A)))) - (lambda * ( the_area_of_polygon3 (B,B,A)))) by Th7;

          hence ( the_area_of_polygon3 (A,B,C)) = 0 ;

        end;

      end;

      assume ( the_area_of_polygon3 (A,B,C)) = 0 ;

      then ((( |.(A - B).| * |.(C - B).|) * ( sin ( angle (C,B,A)))) / 2) = 0 by EUCLID_6: 5;

      per cases ;

        suppose |.(A - B).| = 0 ;

        then A = B by EUCLID_6: 42;

        then not (A,B,C) are_mutually_distinct by ZFMISC_1:def 5;

        hence (A,B,C) are_collinear by EUCLID_6: 20;

      end;

        suppose |.(C - B).| = 0 ;

        then C = B by EUCLID_6: 42;

        then not (A,B,C) are_mutually_distinct by ZFMISC_1:def 5;

        hence (A,B,C) are_collinear by EUCLID_6: 20;

      end;

        suppose

         A4: ( sin ( angle (C,B,A))) = 0 ;

        ((2 * PI ) * 0 ) <= ( angle (C,B,A)) & ( angle (C,B,A)) < ((2 * PI ) + ((2 * PI ) * 0 )) by COMPLEX2: 70;

        then ( angle (C,B,A)) = ((2 * PI ) * 0 ) or ( angle (C,B,A)) = ( PI + ((2 * PI ) * 0 )) by A4, SIN_COS6: 21;

        per cases ;

          suppose ( angle (C,B,A)) = 0 ;

          then ( angle (B,C,A)) = PI or ( angle (B,A,C)) = PI or not (C,B,A) are_mutually_distinct by Th8;

          then C in ( LSeg (B,A)) or A in ( LSeg (B,C)) or not (C <> B & C <> A & B <> A) by EUCLID_6: 11, ZFMISC_1:def 5;

          then C in ( LSeg (B,A)) or A in ( LSeg (B,C)) or not (A,B,C) are_mutually_distinct by ZFMISC_1:def 5;

          hence thesis by EUCLID_6: 20, TOPREAL9: 67;

        end;

          suppose ( angle (C,B,A)) = PI ;

          then B in ( LSeg (C,A)) by EUCLID_6: 11;

          hence thesis by TOPREAL9: 67;

        end;

      end;

    end;

    theorem :: MENELAUS:10

    

     Th10: ( the_area_of_polygon3 (( 0. ( TOP-REAL 2)),B,C)) = ((((B `1 ) * (C `2 )) - ((C `1 ) * (B `2 ))) / 2)

    proof

      ( the_area_of_polygon3 (( 0. ( TOP-REAL 2)),B,C)) = ((((( 0 * (B `2 )) - ((B `1 ) * ( |[ 0 , 0 ]| `2 ))) + (((B `1 ) * (C `2 )) - ((C `1 ) * (B `2 )))) + (((C `1 ) * ( |[ 0 , 0 ]| `2 )) - (( |[ 0 , 0 ]| `1 ) * (C `2 )))) / 2) by EUCLID: 52, EUCLID: 54

      .= (((( 0 - ((B `1 ) * 0 )) + (((B `1 ) * (C `2 )) - ((C `1 ) * (B `2 )))) + (((C `1 ) * ( |[ 0 , 0 ]| `2 )) - (( |[ 0 , 0 ]| `1 ) * (C `2 )))) / 2) by EUCLID: 52

      .= (((((B `1 ) * (C `2 )) - ((C `1 ) * (B `2 ))) + (((C `1 ) * 0 ) - (( |[ 0 , 0 ]| `1 ) * (C `2 )))) / 2) by EUCLID: 52

      .= (((((B `1 ) * (C `2 )) - ((C `1 ) * (B `2 ))) + ( 0 - ( 0 * (C `2 )))) / 2) by EUCLID: 52;

      hence thesis;

    end;

    theorem :: MENELAUS:11

    ( the_area_of_polygon3 ((A + A1),B,C)) = ((( the_area_of_polygon3 (A,B,C)) + ( the_area_of_polygon3 (A1,B,C))) - ( the_area_of_polygon3 (( 0. ( TOP-REAL 2)),B,C)))

    proof

      ( the_area_of_polygon3 ((A + A1),B,C)) = (((((((A `1 ) + (A1 `1 )) * (B `2 )) - ((B `1 ) * ((A + A1) `2 ))) + (((B `1 ) * (C `2 )) - ((C `1 ) * (B `2 )))) + (((C `1 ) * ((A + A1) `2 )) - (((A + A1) `1 ) * (C `2 )))) / 2) by Th1

      .= (((((((A `1 ) + (A1 `1 )) * (B `2 )) - ((B `1 ) * ((A `2 ) + (A1 `2 )))) + (((B `1 ) * (C `2 )) - ((C `1 ) * (B `2 )))) + (((C `1 ) * ((A + A1) `2 )) - (((A + A1) `1 ) * (C `2 )))) / 2) by Th1

      .= (((((((A `1 ) + (A1 `1 )) * (B `2 )) - ((B `1 ) * ((A `2 ) + (A1 `2 )))) + (((B `1 ) * (C `2 )) - ((C `1 ) * (B `2 )))) + (((C `1 ) * ((A `2 ) + (A1 `2 ))) - (((A + A1) `1 ) * (C `2 )))) / 2) by Th1

      .= (((((((A `1 ) + (A1 `1 )) * (B `2 )) - ((B `1 ) * ((A `2 ) + (A1 `2 )))) + (((B `1 ) * (C `2 )) - ((C `1 ) * (B `2 )))) + (((C `1 ) * ((A `2 ) + (A1 `2 ))) - (((A `1 ) + (A1 `1 )) * (C `2 )))) / 2) by Th1

      .= ((((((((A `1 ) + (A1 `1 )) * (B `2 )) - ((B `1 ) * ((A `2 ) + (A1 `2 )))) + (2 * (((B `1 ) * (C `2 )) - ((C `1 ) * (B `2 ))))) + (((C `1 ) * ((A `2 ) + (A1 `2 ))) - (((A `1 ) + (A1 `1 )) * (C `2 )))) / 2) - ((((B `1 ) * (C `2 )) - ((C `1 ) * (B `2 ))) / 2));

      hence thesis by Th10;

    end;

    theorem :: MENELAUS:12

    

     Th12: A in ( LSeg (B,C)) implies A in ( Line (B,C))

    proof

      assume A in ( LSeg (B,C));

      then

      consider lambda such that

       A1: A = (((1 - lambda) * B) + (lambda * C)) & 0 <= lambda & lambda <= 1;

      thus thesis by A1;

    end;

    theorem :: MENELAUS:13

    

     Th13: B <> C implies ((A,B,C) are_collinear iff A in ( Line (B,C)))

    proof

      assume

       A1: B <> C;

      hereby

        assume (A,B,C) are_collinear ;

        per cases by TOPREAL9: 67;

          suppose A in ( LSeg (B,C));

          hence A in ( Line (B,C)) by Th12;

        end;

          suppose B in ( LSeg (C,A));

          then

           A2: B in ( Line (C,A)) by Th12;

          

           A3: C in ( Line (C,A)) & A in ( Line (C,A)) by EUCLID_4: 41;

          then ( Line (C,A)) c= ( Line (B,C)) by A2, A1, EUCLID_4: 43;

          hence A in ( Line (B,C)) by A3;

        end;

          suppose C in ( LSeg (A,B));

          then

           A4: C in ( Line (A,B)) by Th12;

          

           A5: A in ( Line (A,B)) & B in ( Line (A,B)) by EUCLID_4: 41;

          then ( Line (A,B)) c= ( Line (B,C)) by A4, A1, EUCLID_4: 43;

          hence A in ( Line (B,C)) by A5;

        end;

      end;

      assume A in ( Line (B,C));

      then

      consider lambda such that

       A6: A = (((1 - lambda) * B) + (lambda * C));

      ( the_area_of_polygon3 (A,B,C)) = (((1 - lambda) * ( the_area_of_polygon3 (B,B,C))) + (lambda * ( the_area_of_polygon3 (C,B,C)))) by Th7, A6;

      hence thesis by Th9;

    end;

    

     Lm1: (A1 = (((1 - lambda) * B) + (lambda * C)) & B1 = (((1 - mu) * C) + (mu * A)) & C2 = (((1 - alpha) * A) + (alpha * A1))) implies ( the_area_of_polygon3 (B,B1,C2)) = (((1 - mu) - (alpha * ((1 - mu) + (lambda * mu)))) * ( the_area_of_polygon3 (A,B,C)))

    proof

      assume that

       A1: A1 = (((1 - lambda) * B) + (lambda * C)) and

       A2: B1 = (((1 - mu) * C) + (mu * A)) and

       A3: C2 = (((1 - alpha) * A) + (alpha * A1));

      ( the_area_of_polygon3 (B,B1,C2)) = ( the_area_of_polygon3 ((((1 - alpha) * A) + (alpha * A1)),B,B1)) by A3

      .= (((1 - alpha) * ( the_area_of_polygon3 (A,B,B1))) + (alpha * ( the_area_of_polygon3 (A1,B,B1)))) by Th7

      .= (((1 - alpha) * ( the_area_of_polygon3 (B1,A,B))) + (alpha * (((1 - lambda) * ( the_area_of_polygon3 (B,B,B1))) + (lambda * ( the_area_of_polygon3 (C,B,B1)))))) by Th7, A1

      .= (((1 - alpha) * (((1 - mu) * ( the_area_of_polygon3 (C,A,B))) + (mu * ( the_area_of_polygon3 (A,A,B))))) + ((alpha * lambda) * ( the_area_of_polygon3 (B1,C,B)))) by Th7, A2

      .= ((((1 - alpha) * (1 - mu)) * ( the_area_of_polygon3 (C,A,B))) + ((alpha * lambda) * (((1 - mu) * ( the_area_of_polygon3 (C,C,B))) + (mu * ( the_area_of_polygon3 (A,C,B)))))) by Th7, A2

      .= ((((1 - alpha) * (1 - mu)) * ( the_area_of_polygon3 (A,B,C))) - (((alpha * lambda) * mu) * ( the_area_of_polygon3 (A,B,C))));

      hence thesis;

    end;

    theorem :: MENELAUS:14

    

     Th14: (A,B,C) is_a_triangle & A1 = (((1 - lambda) * B) + (lambda * C)) implies A <> A1

    proof

      assume that

       A1: (A,B,C) is_a_triangle and

       A2: A1 = (((1 - lambda) * B) + (lambda * C));

      (A,B,C) are_mutually_distinct by A1, EUCLID_6: 20;

      then

       A3: A <> B & A <> C & B <> C by ZFMISC_1:def 5;

      hereby

        assume A = A1;

        then A in ( Line (B,C)) by A2;

        hence contradiction by A3, Th13, A1;

      end;

    end;

    theorem :: MENELAUS:15

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

    

     Lm2: ((A,B,C) is_a_triangle & A1 = (((1 - lambda) * B) + (lambda * C)) & B1 = (((1 - mu) * C) + (mu * A)) & mu <> 1 & (A,A1,C2) are_collinear & (B,B1,C2) are_collinear ) implies ((1 - mu) + (lambda * mu)) <> 0 & (ex alpha st (C2 = (((1 - alpha) * A) + (alpha * A1)) & alpha = ((1 - mu) / ((1 - mu) + (lambda * mu)))))

    proof

      assume that

       A1: (A,B,C) is_a_triangle and

       A2: A1 = (((1 - lambda) * B) + (lambda * C)) and

       A3: B1 = (((1 - mu) * C) + (mu * A)) and

       A4: mu <> 1 and

       A5: (A,A1,C2) are_collinear and

       A6: (B,B1,C2) are_collinear ;

      

       A7: A <> A1 by Th14, A1, A2;

      

       A8: ( the_area_of_polygon3 (A,B,C)) <> 0 by A1, Th9;

      (C2,A,A1) are_collinear by A5;

      then C2 in ( Line (A,A1)) by A7, Th13;

      then

      consider alpha such that

       A9: C2 = (((1 - alpha) * A) + (alpha * A1));

       0 = ( the_area_of_polygon3 (B,B1,C2)) by A6, Th9

      .= (((1 - mu) - (((1 - mu) + (lambda * mu)) * alpha)) * ( the_area_of_polygon3 (A,B,C))) by Lm1, A9, A2, A3;

      then

       A10: ((1 - mu) - (((1 - mu) + (lambda * mu)) * alpha)) = 0 & (1 - mu) <> 0 by A8, A4;

      then ((1 - mu) + (lambda * mu)) <> 0 ;

      hence thesis by A9, A10, XCMPLX_1: 89;

    end;

    

     Lm3: ((A,B,C) is_a_triangle & A1 = (((1 - lambda) * B) + (lambda * C)) & B1 = (((1 - mu) * C) + (mu * A)) & ((1 - mu) + (lambda * mu)) <> 0 ) implies (ex C2 st (A,A1,C2) are_collinear & (B,B1,C2) are_collinear )

    proof

      assume that

       A1: (A,B,C) is_a_triangle and

       A2: A1 = (((1 - lambda) * B) + (lambda * C)) and

       A3: B1 = (((1 - mu) * C) + (mu * A)) and

       A4: ((1 - mu) + (lambda * mu)) <> 0 ;

      

       A5: A <> A1 by Th14, A1, A2;

      consider alpha such that

       A6: alpha = ((1 - mu) / ((1 - mu) + (lambda * mu)));

      consider C2 such that

       A7: C2 = (((1 - alpha) * A) + (alpha * A1));

      take C2;

      C2 in ( Line (A,A1)) by A7;

      then (C2,A,A1) are_collinear by A5, Th13;

      hence (A,A1,C2) are_collinear ;

      ( the_area_of_polygon3 (B,B1,C2)) = (((1 - mu) - (((1 - mu) / ((1 - mu) + (lambda * mu))) * ((1 - mu) + (lambda * mu)))) * ( the_area_of_polygon3 (A,B,C))) by A6, Lm1, A2, A3, A7

      .= (((1 - mu) - (1 - mu)) * ( the_area_of_polygon3 (A,B,C))) by A4, XCMPLX_1: 87;

      hence (B,B1,C2) are_collinear by Th9;

    end;

    

     Lm4: (lambda <> 1 & mu <> 1 & nu <> 1) implies ( 0 = (((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu))) iff (((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu))) = 1)

    proof

      set q = (((1 - lambda) * (1 - mu)) * (1 - nu));

      assume lambda <> 1 & mu <> 1 & nu <> 1;

      then

       A1: (1 - lambda) <> 0 & (1 - mu) <> 0 & (1 - nu) <> 0 ;

       0 = (((lambda * mu) * nu) - q) iff 0 = ((q * 1) + ( - ((mu * nu) * lambda)));

      then 0 = (((lambda * mu) * nu) - q) iff (q * (1 + (( - ((lambda * mu) * nu)) / q))) = 0 by A1, XCMPLX_1: 235;

      then 0 = (((lambda * mu) * nu) - q) iff (1 + (( - ((lambda * mu) * nu)) / q)) = 0 by A1;

      then 0 = (((lambda * mu) * nu) - q) iff (1 + ( - (((lambda * mu) * nu) / q))) = 0 by XCMPLX_1: 187;

      then 0 = (((lambda * mu) * nu) - q) iff 1 = ((lambda * (mu * nu)) / ((1 - lambda) * ((1 - mu) * (1 - nu))));

      then 0 = (((lambda * mu) * nu) - q) iff 1 = (((lambda / (1 - lambda)) * (mu * nu)) / ((1 - mu) * (1 - nu))) by XCMPLX_1: 83;

      then 0 = (((lambda * mu) * nu) - q) iff 1 = ((lambda / (1 - lambda)) * ((mu * nu) / ((1 - mu) * (1 - nu)))) by XCMPLX_1: 74;

      then 0 = (((lambda * mu) * nu) - q) iff 1 = ((lambda / (1 - lambda)) * (((mu / (1 - mu)) * nu) / (1 - nu))) by XCMPLX_1: 83;

      then 0 = (((lambda * mu) * nu) - q) iff 1 = ((lambda / (1 - lambda)) * ((mu / (1 - mu)) * (nu / (1 - nu)))) by XCMPLX_1: 74;

      hence thesis;

    end;

    

     Lm5: (mu <> 1 & 0 = (((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)))) implies (((1 - mu) + (mu * lambda)) = 0 implies ((1 - lambda) + (lambda * nu)) = 0 )

    proof

      assume that

       A1: mu <> 1 and

       A2: 0 = (((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu))) and

       A3: ((1 - mu) + (mu * lambda)) = 0 ;

      

       A4: (1 - mu) <> 0 by A1;

       0 = ((( - (1 - mu)) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu))) by A2, A3;

      then 0 = ((1 - mu) * (nu + ((1 - lambda) * (1 - nu))));

      hence thesis by A4;

    end;

    theorem :: MENELAUS:16

    

     Th16: ((A,B,C) is_a_triangle & A1 = (((1 - lambda) * B) + (lambda * C)) & B1 = (((1 - mu) * C) + (mu * A)) & mu <> 1) implies (((1 - mu) + (lambda * mu)) <> 0 iff not ( Line (A,A1)) is_parallel_to ( Line (B,B1)))

    proof

      assume that

       A1: (A,B,C) is_a_triangle and

       A2: A1 = (((1 - lambda) * B) + (lambda * C)) and

       A3: B1 = (((1 - mu) * C) + (mu * A)) and

       A4: mu <> 1;

      

       A5: A <> A1 by A1, A2, Th14;

      (B,C,A) is_a_triangle by A1;

      then

       A6: B <> B1 by A3, Th14;

      hereby

        assume ((1 - mu) + (lambda * mu)) <> 0 ;

        then

        consider C2 such that

         A7: (A,A1,C2) are_collinear & (B,B1,C2) are_collinear by Lm3, A1, A2, A3;

        (C2,A,A1) are_collinear & (C2,B,B1) are_collinear by A7;

        then C2 in ( Line (A,A1)) & C2 in ( Line (B,B1)) by A5, A6, Th13;

        hence not ( Line (A,A1)) is_parallel_to ( Line (B,B1)) by XBOOLE_0: 3;

      end;

      assume not ( Line (A,A1)) is_parallel_to ( Line (B,B1));

      then

      consider C2 be object such that

       A8: C2 in ( Line (A,A1)) & C2 in ( Line (B,B1)) by XBOOLE_0: 3;

      reconsider C2 as Point of ( TOP-REAL 2) by A8;

      (C2,A,A1) are_collinear & (C2,B,B1) are_collinear by A8, A5, A6, Th13;

      then (A,A1,C2) are_collinear & (B,B1,C2) are_collinear ;

      hence thesis by Lm2, A1, A2, A3, A4;

    end;

    

     Lm6: ((A,B,C) is_a_triangle & A1 = (((1 - lambda) * B) + (lambda * C)) & B1 = (((1 - mu) * C) + (mu * A)) & C1 = (((1 - nu) * A) + (nu * B)) & lambda <> 1 & mu <> 1 & nu <> 1 & not (((1 - mu) + (lambda * mu)) <> 0 & ((1 - lambda) + (nu * lambda)) <> 0 & ((1 - nu) + (mu * nu)) <> 0 )) implies ((((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu))) = 1 iff (( Line (A,A1)) is_parallel_to ( Line (B,B1)) & ( Line (B,B1)) is_parallel_to ( Line (C,C1)) & ( Line (C,C1)) is_parallel_to ( Line (A,A1))))

    proof

      assume that

       A1: (A,B,C) is_a_triangle and

       A2: A1 = (((1 - lambda) * B) + (lambda * C)) and

       A3: B1 = (((1 - mu) * C) + (mu * A)) and

       A4: C1 = (((1 - nu) * A) + (nu * B)) and

       A5: lambda <> 1 and

       A6: mu <> 1 and

       A7: nu <> 1 and

       A8: not (((1 - mu) + (lambda * mu)) <> 0 & ((1 - lambda) + (nu * lambda)) <> 0 & ((1 - nu) + (mu * nu)) <> 0 );

      

       A9: (B,C,A) is_a_triangle by A1;

      

       A10: (C,A,B) is_a_triangle by A1;

      hereby

        assume (((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu))) = 1;

        then

         A11: 0 = (((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu))) by Lm4, A5, A6, A7;

        then

         A12: 0 = (((nu * lambda) * mu) - (((1 - nu) * (1 - lambda)) * (1 - mu)));

        

         A13: 0 = (((mu * nu) * lambda) - (((1 - mu) * (1 - nu)) * (1 - lambda))) by A11;

        ((1 - mu) + (lambda * mu)) = 0 & ((1 - nu) + (mu * nu)) = 0 & ((1 - lambda) + (nu * lambda)) = 0

        proof

          per cases by A8;

            suppose

             A14: ((1 - mu) + (lambda * mu)) = 0 ;

            then ((1 - lambda) + (nu * lambda)) = 0 by Lm5, A6, A11;

            hence thesis by Lm5, A5, A12, A14;

          end;

            suppose

             A15: ((1 - lambda) + (nu * lambda)) = 0 ;

            then ((1 - nu) + (nu * mu)) = 0 by Lm5, A5, A12;

            hence thesis by Lm5, A7, A13, A15;

          end;

            suppose

             A16: ((1 - nu) + (mu * nu)) = 0 ;

            then ((1 - mu) + (lambda * mu)) = 0 by Lm5, A7, A13;

            hence thesis by Lm5, A6, A11, A16;

          end;

        end;

        hence ( Line (A,A1)) is_parallel_to ( Line (B,B1)) & ( Line (B,B1)) is_parallel_to ( Line (C,C1)) & ( Line (C,C1)) is_parallel_to ( Line (A,A1)) by A1, A9, Th16, A2, A3, A4, A5, A6, A7, A10;

      end;

      assume ( Line (A,A1)) is_parallel_to ( Line (B,B1)) & ( Line (B,B1)) is_parallel_to ( Line (C,C1));

      then

       A17: ((1 - mu) + (lambda * mu)) = 0 & ((1 - nu) + (mu * nu)) = 0 by A1, A9, Th16, A2, A3, A4, A6, A7;

      

      then (((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu))) = (((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * ( - (mu * nu))))

      .= (((lambda + ((1 - lambda) * (1 - mu))) * mu) * nu)

      .= 0 by A17;

      hence thesis by Lm4, A5, A6, A7;

    end;

    begin

    ::$Notion-Name

    theorem :: MENELAUS:17

    

     Th17: (A1 = (((1 - lambda) * B) + (lambda * C)) & B1 = (((1 - mu) * C) + (mu * A)) & C1 = (((1 - nu) * A) + (nu * B))) implies ( the_area_of_polygon3 (A1,B1,C1)) = (((((1 - lambda) * (1 - mu)) * (1 - nu)) + ((lambda * mu) * nu)) * ( the_area_of_polygon3 (A,B,C)))

    proof

      assume that

       A1: A1 = (((1 - lambda) * B) + (lambda * C)) and

       A2: B1 = (((1 - mu) * C) + (mu * A)) and

       A3: C1 = (((1 - nu) * A) + (nu * B));

      ( the_area_of_polygon3 (A1,B1,C1)) = (((1 - lambda) * ( the_area_of_polygon3 (B,B1,C1))) + (lambda * ( the_area_of_polygon3 (C,B1,C1)))) by Th7, A1

      .= (( - ((1 - lambda) * ( the_area_of_polygon3 ((((1 - mu) * C) + (mu * A)),B,C1)))) - (lambda * ( the_area_of_polygon3 ((((1 - mu) * C) + (mu * A)),C,C1)))) by A2

      .= (( - ((1 - lambda) * (((1 - mu) * ( the_area_of_polygon3 (C,B,C1))) + (mu * ( the_area_of_polygon3 (A,B,C1)))))) - (lambda * ( the_area_of_polygon3 ((((1 - mu) * C) + (mu * A)),C,C1)))) by Th7

      .= (( - ((1 - lambda) * (((1 - mu) * ( the_area_of_polygon3 (C,B,C1))) + (mu * ( the_area_of_polygon3 (A,B,C1)))))) - (lambda * (((1 - mu) * ( the_area_of_polygon3 (C,C,C1))) + (mu * ( the_area_of_polygon3 (A,C,C1)))))) by Th7

      .= (((((1 - lambda) * (1 - mu)) * ( the_area_of_polygon3 ((((1 - nu) * A) + (nu * B)),B,C))) + (((1 - lambda) * mu) * ( the_area_of_polygon3 ((((1 - nu) * A) + (nu * B)),B,A)))) + ((lambda * mu) * ( the_area_of_polygon3 ((((1 - nu) * A) + (nu * B)),C,A)))) by A3

      .= (((((1 - lambda) * (1 - mu)) * (((1 - nu) * ( the_area_of_polygon3 (A,B,C))) + (nu * ( the_area_of_polygon3 (B,B,C))))) + (((1 - lambda) * mu) * ( the_area_of_polygon3 ((((1 - nu) * A) + (nu * B)),B,A)))) + ((lambda * mu) * ( the_area_of_polygon3 ((((1 - nu) * A) + (nu * B)),C,A)))) by Th7

      .= ((((((1 - lambda) * (1 - mu)) * (1 - nu)) * ( the_area_of_polygon3 (A,B,C))) + (((1 - lambda) * mu) * (((1 - nu) * ( the_area_of_polygon3 (A,B,A))) + (nu * ( the_area_of_polygon3 (B,B,A)))))) + ((lambda * mu) * ( the_area_of_polygon3 ((((1 - nu) * A) + (nu * B)),C,A)))) by Th7

      .= (((((1 - lambda) * (1 - mu)) * (1 - nu)) * ( the_area_of_polygon3 (A,B,C))) + ((lambda * mu) * (((1 - nu) * ( the_area_of_polygon3 (A,C,A))) + (nu * ( the_area_of_polygon3 (B,C,A)))))) by Th7;

      hence thesis;

    end;

    ::$Notion-Name

    theorem :: MENELAUS:18

    ((A,B,C) is_a_triangle & A1 = (((1 - lambda) * B) + (lambda * C)) & B1 = (((1 - mu) * C) + (mu * A)) & C1 = (((1 - nu) * A) + (nu * B)) & lambda <> 1 & mu <> 1 & nu <> 1) implies ((A1,B1,C1) are_collinear iff (((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu))) = ( - 1))

    proof

      assume that

       A1: (A,B,C) is_a_triangle and

       A2: A1 = (((1 - lambda) * B) + (lambda * C)) and

       A3: B1 = (((1 - mu) * C) + (mu * A)) and

       A4: C1 = (((1 - nu) * A) + (nu * B)) and

       A5: lambda <> 1 & mu <> 1 & nu <> 1;

      

       A6: ( the_area_of_polygon3 (A,B,C)) <> 0 by Th9, A1;

      set q = (((1 - lambda) * (1 - mu)) * (1 - nu));

      

       A7: (1 - lambda) <> 0 & (1 - mu) <> 0 & (1 - nu) <> 0 by A5;

      (A1,B1,C1) are_collinear iff ( the_area_of_polygon3 (A1,B1,C1)) = 0 by Th9;

      then (A1,B1,C1) are_collinear iff ((q + ((lambda * mu) * nu)) * ( the_area_of_polygon3 (A,B,C))) = 0 by Th17, A2, A3, A4;

      then (A1,B1,C1) are_collinear iff ((1 * q) + ((lambda * mu) * nu)) = 0 by A6;

      then (A1,B1,C1) are_collinear iff (q * (1 + (((lambda * mu) * nu) / q))) = 0 by A7, XCMPLX_1: 235;

      then (A1,B1,C1) are_collinear iff (1 + (((lambda * mu) * nu) / q)) = 0 by A7;

      then (A1,B1,C1) are_collinear iff ( - 1) = ((lambda * (mu * nu)) / ((1 - lambda) * ((1 - mu) * (1 - nu))));

      then (A1,B1,C1) are_collinear iff ( - 1) = (((lambda / (1 - lambda)) * (mu * nu)) / ((1 - mu) * (1 - nu))) by XCMPLX_1: 83;

      then (A1,B1,C1) are_collinear iff ( - 1) = ((lambda / (1 - lambda)) * ((mu * nu) / ((1 - mu) * (1 - nu)))) by XCMPLX_1: 74;

      then (A1,B1,C1) are_collinear iff ( - 1) = ((lambda / (1 - lambda)) * (((mu / (1 - mu)) * nu) / (1 - nu))) by XCMPLX_1: 83;

      then (A1,B1,C1) are_collinear iff ( - 1) = ((lambda / (1 - lambda)) * ((mu / (1 - mu)) * (nu / (1 - nu)))) by XCMPLX_1: 74;

      hence thesis;

    end;

    ::$Notion-Name

    theorem :: MENELAUS:19

    

     Th19: ((A,B,C) is_a_triangle & A1 = (((1 - lambda) * B) + (lambda * C)) & B1 = (((1 - mu) * C) + (mu * A)) & C1 = (((1 - nu) * A) + (nu * B)) & lambda <> 1 & mu <> 1 & nu <> 1 & (A,A1,B2,C2) are_collinear & (B,B1,A2,C2) are_collinear & (C,C1,A2,B2) are_collinear ) implies ((((1 - mu) + (lambda * mu)) * ((1 - lambda) + (nu * lambda))) * ((1 - nu) + (mu * nu))) <> 0 & ( the_area_of_polygon3 (A2,B2,C2)) = ((((((mu * nu) * lambda) - (((1 - mu) * (1 - nu)) * (1 - lambda))) ^2 ) / ((((1 - mu) + (lambda * mu)) * ((1 - lambda) + (nu * lambda))) * ((1 - nu) + (mu * nu)))) * ( the_area_of_polygon3 (A,B,C)))

    proof

      assume that

       A1: (A,B,C) is_a_triangle and

       A2: A1 = (((1 - lambda) * B) + (lambda * C)) and

       A3: B1 = (((1 - mu) * C) + (mu * A)) and

       A4: C1 = (((1 - nu) * A) + (nu * B)) and

       A5: lambda <> 1 and

       A6: mu <> 1 and

       A7: nu <> 1 and

       A8: (A,A1,B2,C2) are_collinear and

       A9: (B,B1,A2,C2) are_collinear and

       A10: (C,C1,A2,B2) are_collinear ;

      

       A11: (A,A1,C2) are_collinear by A8;

      

       A12: (B,B1,C2) are_collinear by A9;

      

       A13: (B,B1,A2) are_collinear by A9;

      

       A14: (C,C1,A2) are_collinear by A10;

      

       A15: (A,A1,B2) are_collinear by A8;

      

       A16: (C,C1,B2) are_collinear by A10;

      

       A17: (C,A,B) is_a_triangle by A1;

      

       A18: (B,C,A) is_a_triangle by A1;

      set q1 = ((1 - mu) + (lambda * mu));

      set q2 = ((1 - lambda) + (nu * lambda));

      set q3 = ((1 - nu) + (mu * nu));

      consider alpha such that

       A19: C2 = (((1 - alpha) * A) + (alpha * A1)) and

       A20: alpha = ((1 - mu) / q1) by Lm2, A1, A2, A3, A6, A11, A12;

      

       A21: q1 <> 0 by Lm2, A1, A2, A3, A6, A11, A12;

      consider beta such that

       A22: B2 = (((1 - beta) * C) + (beta * C1)) and

       A23: beta = ((1 - lambda) / q2) by Lm2, A17, A4, A2, A5, A16, A15;

      

       A24: q2 <> 0 by Lm2, A17, A4, A2, A5, A16, A15;

      consider gamma such that

       A25: A2 = (((1 - gamma) * B) + (gamma * B1)) and

       A26: gamma = ((1 - nu) / q3) by Lm2, A18, A3, A4, A7, A13, A14;

      

       A27: q3 <> 0 by Lm2, A18, A3, A4, A7, A13, A14;

      (1 - alpha) = (((1 * q1) - (1 - mu)) / q1) by A20, A21, XCMPLX_1: 127;

      then

       A28: (1 - alpha) = ((lambda * mu) * (1 / q1)) by XCMPLX_1: 99;

      (1 - beta) = (((1 * q2) - (1 - lambda)) / q2) by A23, A24, XCMPLX_1: 127;

      then

       A29: (1 - beta) = ((nu * lambda) * (1 / q2)) by XCMPLX_1: 99;

      (1 - gamma) = (((1 * q3) - (1 - nu)) / q3) by A26, A27, XCMPLX_1: 127;

      then

       A30: (1 - gamma) = ((mu * nu) * (1 / q3)) by XCMPLX_1: 99;

      

       A31: alpha = ((1 - mu) * (1 / q1)) by A20, XCMPLX_1: 99;

      

       A32: beta = ((1 - lambda) * (1 / q2)) by A23, XCMPLX_1: 99;

      

       A33: gamma = ((1 - nu) * (1 / q3)) by A26, XCMPLX_1: 99;

      thus ((q1 * q2) * q3) <> 0 by A21, A24, A27;

      set S = ( the_area_of_polygon3 (A,B,C));

      ( the_area_of_polygon3 (A2,B2,C2)) = (((1 - gamma) * ( the_area_of_polygon3 (B,B2,C2))) + (gamma * ( the_area_of_polygon3 ((((1 - mu) * C) + (mu * A)),B2,C2)))) by A3, Th7, A25

      .= (((1 - gamma) * ( the_area_of_polygon3 (B,B2,C2))) + (gamma * (((1 - mu) * ( the_area_of_polygon3 (C,B2,C2))) + (mu * ( the_area_of_polygon3 (A,B2,C2)))))) by Th7

      .= (( - ((1 - gamma) * ( the_area_of_polygon3 (C2,B2,B)))) - (gamma * (((1 - mu) * ( the_area_of_polygon3 ((((1 - beta) * C) + (beta * C1)),C,C2))) + (mu * ( the_area_of_polygon3 (C2,B2,A)))))) by A22

      .= (( - ((1 - gamma) * ( the_area_of_polygon3 (C2,B2,B)))) - (gamma * (((1 - mu) * (((1 - beta) * ( the_area_of_polygon3 (C,C,C2))) + (beta * ( the_area_of_polygon3 (C1,C,C2))))) + (mu * ( the_area_of_polygon3 (C2,B2,A)))))) by Th7

      .= ((( - ((1 - gamma) * ( the_area_of_polygon3 ((((1 - alpha) * A) + (alpha * A1)),B2,B)))) - (((gamma * (1 - mu)) * beta) * ( the_area_of_polygon3 (C1,C,C2)))) - ((gamma * mu) * ( the_area_of_polygon3 (C2,B2,A)))) by A19

      .= ((( - ((1 - gamma) * (((1 - alpha) * ( the_area_of_polygon3 (A,B2,B))) + (alpha * ( the_area_of_polygon3 ((((1 - lambda) * B) + (lambda * C)),B2,B)))))) - (((gamma * (1 - mu)) * beta) * ( the_area_of_polygon3 (C1,C,C2)))) - ((gamma * mu) * ( the_area_of_polygon3 (C2,B2,A)))) by A2, Th7

      .= ((( - ((1 - gamma) * (((1 - alpha) * ( the_area_of_polygon3 (A,B2,B))) + (alpha * (((1 - lambda) * ( the_area_of_polygon3 (B,B2,B))) + (lambda * ( the_area_of_polygon3 (C,B2,B)))))))) - (((gamma * (1 - mu)) * beta) * ( the_area_of_polygon3 (C1,C,C2)))) - ((gamma * mu) * ( the_area_of_polygon3 (C2,B2,A)))) by Th7

      .= ((( - ((1 - gamma) * (((1 - alpha) * ( the_area_of_polygon3 (A,B2,B))) - ((alpha * lambda) * ( the_area_of_polygon3 ((((1 - beta) * C) + (beta * C1)),C,B)))))) - (((gamma * (1 - mu)) * beta) * ( the_area_of_polygon3 (C1,C,C2)))) - ((gamma * mu) * ( the_area_of_polygon3 (C2,B2,A)))) by A22

      .= ((( - ((1 - gamma) * (((1 - alpha) * ( the_area_of_polygon3 (A,B2,B))) - ((alpha * lambda) * (((1 - beta) * ( the_area_of_polygon3 (C,C,B))) + (beta * ( the_area_of_polygon3 (C1,C,B)))))))) - (((gamma * (1 - mu)) * beta) * ( the_area_of_polygon3 (C1,C,C2)))) - ((gamma * mu) * ( the_area_of_polygon3 (C2,B2,A)))) by Th7

      .= ((( - ((1 - gamma) * (((1 - alpha) * ( the_area_of_polygon3 (A,B2,B))) - (((alpha * lambda) * beta) * ( the_area_of_polygon3 ((((1 - nu) * A) + (nu * B)),C,B)))))) - (((gamma * (1 - mu)) * beta) * ( the_area_of_polygon3 (C1,C,C2)))) - ((gamma * mu) * ( the_area_of_polygon3 (C2,B2,A)))) by A4

      .= ((( - ((1 - gamma) * (((1 - alpha) * ( the_area_of_polygon3 (A,B2,B))) - (((alpha * lambda) * beta) * (((1 - nu) * ( the_area_of_polygon3 (A,C,B))) + (nu * ( the_area_of_polygon3 (B,C,B)))))))) - (((gamma * (1 - mu)) * beta) * ( the_area_of_polygon3 (C1,C,C2)))) - ((gamma * mu) * ( the_area_of_polygon3 (C2,B2,A)))) by Th7

      .= ((((1 - gamma) * (((1 - alpha) * ( the_area_of_polygon3 ((((1 - beta) * C) + (beta * C1)),A,B))) - ((((alpha * lambda) * beta) * (1 - nu)) * S))) - (((gamma * (1 - mu)) * beta) * ( the_area_of_polygon3 (C1,C,C2)))) - ((gamma * mu) * ( the_area_of_polygon3 (C2,B2,A)))) by A22

      .= ((((1 - gamma) * (((1 - alpha) * (((1 - beta) * ( the_area_of_polygon3 (C,A,B))) + (beta * ( the_area_of_polygon3 (C1,A,B))))) - ((((alpha * lambda) * beta) * (1 - nu)) * S))) - (((gamma * (1 - mu)) * beta) * ( the_area_of_polygon3 (C1,C,C2)))) - ((gamma * mu) * ( the_area_of_polygon3 (C2,B2,A)))) by Th7

      .= ((((1 - gamma) * (((1 - alpha) * (((1 - beta) * S) + (beta * (((1 - nu) * ( the_area_of_polygon3 (A,A,B))) + (nu * ( the_area_of_polygon3 (B,A,B))))))) - ((((alpha * lambda) * beta) * (1 - nu)) * S))) - (((gamma * (1 - mu)) * beta) * ( the_area_of_polygon3 (C1,C,C2)))) - ((gamma * mu) * ( the_area_of_polygon3 (C2,B2,A)))) by Th7, A4

      .= (((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * S) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * S)) - (((gamma * (1 - mu)) * beta) * (((1 - nu) * ( the_area_of_polygon3 (A,C,C2))) + (nu * ( the_area_of_polygon3 (B,C,C2)))))) - ((gamma * mu) * ( the_area_of_polygon3 (C2,B2,A)))) by Th7, A4

      .= (((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * S) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * S)) - (((gamma * (1 - mu)) * beta) * (((1 - nu) * ( the_area_of_polygon3 ((((1 - alpha) * A) + (alpha * A1)),A,C))) + (nu * ( the_area_of_polygon3 (C2,B,C)))))) - ((gamma * mu) * ( the_area_of_polygon3 (C2,B2,A)))) by A19

      .= (((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * S) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * S)) - (((gamma * (1 - mu)) * beta) * (((1 - nu) * (((1 - alpha) * ( the_area_of_polygon3 (A,A,C))) + (alpha * ( the_area_of_polygon3 (A1,A,C))))) + (nu * ( the_area_of_polygon3 (C2,B,C)))))) - ((gamma * mu) * ( the_area_of_polygon3 (C2,B2,A)))) by Th7

      .= (((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * S) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * S)) - (((gamma * (1 - mu)) * beta) * ((((1 - nu) * alpha) * ( the_area_of_polygon3 ((((1 - lambda) * B) + (lambda * C)),A,C))) + (nu * ( the_area_of_polygon3 (C2,B,C)))))) - ((gamma * mu) * ( the_area_of_polygon3 (C2,B2,A)))) by A2

      .= (((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * S) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * S)) - (((gamma * (1 - mu)) * beta) * ((((1 - nu) * alpha) * (((1 - lambda) * ( the_area_of_polygon3 (B,A,C))) + (lambda * ( the_area_of_polygon3 (C,A,C))))) + (nu * ( the_area_of_polygon3 (C2,B,C)))))) - ((gamma * mu) * ( the_area_of_polygon3 (C2,B2,A)))) by Th7

      .= (((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * S) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * S)) - (((gamma * (1 - mu)) * beta) * (( - ((((1 - nu) * alpha) * (1 - lambda)) * S)) + (nu * (((1 - alpha) * S) + (alpha * ( the_area_of_polygon3 ((((1 - lambda) * B) + (lambda * C)),B,C)))))))) - ((gamma * mu) * ( the_area_of_polygon3 (C2,B2,A)))) by A2, Th7, A19

      .= (((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * S) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * S)) - (((gamma * (1 - mu)) * beta) * (( - ((((1 - nu) * alpha) * (1 - lambda)) * S)) + (nu * (((1 - alpha) * S) + (alpha * (((1 - lambda) * ( the_area_of_polygon3 (B,B,C))) + (lambda * ( the_area_of_polygon3 (C,B,C)))))))))) - ((gamma * mu) * ( the_area_of_polygon3 (C2,B2,A)))) by Th7

      .= (((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * S) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * S)) + (((((((gamma * (1 - mu)) * beta) * (1 - nu)) * alpha) * (1 - lambda)) * S) - (((((gamma * (1 - mu)) * beta) * nu) * (1 - alpha)) * S))) - ((gamma * mu) * (((1 - alpha) * ( the_area_of_polygon3 (A,B2,A))) + (alpha * ( the_area_of_polygon3 (A1,B2,A)))))) by Th7, A19

      .= (((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * S) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * S)) + (((((((gamma * (1 - mu)) * beta) * (1 - nu)) * alpha) * (1 - lambda)) * S) - (((((gamma * (1 - mu)) * beta) * nu) * (1 - alpha)) * S))) - (((gamma * mu) * alpha) * ( the_area_of_polygon3 ((((1 - lambda) * B) + (lambda * C)),B2,A)))) by A2

      .= (((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * S) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * S)) + (((((((gamma * (1 - mu)) * beta) * (1 - nu)) * alpha) * (1 - lambda)) * S) - (((((gamma * (1 - mu)) * beta) * nu) * (1 - alpha)) * S))) - (((gamma * mu) * alpha) * (((1 - lambda) * ( the_area_of_polygon3 (B,B2,A))) + (lambda * ( the_area_of_polygon3 (C,B2,A)))))) by Th7

      .= (((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * S) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * S)) + (((((((gamma * (1 - mu)) * beta) * (1 - nu)) * alpha) * (1 - lambda)) * S) - (((((gamma * (1 - mu)) * beta) * nu) * (1 - alpha)) * S))) - (((gamma * mu) * alpha) * (((1 - lambda) * ( the_area_of_polygon3 ((((1 - beta) * C) + (beta * C1)),A,B))) + (lambda * ( the_area_of_polygon3 (B2,A,C)))))) by A22

      .= (((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * S) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * S)) + (((((((gamma * (1 - mu)) * beta) * (1 - nu)) * alpha) * (1 - lambda)) * S) - (((((gamma * (1 - mu)) * beta) * nu) * (1 - alpha)) * S))) - (((gamma * mu) * alpha) * (((1 - lambda) * (((1 - beta) * ( the_area_of_polygon3 (C,A,B))) + (beta * ( the_area_of_polygon3 (C1,A,B))))) + (lambda * ( the_area_of_polygon3 (B2,A,C)))))) by Th7

      .= (((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * S) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * S)) + (((((((gamma * (1 - mu)) * beta) * (1 - nu)) * alpha) * (1 - lambda)) * S) - (((((gamma * (1 - mu)) * beta) * nu) * (1 - alpha)) * S))) - (((gamma * mu) * alpha) * (((1 - lambda) * (((1 - beta) * S) + (beta * (((1 - nu) * ( the_area_of_polygon3 (A,A,B))) + (nu * ( the_area_of_polygon3 (B,A,B))))))) + (lambda * ( the_area_of_polygon3 (B2,A,C)))))) by Th7, A4

      .= (((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * S) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * S)) + (((((((gamma * (1 - mu)) * beta) * (1 - nu)) * alpha) * (1 - lambda)) * S) - (((((gamma * (1 - mu)) * beta) * nu) * (1 - alpha)) * S))) - (((gamma * mu) * alpha) * ((((1 - lambda) * (1 - beta)) * S) + (lambda * (((1 - beta) * ( the_area_of_polygon3 (C,A,C))) + (beta * ( the_area_of_polygon3 (C1,A,C)))))))) by Th7, A22

      .= (((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * S) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * S)) + (((((((gamma * (1 - mu)) * beta) * (1 - nu)) * alpha) * (1 - lambda)) * S) - (((((gamma * (1 - mu)) * beta) * nu) * (1 - alpha)) * S))) - (((gamma * mu) * alpha) * ((((1 - lambda) * (1 - beta)) * S) + ((lambda * beta) * ( the_area_of_polygon3 ((((1 - nu) * A) + (nu * B)),A,C)))))) by A4

      .= (((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * S) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * S)) + (((((((gamma * (1 - mu)) * beta) * (1 - nu)) * alpha) * (1 - lambda)) * S) - (((((gamma * (1 - mu)) * beta) * nu) * (1 - alpha)) * S))) - (((gamma * mu) * alpha) * ((((1 - lambda) * (1 - beta)) * S) + ((lambda * beta) * (((1 - nu) * ( the_area_of_polygon3 (A,A,C))) + (nu * ( the_area_of_polygon3 (B,A,C)))))))) by Th7

      .= (((((((1 - gamma) * (1 - alpha)) * (1 - beta)) - (((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu))) + ((((((gamma * (1 - mu)) * beta) * (1 - nu)) * alpha) * (1 - lambda)) - ((((gamma * (1 - mu)) * beta) * nu) * (1 - alpha)))) + ((((((gamma * mu) * alpha) * lambda) * beta) * nu) - ((((gamma * mu) * alpha) * (1 - lambda)) * (1 - beta)))) * S)

      .= ((((((((mu * nu) * (1 / q3)) * ((lambda * mu) * (1 / q1))) * ((nu * lambda) * (1 / q2))) - ((((((mu * nu) * (1 / q3)) * ((1 - mu) * (1 / q1))) * lambda) * ((1 - lambda) * (1 / q2))) * (1 - nu))) + ((((((((1 - nu) * (1 / q3)) * (1 - mu)) * ((1 - lambda) * (1 / q2))) * (1 - nu)) * ((1 - mu) * (1 / q1))) * (1 - lambda)) - ((((((1 - nu) * (1 / q3)) * (1 - mu)) * ((1 - lambda) * (1 / q2))) * nu) * ((lambda * mu) * (1 / q1))))) + ((((((((1 - nu) * (1 / q3)) * mu) * ((1 - mu) * (1 / q1))) * lambda) * ((1 - lambda) * (1 / q2))) * nu) - ((((((1 - nu) * (1 / q3)) * mu) * ((1 - mu) * (1 / q1))) * (1 - lambda)) * ((nu * lambda) * (1 / q2))))) * S) by A28, A31, A29, A32, A30, A33

      .= ((((((mu * nu) * lambda) - (((1 - mu) * (1 - nu)) * (1 - lambda))) ^2 ) * (((1 / q1) * (1 / q2)) * (1 / q3))) * S)

      .= ((((((mu * nu) * lambda) - (((1 - mu) * (1 - nu)) * (1 - lambda))) ^2 ) * ((1 / (q1 * q2)) * (1 / q3))) * S) by XCMPLX_1: 102

      .= ((((((mu * nu) * lambda) - (((1 - mu) * (1 - nu)) * (1 - lambda))) ^2 ) * (1 / ((q1 * q2) * q3))) * S) by XCMPLX_1: 102;

      hence thesis by XCMPLX_1: 99;

    end;

    ::$Notion-Name

    theorem :: MENELAUS:20

    ((A,B,C) is_a_triangle & A1 = (((2 / 3) * B) + ((1 / 3) * C)) & B1 = (((2 / 3) * C) + ((1 / 3) * A)) & C1 = (((2 / 3) * A) + ((1 / 3) * B)) & (A,A1,B2,C2) are_collinear & (B,B1,A2,C2) are_collinear & (C,C1,A2,B2) are_collinear ) implies ( the_area_of_polygon3 (A2,B2,C2)) = (( the_area_of_polygon3 (A,B,C)) / 7)

    proof

      assume that

       A1: (A,B,C) is_a_triangle and

       A2: A1 = (((2 / 3) * B) + ((1 / 3) * C)) & B1 = (((2 / 3) * C) + ((1 / 3) * A)) & C1 = (((2 / 3) * A) + ((1 / 3) * B)) and

       A3: (A,A1,B2,C2) are_collinear & (B,B1,A2,C2) are_collinear & (C,C1,A2,B2) are_collinear ;

      consider lambda, mu, nu such that

       A4: lambda = (1 / 3) & mu = (1 / 3) & nu = (1 / 3);

      A1 = (((1 - lambda) * B) + (lambda * C)) & B1 = (((1 - mu) * C) + (mu * A)) & C1 = (((1 - nu) * A) + (nu * B)) & lambda <> 1 & mu <> 1 & nu <> 1 & (1 - lambda) = (2 / 3) & (1 - mu) = (2 / 3) & (1 - nu) = (2 / 3) by A2, A4;

      then ( the_area_of_polygon3 (A2,B2,C2)) = (((((((1 / 3) * (1 / 3)) * (1 / 3)) - (((2 / 3) * (2 / 3)) * (2 / 3))) ^2 ) / ((((2 / 3) + ((1 / 3) * (1 / 3))) * ((2 / 3) + ((1 / 3) * (1 / 3)))) * ((2 / 3) + ((1 / 3) * (1 / 3))))) * ( the_area_of_polygon3 (A,B,C))) by Th19, A1, A3;

      hence thesis;

    end;

    

     Lm7: ((A,B,C) is_a_triangle & A1 = (((1 - lambda) * B) + (lambda * C)) & B1 = (((1 - mu) * C) + (mu * A)) & C1 = (((1 - nu) * A) + (nu * B)) & lambda <> 1 & mu <> 1 & nu <> 1 & (A,A1,B2,C2) are_collinear & (B,B1,A2,C2) are_collinear & (C,C1,A2,B2) are_collinear ) implies ((((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu))) = 1 iff (A2,B2,C2) are_collinear )

    proof

      assume that

       A1: (A,B,C) is_a_triangle and

       A2: A1 = (((1 - lambda) * B) + (lambda * C)) and

       A3: B1 = (((1 - mu) * C) + (mu * A)) and

       A4: C1 = (((1 - nu) * A) + (nu * B)) and

       A5: lambda <> 1 and

       A6: mu <> 1 and

       A7: nu <> 1 and

       A8: (A,A1,B2,C2) are_collinear and

       A9: (B,B1,A2,C2) are_collinear and

       A10: (C,C1,A2,B2) are_collinear ;

      set q = (((1 - lambda) * (1 - mu)) * (1 - nu));

      

       A11: 0 = (((lambda * mu) * nu) - q) iff (((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu))) = 1 by Lm4, A5, A6, A7;

      

       A12: ((((1 - mu) + (lambda * mu)) * ((1 - lambda) + (nu * lambda))) * ((1 - nu) + (mu * nu))) <> 0 & ( the_area_of_polygon3 (A2,B2,C2)) = ((((((mu * nu) * lambda) - (((1 - mu) * (1 - nu)) * (1 - lambda))) ^2 ) / ((((1 - mu) + (lambda * mu)) * ((1 - lambda) + (nu * lambda))) * ((1 - nu) + (mu * nu)))) * ( the_area_of_polygon3 (A,B,C))) by Th19, A1, A2, A3, A4, A5, A6, A7, A8, A9, A10;

      ( the_area_of_polygon3 (A,B,C)) <> 0 by Th9, A1;

      hence thesis by A12, Th9, A11;

    end;

    ::$Notion-Name

    theorem :: MENELAUS:21

    

     Th21: ((A,B,C) is_a_triangle & A1 = (((1 - lambda) * B) + (lambda * C)) & B1 = (((1 - mu) * C) + (mu * A)) & C1 = (((1 - nu) * A) + (nu * B)) & lambda <> 1 & mu <> 1 & nu <> 1 & ((1 - mu) + (lambda * mu)) <> 0 & ((1 - lambda) + (nu * lambda)) <> 0 & ((1 - nu) + (mu * nu)) <> 0 ) implies ((((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu))) = 1 iff (ex A2 st (A,A1,A2) are_collinear & (B,B1,A2) are_collinear & (C,C1,A2) are_collinear ))

    proof

      set q1 = ((1 - mu) + (lambda * mu));

      set q2 = ((1 - lambda) + (nu * lambda));

      set q3 = ((1 - nu) + (mu * nu));

      assume that

       A1: (A,B,C) is_a_triangle and

       A2: A1 = (((1 - lambda) * B) + (lambda * C)) and

       A3: B1 = (((1 - mu) * C) + (mu * A)) and

       A4: C1 = (((1 - nu) * A) + (nu * B)) and

       A5: lambda <> 1 and

       A6: mu <> 1 and

       A7: nu <> 1 and

       A8: q1 <> 0 and

       A9: q2 <> 0 and

       A10: q3 <> 0 ;

      

       A11: (C,A,B) is_a_triangle by A1;

      

       A12: (B,C,A) is_a_triangle by A1;

      consider C2 such that

       A13: (A,A1,C2) are_collinear and

       A14: (B,B1,C2) are_collinear by Lm3, A1, A2, A3, A8;

      consider B2 such that

       A15: (C,C1,B2) are_collinear and

       A16: (A,A1,B2) are_collinear by Lm3, A11, A4, A2, A9;

      consider A2 such that

       A17: (B,B1,A2) are_collinear and

       A18: (C,C1,A2) are_collinear by Lm3, A12, A3, A4, A10;

      

       A19: A <> A1 by Th14, A1, A2;

      (C2,A,A1) are_collinear by A13;

      then

       A20: C2 in ( Line (A,A1)) by A19, Th13;

      (B2,A,A1) are_collinear by A16;

      then

       A21: B2 in ( Line (A,A1)) by A19, Th13;

      

       A22: (A,A1,B2,C2) are_collinear by A13, A16, A19, RLTOPSP1: 81;

      (B,C,A) is_a_triangle by A1;

      then B <> B1 by Th14, A3;

      then

       A23: (B,B1,A2,C2) are_collinear by A14, A17, RLTOPSP1: 81;

      (C,A,B) is_a_triangle by A1;

      then C <> C1 by Th14, A4;

      then

       A24: (C,C1,A2,B2) are_collinear by A15, A18, RLTOPSP1: 81;

      hereby

        assume

         A25: (((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu))) = 1;

        per cases ;

          suppose

           A26: B2 <> C2;

          take A2;

          (A2,B2,C2) are_collinear by A25, Lm7, A1, A2, A3, A4, A5, A6, A7, A22, A23, A24;

          then

           A27: A2 in ( Line (B2,C2)) by Th13, A26;

          ( Line (B2,C2)) c= ( Line (A,A1)) by A20, A21, EUCLID_4: 42;

          then (A2,A,A1) are_collinear by Th13, A19, A27;

          hence (A,A1,A2) are_collinear ;

          thus (B,B1,A2) are_collinear & (C,C1,A2) are_collinear by A17, A18;

        end;

          suppose

           A28: B2 = C2;

          take B2;

          thus (A,A1,B2) are_collinear & (B,B1,B2) are_collinear & (C,C1,B2) are_collinear by A28, A14, A15, A16;

        end;

      end;

      given C3 such that

       A29: (A,A1,C3) are_collinear and

       A30: (B,B1,C3) are_collinear and

       A31: (C,C1,C3) are_collinear ;

      

       A32: (C3,B2,C2) are_collinear

      proof

        per cases ;

          suppose

           A33: B2 <> C2;

          (C3,A,A1) are_collinear by A29;

          then

           A34: C3 in ( Line (A,A1)) by Th13, A19;

          ( Line (A,A1)) c= ( Line (B2,C2)) by A20, A21, A33, EUCLID_4: 43;

          hence thesis by A33, Th13, A34;

        end;

          suppose B2 = C2;

          then not (C3,B2,C2) are_mutually_distinct by ZFMISC_1:def 5;

          hence thesis by EUCLID_6: 20;

        end;

      end;

      C3 = A2

      proof

        assume

         A35: C3 <> A2;

        (C,A,B) is_a_triangle by A1;

        then

         A36: C <> C1 by Th14, A4;

        then

         A37: ( Line (C,C1)) is being_line;

        (B,C,A) is_a_triangle by A1;

        then

         A38: B <> B1 by Th14, A3;

        then

         A39: ( Line (B,B1)) is being_line;

        (C3,B,B1) are_collinear by A30;

        then

         A40: C3 in ( Line (B,B1)) by Th13, A38;

        (A2,B,B1) are_collinear by A17;

        then

         A41: A2 in ( Line (B,B1)) by Th13, A38;

        (A2,C,C1) are_collinear by A18;

        then

         A42: A2 in ( Line (C,C1)) by Th13, A36;

        (C3,C,C1) are_collinear by A31;

        then C3 in ( Line (C,C1)) by Th13, A36;

        then

         A43: ( Line (B,B1)) = ( Line (C,C1)) by A40, A35, A41, A42, A39, A37, EUCLID_4: 44;

        

         A44: (1 - nu) <> 0 by A7;

        B in ( Line (B,B1)) by EUCLID_4: 41;

        then (B,C,C1) are_collinear by Th13, A36, A43;

        then ( the_area_of_polygon3 (B,C,C1)) = 0 by Th9;

        then ( the_area_of_polygon3 (C1,B,C)) = 0 ;

        then (((1 - nu) * ( the_area_of_polygon3 (A,B,C))) + (nu * ( the_area_of_polygon3 (B,B,C)))) = 0 by Th7, A4;

        then ( the_area_of_polygon3 (A,B,C)) = 0 by A44;

        hence contradiction by Th9, A1;

      end;

      hence thesis by A32, Lm7, A1, A2, A3, A4, A5, A6, A7, A22, A23, A24;

    end;

    ::$Notion-Name

    theorem :: MENELAUS:22

    ((A,B,C) is_a_triangle & A1 = (((1 - lambda) * B) + (lambda * C)) & B1 = (((1 - mu) * C) + (mu * A)) & C1 = (((1 - nu) * A) + (nu * B)) & lambda <> 1 & mu <> 1 & nu <> 1) implies ((((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu))) = 1 iff (( Line (A,A1)),( Line (B,B1)),( Line (C,C1))) are_concurrent )

    proof

      assume that

       A1: (A,B,C) is_a_triangle and

       A2: A1 = (((1 - lambda) * B) + (lambda * C)) and

       A3: B1 = (((1 - mu) * C) + (mu * A)) and

       A4: C1 = (((1 - nu) * A) + (nu * B)) and

       A5: lambda <> 1 and

       A6: mu <> 1 and

       A7: nu <> 1;

      

       A8: A <> A1 by Th14, A1, A2;

      

       A9: (B,C,A) is_a_triangle by A1;

      then

       A10: B <> B1 by Th14, A3;

      

       A11: (C,A,B) is_a_triangle by A1;

      then

       A12: C <> C1 by Th14, A4;

      hereby

        assume

         A13: (((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu))) = 1;

        per cases ;

          suppose ((1 - mu) + (lambda * mu)) <> 0 & ((1 - lambda) + (nu * lambda)) <> 0 & ((1 - nu) + (mu * nu)) <> 0 ;

          then

          consider A2 such that

           A14: (A,A1,A2) are_collinear & (B,B1,A2) are_collinear & (C,C1,A2) are_collinear by A13, Th21, A1, A2, A3, A4, A5, A6, A7;

          (A2,A,A1) are_collinear & (A2,B,B1) are_collinear & (A2,C,C1) are_collinear by A14;

          then A2 in ( Line (A,A1)) & A2 in ( Line (B,B1)) & A2 in ( Line (C,C1)) by Th13, A8, A10, A12;

          hence (( Line (A,A1)),( Line (B,B1)),( Line (C,C1))) are_concurrent ;

        end;

          suppose not (((1 - mu) + (lambda * mu)) <> 0 & ((1 - lambda) + (nu * lambda)) <> 0 & ((1 - nu) + (mu * nu)) <> 0 );

          then ( Line (A,A1)) is_parallel_to ( Line (B,B1)) & ( Line (B,B1)) is_parallel_to ( Line (C,C1)) & ( Line (C,C1)) is_parallel_to ( Line (A,A1)) by A13, Lm6, A1, A2, A3, A4, A5, A6, A7;

          hence (( Line (A,A1)),( Line (B,B1)),( Line (C,C1))) are_concurrent ;

        end;

      end;

      assume (( Line (A,A1)),( Line (B,B1)),( Line (C,C1))) are_concurrent ;

      per cases ;

        suppose

         A15: ( Line (A,A1)) is_parallel_to ( Line (B,B1)) & ( Line (B,B1)) is_parallel_to ( Line (C,C1)) & ( Line (C,C1)) is_parallel_to ( Line (A,A1));

        then ((1 - mu) + (lambda * mu)) = 0 & ((1 - nu) + (mu * nu)) = 0 & ((1 - lambda) + (nu * lambda)) = 0 by Th16, A1, A9, A11, A2, A3, A4, A5, A6, A7;

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

      end;

        suppose ex C2 st (C2 in ( Line (A,A1)) & C2 in ( Line (B,B1)) & C2 in ( Line (C,C1)));

        then

        consider C2 such that

         A16: C2 in ( Line (A,A1)) & C2 in ( Line (B,B1)) & C2 in ( Line (C,C1));

         not ( Line (A,A1)) is_parallel_to ( Line (B,B1)) & not ( Line (B,B1)) is_parallel_to ( Line (C,C1)) & not ( Line (C,C1)) is_parallel_to ( Line (A,A1)) by A16, XBOOLE_0: 3;

        then

         A17: ((1 - mu) + (lambda * mu)) <> 0 & ((1 - nu) + (mu * nu)) <> 0 & ((1 - lambda) + (nu * lambda)) <> 0 by Th16, A1, A2, A3, A4, A5, A6, A7, A9, A11;

        (C2,A,A1) are_collinear & (C2,B,B1) are_collinear & (C2,C,C1) are_collinear by A16, Th13, A8, A10, A12;

        then (A,A1,C2) are_collinear & (B,B1,C2) are_collinear & (C,C1,C2) are_collinear ;

        hence thesis by A17, Th21, A1, A2, A3, A4, A5, A6, A7;

      end;

    end;