:: MENELAUS semantic presentation

begin


notation
let X, Y be Subset of (TOP-REAL 2);
synonym X is_parallel_to Y for X misses Y;
end;

definition
let X, Y, Z be Subset of (TOP-REAL 2);
predX,Y,Z are_concurrent  means :def2: :: MENELAUS:def 1
( ( X is_parallel_to Y & Y is_parallel_to Z & Z is_parallel_to X ) or ex A being Point of (TOP-REAL 2) st
( A in X & A in Y & A in Z ) );
end;

:: deftheorem def2 defines are_concurrent MENELAUS:def_1_:_
 for X, Y, Z being Subset of (TOP-REAL 2) holds
( X,Y,Z are_concurrent iff ( ( X is_parallel_to Y & Y is_parallel_to Z & Z is_parallel_to X ) or ex A being Point of (TOP-REAL 2) st
( A in X & A in Y & A in Z ) ) );

theorem Th1: :: MENELAUS:1
for A, B being Point of (TOP-REAL 2) holds
( (A + B) `1 = (A `1) + (B `1) & (A + B) `2 = (A `2) + (B `2) )
proof
let A, B be Point of (TOP-REAL 2); ::_thesis: ( (A + B) `1 = (A `1) + (B `1) & (A + B) `2 = (A `2) + (B `2) )
 A + B = |[((A `1) + (B `1)),((A `2) + (B `2))]| by EUCLID:55;
hence  ( (A + B) `1 = (A `1) + (B `1) & (A + B) `2 = (A `2) + (B `2) ) by EUCLID:52; ::_thesis: verum
end;

theorem Th2: :: MENELAUS:2
for A being Point of (TOP-REAL 2)
for lambda being Real holds
( (lambda * A) `1 = lambda * (A `1) & (lambda * A) `2 = lambda * (A `2) )
proof
let A be Point of (TOP-REAL 2); ::_thesis: for lambda being Real holds
( (lambda * A) `1 = lambda * (A `1) & (lambda * A) `2 = lambda * (A `2) )
let lambda be Real; ::_thesis: ( (lambda * A) `1 = lambda * (A `1) & (lambda * A) `2 = lambda * (A `2) )
 lambda * A = |[(lambda * (A `1)),(lambda * (A `2))]| by EUCLID:57;
hence  ( (lambda * A) `1 = lambda * (A `1) & (lambda * A) `2 = lambda * (A `2) ) by EUCLID:52; ::_thesis: verum
end;

theorem Th3: :: MENELAUS:3
for A being Point of (TOP-REAL 2) holds
( (- A) `1 = - (A `1) & (- A) `2 = - (A `2) )
proof
let A be Point of (TOP-REAL 2); ::_thesis: ( (- A) `1 = - (A `1) & (- A) `2 = - (A `2) )
 - A = |[(- (A `1)),(- (A `2))]| by EUCLID:59;
hence  ( (- A) `1 = - (A `1) & (- A) `2 = - (A `2) ) by EUCLID:52; ::_thesis: verum
end;

theorem Th4: :: MENELAUS:4
for A, B being Point of (TOP-REAL 2)
for lambda, mu being Real holds
( ((lambda * A) + (mu * B)) `1 = (lambda * (A `1)) + (mu * (B `1)) & ((lambda * A) + (mu * B)) `2 = (lambda * (A `2)) + (mu * (B `2)) )
proof
let A, B be Point of (TOP-REAL 2); ::_thesis: for lambda, mu being Real holds
( ((lambda * A) + (mu * B)) `1 = (lambda * (A `1)) + (mu * (B `1)) & ((lambda * A) + (mu * B)) `2 = (lambda * (A `2)) + (mu * (B `2)) )
let lambda, mu be Real; ::_thesis: ( ((lambda * A) + (mu * B)) `1 = (lambda * (A `1)) + (mu * (B `1)) & ((lambda * A) + (mu * B)) `2 = (lambda * (A `2)) + (mu * (B `2)) )
((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; ::_thesis: ((lambda * A) + (mu * B)) `2 = (lambda * (A `2)) + (mu * (B `2))
((lambda * A) + (mu * B)) `2 = ((lambda * A) `2) + ((mu * B) `2) by Th1
.= (lambda * (A `2)) + ((mu * B) `2) by Th2 ;
hence  ((lambda * A) + (mu * B)) `2 = (lambda * (A `2)) + (mu * (B `2)) by Th2; ::_thesis: verum
end;

theorem :: MENELAUS:5
for A being Point of (TOP-REAL 2)
for lambda being Real holds
( ((- lambda) * A) `1 = - (lambda * (A `1)) & ((- lambda) * A) `2 = - (lambda * (A `2)) )
proof
let A be Point of (TOP-REAL 2); ::_thesis: for lambda being Real holds
( ((- lambda) * A) `1 = - (lambda * (A `1)) & ((- lambda) * A) `2 = - (lambda * (A `2)) )
let lambda be Real; ::_thesis: ( ((- lambda) * A) `1 = - (lambda * (A `1)) & ((- lambda) * A) `2 = - (lambda * (A `2)) )
((- lambda) * A) `1 = (- (lambda * A)) `1 by EUCLID:40
.= - ((lambda * A) `1) by Th3 ;
hence  ((- lambda) * A) `1 = - (lambda * (A `1)) by Th2; ::_thesis: ((- lambda) * A) `2 = - (lambda * (A `2))
((- lambda) * A) `2 = (- (lambda * A)) `2 by EUCLID:40
.= - ((lambda * A) `2) by Th3 ;
hence  ((- lambda) * A) `2 = - (lambda * (A `2)) by Th2; ::_thesis: verum
end;

theorem :: MENELAUS:6
for A, B being Point of (TOP-REAL 2)
for lambda, mu being Real holds
( ((lambda * A) - (mu * B)) `1 = (lambda * (A `1)) - (mu * (B `1)) & ((lambda * A) - (mu * B)) `2 = (lambda * (A `2)) - (mu * (B `2)) )
proof
let A, B be Point of (TOP-REAL 2); ::_thesis: for lambda, mu being Real holds
( ((lambda * A) - (mu * B)) `1 = (lambda * (A `1)) - (mu * (B `1)) & ((lambda * A) - (mu * B)) `2 = (lambda * (A `2)) - (mu * (B `2)) )
let lambda, mu be Real; ::_thesis: ( ((lambda * A) - (mu * B)) `1 = (lambda * (A `1)) - (mu * (B `1)) & ((lambda * A) - (mu * B)) `2 = (lambda * (A `2)) - (mu * (B `2)) )
((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; ::_thesis: ((lambda * A) - (mu * B)) `2 = (lambda * (A `2)) - (mu * (B `2))
((lambda * A) - (mu * B)) `2 = ((lambda * A) `2) - ((mu * B) `2) by EUCLID_6:41
.= (lambda * (A `2)) - ((mu * B) `2) by Th2 ;
hence  ((lambda * A) - (mu * B)) `2 = (lambda * (A `2)) - (mu * (B `2)) by Th2; ::_thesis: verum
end;

theorem Th7: :: MENELAUS:7
for A, A1, B, C being Point of (TOP-REAL 2)
for lambda being Real holds 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
let A, A1, B, C be Point of (TOP-REAL 2); ::_thesis: for lambda being Real holds 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)))
let lambda be Real; ::_thesis: 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)))
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  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))) ; ::_thesis: verum
end;

theorem Th8: :: MENELAUS:8
for A, B, C being Point of (TOP-REAL 2) st angle (A,B,C) = 0 & A,B,C are_mutually_different & not angle (B,C,A) = PI holds
angle (B,A,C) = PI
proof
let A, B, C be Point of (TOP-REAL 2); ::_thesis: ( angle (A,B,C) = 0 & A,B,C are_mutually_different & not angle (B,C,A) = PI implies angle (B,A,C) = PI )
set z1 = euc2cpx A;
set z2 = euc2cpx B;
set z3 = euc2cpx C;
assume that
A: angle (A,B,C) = 0 and
B: A,B,C are_mutually_different ; ::_thesis: ( angle (B,C,A) = PI or angle (B,A,C) = PI )
 ( A <> B & A <> C & B <> C ) by B, ZFMISC_1:def_5;
then C: ( euc2cpx A <> euc2cpx B & euc2cpx A <> euc2cpx C & euc2cpx B <> euc2cpx C ) by EUCLID_3:4;
percases ( ( angle ((euc2cpx B),(euc2cpx C),(euc2cpx A)) = 0 & angle ((euc2cpx C),(euc2cpx A),(euc2cpx B)) = PI ) or not angle ((euc2cpx B),(euc2cpx C),(euc2cpx A)) = 0 or not angle ((euc2cpx C),(euc2cpx A),(euc2cpx B)) = PI ) ;
suppose ( angle ((euc2cpx B),(euc2cpx C),(euc2cpx A)) = 0 & angle ((euc2cpx C),(euc2cpx A),(euc2cpx B)) = PI ) ; ::_thesis: ( angle (B,C,A) = PI or angle (B,A,C) = PI )
hence  ( angle (B,C,A) = PI or angle (B,A,C) = PI ) by COMPLEX2:82; ::_thesis: verum
end;
suppose ( not angle ((euc2cpx B),(euc2cpx C),(euc2cpx A)) = 0 or not angle ((euc2cpx C),(euc2cpx A),(euc2cpx B)) = PI ) ; ::_thesis: ( angle (B,C,A) = PI or angle (B,A,C) = PI )
hence  ( angle (B,C,A) = PI or angle (B,A,C) = PI ) by COMPLEX2:87, C, A; ::_thesis: verum
end;
end;
end;

theorem Th9: :: MENELAUS:9
for A, B, C being Point of (TOP-REAL 2) holds
( A,B,C is_collinear iff the_area_of_polygon3 (A,B,C) = 0 )
proof
let A, B, C be Point of (TOP-REAL 2); ::_thesis: ( A,B,C is_collinear iff the_area_of_polygon3 (A,B,C) = 0 )
hereby  ::_thesis: ( the_area_of_polygon3 (A,B,C) = 0 implies A,B,C is_collinear )
assume  A,B,C is_collinear ; ::_thesis: the_area_of_polygon3 (A,B,C) = 0
percasesthen  ( A in LSeg (B,C) or B in LSeg (C,A) or C in LSeg (A,B) ) by EUCLID_6:def_3;
suppose A in LSeg (B,C) ; ::_thesis: the_area_of_polygon3 (A,B,C) = 0
then consider lambda being Real such that
A: ( 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, A;
hence  the_area_of_polygon3 (A,B,C) = 0 ; ::_thesis: verum
end;
suppose B in LSeg (C,A) ; ::_thesis: the_area_of_polygon3 (A,B,C) = 0
then consider lambda being Real such that
A: ( 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 A
.= (- ((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 ; ::_thesis: verum
end;
suppose C in LSeg (A,B) ; ::_thesis: the_area_of_polygon3 (A,B,C) = 0
then consider lambda being Real such that
A: ( 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 A
.= (- ((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 ; ::_thesis: verum
end;
end;
end;
assume  the_area_of_polygon3 (A,B,C) = 0 ; ::_thesis: A,B,C is_collinear
then  ((|.(A - B).| * |.(C - B).|) * (sin (angle (C,B,A)))) / 2 = 0 by EUCLID_6:5;
percasesthen  ( |.(A - B).| = 0 or |.(C - B).| = 0 or sin (angle (C,B,A)) = 0 ) ;
suppose |.(A - B).| = 0 ; ::_thesis: A,B,C is_collinear
then  A = B by EUCLID_6:42;
then  not A,B,C are_mutually_different by ZFMISC_1:def_5;
hence  A,B,C is_collinear by EUCLID_6:20; ::_thesis: verum
end;
suppose |.(C - B).| = 0 ; ::_thesis: A,B,C is_collinear
then  C = B by EUCLID_6:42;
then  not A,B,C are_mutually_different by ZFMISC_1:def_5;
hence  A,B,C is_collinear by EUCLID_6:20; ::_thesis: verum
end;
supposeA: sin (angle (C,B,A)) = 0 ; ::_thesis: A,B,C is_collinear
 ( (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 SIN_COS6:21, A;
percasesthen  ( angle (C,B,A) = 0 or angle (C,B,A) = PI ) ;
suppose angle (C,B,A) = 0 ; ::_thesis: A,B,C is_collinear
then  ( angle (B,C,A) = PI or angle (B,A,C) = PI or not C,B,A are_mutually_different ) by Th8;
then  ( C in LSeg (B,A) or A in LSeg (B,C) or not C <> B or not C <> A or not 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_different ) by ZFMISC_1:def_5;
hence  A,B,C is_collinear by EUCLID_6:def_3, EUCLID_6:20; ::_thesis: verum
end;
suppose angle (C,B,A) = PI ; ::_thesis: A,B,C is_collinear
then  B in LSeg (C,A) by EUCLID_6:11;
hence  A,B,C is_collinear by EUCLID_6:def_3; ::_thesis: verum
end;
end;
end;
end;
end;

theorem Th21: :: MENELAUS:10
for B, C being Point of (TOP-REAL 2) holds the_area_of_polygon3 ((0. (TOP-REAL 2)),B,C) = (((B `1) * (C `2)) - ((C `1) * (B `2))) / 2
proof
let B, C be Point of (TOP-REAL 2); ::_thesis: the_area_of_polygon3 ((0. (TOP-REAL 2)),B,C) = (((B `1) * (C `2)) - ((C `1) * (B `2))) / 2
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  the_area_of_polygon3 ((0. (TOP-REAL 2)),B,C) = (((B `1) * (C `2)) - ((C `1) * (B `2))) / 2 ; ::_thesis: verum
end;

theorem :: MENELAUS:11
for A, A1, B, C being Point of (TOP-REAL 2) holds 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
let A, A1, B, C be Point of (TOP-REAL 2); ::_thesis: 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))
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  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)) by Th21; ::_thesis: verum
end;

theorem Th12: :: MENELAUS:12
for A, B, C being Point of (TOP-REAL 2) st A in LSeg (B,C) holds
A in Line (B,C)
proof
let A, B, C be Point of (TOP-REAL 2); ::_thesis: ( A in LSeg (B,C) implies A in Line (B,C) )
assume  A in LSeg (B,C) ; ::_thesis: A in Line (B,C)
then consider lambda being Real such that
A: ( A = ((1 - lambda) * B) + (lambda * C) & 0 <= lambda & lambda <= 1 ) ;
thus  A in Line (B,C) by A; ::_thesis: verum
end;

theorem Th13: :: MENELAUS:13
for B, C, A being Point of (TOP-REAL 2) st B <> C holds
( A,B,C is_collinear iff A in Line (B,C) )
proof
let B, C, A be Point of (TOP-REAL 2); ::_thesis: ( B <> C implies ( A,B,C is_collinear iff A in Line (B,C) ) )
assume A: B <> C ; ::_thesis: ( A,B,C is_collinear iff A in Line (B,C) )
hereby  ::_thesis: ( A in Line (B,C) implies A,B,C is_collinear )
assume  A,B,C is_collinear ; ::_thesis: A in Line (B,C)
percasesthen  ( A in LSeg (B,C) or B in LSeg (C,A) or C in LSeg (A,B) ) by EUCLID_6:def_3;
suppose A in LSeg (B,C) ; ::_thesis: A in Line (B,C)
hence  A in Line (B,C) by Th12; ::_thesis: verum
end;
suppose B in LSeg (C,A) ; ::_thesis: A in Line (B,C)
then B: B in Line (C,A) by Th12;
C: ( C in Line (C,A) & A in Line (C,A) ) by EUCLID_4:41;
then  Line (C,A) c= Line (B,C) by EUCLID_4:43, B, A;
hence  A in Line (B,C) by C; ::_thesis: verum
end;
suppose C in LSeg (A,B) ; ::_thesis: A in Line (B,C)
then B: C in Line (A,B) by Th12;
C: ( A in Line (A,B) & B in Line (A,B) ) by EUCLID_4:41;
then  Line (A,B) c= Line (B,C) by EUCLID_4:43, B, A;
hence  A in Line (B,C) by C; ::_thesis: verum
end;
end;
end;
assume  A in Line (B,C) ; ::_thesis: A,B,C is_collinear
then consider lambda being Real such that
A: 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, A;
hence  A,B,C is_collinear by Th9; ::_thesis: verum
end;

Lm1:  for A1, B, C, B1, A, C2 being Point of (TOP-REAL 2)
for lambda, mu, alpha being Real st A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & C2 = ((1 - alpha) * A) + (alpha * A1) holds
the_area_of_polygon3 (B,B1,C2) = ((1 - mu) - (alpha * ((1 - mu) + (lambda * mu)))) * (the_area_of_polygon3 (A,B,C))
proof
let A1, B, C, B1, A, C2 be Point of (TOP-REAL 2); ::_thesis: for lambda, mu, alpha being Real st A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & C2 = ((1 - alpha) * A) + (alpha * A1) holds
the_area_of_polygon3 (B,B1,C2) = ((1 - mu) - (alpha * ((1 - mu) + (lambda * mu)))) * (the_area_of_polygon3 (A,B,C))
let lambda, mu, alpha be Real; ::_thesis: ( 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)) )
assume that
A: A1 = ((1 - lambda) * B) + (lambda * C) and
B: B1 = ((1 - mu) * C) + (mu * A) and
C: C2 = ((1 - alpha) * A) + (alpha * A1) ; ::_thesis: the_area_of_polygon3 (B,B1,C2) = ((1 - mu) - (alpha * ((1 - mu) + (lambda * mu)))) * (the_area_of_polygon3 (A,B,C))
the_area_of_polygon3 (B,B1,C2) = the_area_of_polygon3 ((((1 - alpha) * A) + (alpha * A1)),B,B1) by C
.= ((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, A
.= ((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, B
.= (((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, B
.= (((1 - alpha) * (1 - mu)) * (the_area_of_polygon3 (A,B,C))) - (((alpha * lambda) * mu) * (the_area_of_polygon3 (A,B,C))) ;
hence  the_area_of_polygon3 (B,B1,C2) = ((1 - mu) - (alpha * ((1 - mu) + (lambda * mu)))) * (the_area_of_polygon3 (A,B,C)) ; ::_thesis: verum
end;

theorem Th14: :: MENELAUS:14
for A, B, C, A1 being Point of (TOP-REAL 2)
for lambda being Real st A,B,C is_a_triangle & A1 = ((1 - lambda) * B) + (lambda * C) holds
A <> A1
proof
let A, B, C, A1 be Point of (TOP-REAL 2); ::_thesis: for lambda being Real st A,B,C is_a_triangle & A1 = ((1 - lambda) * B) + (lambda * C) holds
A <> A1
let lambda be Real; ::_thesis: ( A,B,C is_a_triangle & A1 = ((1 - lambda) * B) + (lambda * C) implies A <> A1 )
assume that
A: A,B,C is_a_triangle and
B: A1 = ((1 - lambda) * B) + (lambda * C) ; ::_thesis: A <> A1
 A,B,C are_mutually_different by A, EUCLID_6:20;
then H: ( A <> B & A <> C & B <> C ) by ZFMISC_1:def_5;
hereby  ::_thesis: verum
assume  A = A1 ; ::_thesis: contradiction
then  A in Line (B,C) by B;
hence  contradiction by H, Th13, A; ::_thesis: verum
end;
end;

theorem Th15: :: MENELAUS:15
for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds
( 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 )
proof
let A, B, C be Point of (TOP-REAL 2); ::_thesis: ( 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 ) )
assume  A,B,C is_a_triangle ; ::_thesis: ( 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 )
then A: the_area_of_polygon3 (A,B,C) <> 0 by Th9;
then  the_area_of_polygon3 (A,C,B) <> 0 ;
hence  A,C,B is_a_triangle by Th9; ::_thesis: ( B,A,C is_a_triangle & B,C,A is_a_triangle & C,A,B is_a_triangle & C,B,A is_a_triangle )
 the_area_of_polygon3 (B,A,C) <> 0 by A;
hence  B,A,C is_a_triangle by Th9; ::_thesis: ( B,C,A is_a_triangle & C,A,B is_a_triangle & C,B,A is_a_triangle )
 the_area_of_polygon3 (B,C,A) <> 0 by A;
hence  B,C,A is_a_triangle by Th9; ::_thesis: ( C,A,B is_a_triangle & C,B,A is_a_triangle )
 the_area_of_polygon3 (C,A,B) <> 0 by A;
hence  C,A,B is_a_triangle by Th9; ::_thesis: C,B,A is_a_triangle
 the_area_of_polygon3 (C,B,A) <> 0 by A;
hence  C,B,A is_a_triangle by Th9; ::_thesis: verum
end;

Lm2:  for A, B, C, A1, B1, C2 being Point of (TOP-REAL 2)
for lambda, mu being Real st A,B,C is_a_triangle & A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & mu <> 1 & A,A1,C2 is_collinear & B,B1,C2 is_collinear holds
( (1 - mu) + (lambda * mu) <> 0 & ex alpha being Real st
( C2 = ((1 - alpha) * A) + (alpha * A1) & alpha = (1 - mu) / ((1 - mu) + (lambda * mu)) ) )
proof
let A, B, C, A1, B1, C2 be Point of (TOP-REAL 2); ::_thesis: for lambda, mu being Real st A,B,C is_a_triangle & A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & mu <> 1 & A,A1,C2 is_collinear & B,B1,C2 is_collinear holds
( (1 - mu) + (lambda * mu) <> 0 & ex alpha being Real st
( C2 = ((1 - alpha) * A) + (alpha * A1) & alpha = (1 - mu) / ((1 - mu) + (lambda * mu)) ) )
let lambda, mu be Real; ::_thesis: ( A,B,C is_a_triangle & A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & mu <> 1 & A,A1,C2 is_collinear & B,B1,C2 is_collinear implies ( (1 - mu) + (lambda * mu) <> 0 & ex alpha being Real st
( C2 = ((1 - alpha) * A) + (alpha * A1) & alpha = (1 - mu) / ((1 - mu) + (lambda * mu)) ) ) )
assume that
A: A,B,C is_a_triangle and
B: A1 = ((1 - lambda) * B) + (lambda * C) and
C: B1 = ((1 - mu) * C) + (mu * A) and
D: mu <> 1 and
E: A,A1,C2 is_collinear and
F: B,B1,C2 is_collinear ; ::_thesis: ( (1 - mu) + (lambda * mu) <> 0 & ex alpha being Real st
( C2 = ((1 - alpha) * A) + (alpha * A1) & alpha = (1 - mu) / ((1 - mu) + (lambda * mu)) ) )
H2: A <> A1 by Th14, A, B;
H3: the_area_of_polygon3 (A,B,C) <> 0 by A, Th9;
 C2,A,A1 is_collinear by Th15, E;
then  C2 in Line (A,A1) by H2, Th13;
then consider alpha being Real such that
G1: C2 = ((1 - alpha) * A) + (alpha * A1) ;
0 = the_area_of_polygon3 (B,B1,C2) by F, Th9
.= ((1 - mu) - (((1 - mu) + (lambda * mu)) * alpha)) * (the_area_of_polygon3 (A,B,C)) by Lm1, G1, B, C ;
then G3: ( (1 - mu) - (((1 - mu) + (lambda * mu)) * alpha) = 0 & 1 - mu <> 0 ) by H3, D;
then  (1 - mu) + (lambda * mu) <> 0 ;
hence  ( (1 - mu) + (lambda * mu) <> 0 & ex alpha being Real st
( C2 = ((1 - alpha) * A) + (alpha * A1) & alpha = (1 - mu) / ((1 - mu) + (lambda * mu)) ) ) by G1, XCMPLX_1:89, G3; ::_thesis: verum
end;

Lm3:  for A, B, C, A1, B1 being Point of (TOP-REAL 2)
for lambda, mu being Real st A,B,C is_a_triangle & A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & (1 - mu) + (lambda * mu) <> 0 holds
ex C2 being Point of (TOP-REAL 2) st
( A,A1,C2 is_collinear & B,B1,C2 is_collinear )
proof
let A, B, C, A1, B1 be Point of (TOP-REAL 2); ::_thesis: for lambda, mu being Real st A,B,C is_a_triangle & A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & (1 - mu) + (lambda * mu) <> 0 holds
ex C2 being Point of (TOP-REAL 2) st
( A,A1,C2 is_collinear & B,B1,C2 is_collinear )
let lambda, mu be Real; ::_thesis: ( 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 being Point of (TOP-REAL 2) st
( A,A1,C2 is_collinear & B,B1,C2 is_collinear ) )
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 ; ::_thesis: ex C2 being Point of (TOP-REAL 2) st
( A,A1,C2 is_collinear & B,B1,C2 is_collinear )
B2: A <> A1 by Th14, A1, A2;
consider alpha being Real such that
B3: alpha = (1 - mu) / ((1 - mu) + (lambda * mu)) ;
consider C2 being Point of (TOP-REAL 2) such that
B4: C2 = ((1 - alpha) * A) + (alpha * A1) ;
take  C2 ; ::_thesis: ( A,A1,C2 is_collinear & B,B1,C2 is_collinear )
 C2 in Line (A,A1) by B4;
then  C2,A,A1 is_collinear by B2, Th13;
hence  A,A1,C2 is_collinear by Th15; ::_thesis: B,B1,C2 is_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 B3, Lm1, A2, A3, B4
.= ((1 - mu) - (1 - mu)) * (the_area_of_polygon3 (A,B,C)) by XCMPLX_1:87, A4 ;
hence  B,B1,C2 is_collinear by Th9; ::_thesis: verum
end;

Lm4:  for lambda, mu, nu being Real st lambda <> 1 & mu <> 1 & nu <> 1 holds
( 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) iff ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 )
proof
let lambda, mu, nu be Real; ::_thesis: ( 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 ) )
set q = ((1 - lambda) * (1 - mu)) * (1 - nu);
assume  ( lambda <> 1 & mu <> 1 & nu <> 1 ) ; ::_thesis: ( 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) iff ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 )
then A: ( 1 - lambda <> 0 & 1 - mu <> 0 & 1 - nu <> 0 ) ;
 ( 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) iff 0 = ((((1 - lambda) * (1 - mu)) * (1 - nu)) * 1) + (- ((mu * nu) * lambda)) ) ;
then  ( 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) iff (((1 - lambda) * (1 - mu)) * (1 - nu)) * (1 + ((- ((lambda * mu) * nu)) / (((1 - lambda) * (1 - mu)) * (1 - nu)))) = 0 ) by XCMPLX_1:235, A;
then  ( 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) iff 1 + ((- ((lambda * mu) * nu)) / (((1 - lambda) * (1 - mu)) * (1 - nu))) = 0 ) by A;
then  ( 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) iff 1 + (- (((lambda * mu) * nu) / (((1 - lambda) * (1 - mu)) * (1 - nu)))) = 0 ) by XCMPLX_1:187;
then  ( 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) iff 1 = (lambda * (mu * nu)) / ((1 - lambda) * ((1 - mu) * (1 - nu))) ) ;
then  ( 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) iff 1 = ((lambda / (1 - lambda)) * (mu * nu)) / ((1 - mu) * (1 - nu)) ) by XCMPLX_1:83;
then  ( 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) iff 1 = (lambda / (1 - lambda)) * ((mu * nu) / ((1 - mu) * (1 - nu))) ) by XCMPLX_1:74;
then  ( 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) iff 1 = (lambda / (1 - lambda)) * (((mu / (1 - mu)) * nu) / (1 - nu)) ) by XCMPLX_1:83;
then  ( 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) iff 1 = (lambda / (1 - lambda)) * ((mu / (1 - mu)) * (nu / (1 - nu))) ) by XCMPLX_1:74;
hence  ( 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) iff ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 ) ; ::_thesis: verum
end;

Lm6:  for mu, lambda, nu being Real st mu <> 1 & 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) & (1 - mu) + (mu * lambda) = 0 holds
(1 - lambda) + (lambda * nu) = 0
proof
let mu, lambda, nu be Real; ::_thesis: ( mu <> 1 & 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) & (1 - mu) + (mu * lambda) = 0 implies (1 - lambda) + (lambda * nu) = 0 )
assume that
A: mu <> 1 and
B: 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) and
C: (1 - mu) + (mu * lambda) = 0 ; ::_thesis: (1 - lambda) + (lambda * nu) = 0
D: 1 - mu <> 0 by A;
 0 = ((- (1 - mu)) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) by B, C;
then  0 = (1 - mu) * (nu + ((1 - lambda) * (1 - nu))) ;
hence  (1 - lambda) + (lambda * nu) = 0 by D; ::_thesis: verum
end;

theorem Th18: :: MENELAUS:16
for A, B, C, A1, B1 being Point of (TOP-REAL 2)
for lambda, mu being Real st A,B,C is_a_triangle & A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & mu <> 1 holds
( (1 - mu) + (lambda * mu) <> 0 iff not Line (A,A1) is_parallel_to Line (B,B1) )
proof
let A, B, C, A1, B1 be Point of (TOP-REAL 2); ::_thesis: for lambda, mu being Real st A,B,C is_a_triangle & A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & mu <> 1 holds
( (1 - mu) + (lambda * mu) <> 0 iff not Line (A,A1) is_parallel_to Line (B,B1) )
let lambda, mu be Real; ::_thesis: ( 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) ) )
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 ; ::_thesis: ( (1 - mu) + (lambda * mu) <> 0 iff not Line (A,A1) is_parallel_to Line (B,B1) )
A5: A <> A1 by A1, A2, Th14;
 B,C,A is_a_triangle by Th15, A1;
then A6: B <> B1 by A3, Th14;
hereby  ::_thesis: ( not Line (A,A1) is_parallel_to Line (B,B1) implies (1 - mu) + (lambda * mu) <> 0 )
assume  (1 - mu) + (lambda * mu) <> 0 ; ::_thesis: not Line (A,A1) is_parallel_to Line (B,B1)
then consider C2 being Point of (TOP-REAL 2) such that
B1: ( A,A1,C2 is_collinear & B,B1,C2 is_collinear ) by Lm3, A1, A2, A3;
 ( C2,A,A1 is_collinear & C2,B,B1 is_collinear ) by Th15, B1;
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; ::_thesis: verum
end;
assume  not Line (A,A1) is_parallel_to Line (B,B1) ; ::_thesis: (1 - mu) + (lambda * mu) <> 0
then consider C2 being set  such that
B2: ( C2 in Line (A,A1) & C2 in Line (B,B1) ) by XBOOLE_0:3;
reconsider C2 = C2 as Point of (TOP-REAL 2) by B2;
 ( C2,A,A1 is_collinear & C2,B,B1 is_collinear ) by B2, A5, A6, Th13;
then  ( A,A1,C2 is_collinear & B,B1,C2 is_collinear ) by Th15;
hence  (1 - mu) + (lambda * mu) <> 0 by Lm2, A1, A2, A3, A4; ::_thesis: verum
end;

Lm7:  for A, B, C, A1, B1, C1 being Point of (TOP-REAL 2)
for lambda, mu, nu being Real st 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 or not (1 - lambda) + (nu * lambda) <> 0 or not (1 - nu) + (mu * nu) <> 0 ) holds
( ((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
let A, B, C, A1, B1, C1 be Point of (TOP-REAL 2); ::_thesis: for lambda, mu, nu being Real st 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 or not (1 - lambda) + (nu * lambda) <> 0 or not (1 - nu) + (mu * nu) <> 0 ) holds
( ((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) ) )
let lambda, mu, nu be Real; ::_thesis: ( 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 or not (1 - lambda) + (nu * lambda) <> 0 or not (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) ) ) )
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 or not (1 - lambda) + (nu * lambda) <> 0 or not (1 - nu) + (mu * nu) <> 0 ) ; ::_thesis: ( ((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) ) )
A9: B,C,A is_a_triangle by Th15, A1;
A10: C,A,B is_a_triangle by Th15, A1;
hereby  ::_thesis: ( 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) implies ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 )
assume  ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 ; ::_thesis: ( 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 B1: 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) by Lm4, A5, A6, A7;
then B2: 0 = ((nu * lambda) * mu) - (((1 - nu) * (1 - lambda)) * (1 - mu)) ;
B3: 0 = ((mu * nu) * lambda) - (((1 - mu) * (1 - nu)) * (1 - lambda)) by B1;
 ( (1 - mu) + (lambda * mu) = 0 & (1 - nu) + (mu * nu) = 0 & (1 - lambda) + (nu * lambda) = 0 )
proof
percases ( (1 - mu) + (lambda * mu) = 0 or (1 - lambda) + (nu * lambda) = 0 or (1 - nu) + (mu * nu) = 0 ) by A8;
supposeH0: (1 - mu) + (lambda * mu) = 0 ; ::_thesis: ( (1 - mu) + (lambda * mu) = 0 & (1 - nu) + (mu * nu) = 0 & (1 - lambda) + (nu * lambda) = 0 )
then  (1 - lambda) + (nu * lambda) = 0 by Lm6, A6, B1;
hence  ( (1 - mu) + (lambda * mu) = 0 & (1 - nu) + (mu * nu) = 0 & (1 - lambda) + (nu * lambda) = 0 ) by Lm6, A5, B2, H0; ::_thesis: verum
end;
supposeH1: (1 - lambda) + (nu * lambda) = 0 ; ::_thesis: ( (1 - mu) + (lambda * mu) = 0 & (1 - nu) + (mu * nu) = 0 & (1 - lambda) + (nu * lambda) = 0 )
then  (1 - nu) + (nu * mu) = 0 by Lm6, A5, B2;
hence  ( (1 - mu) + (lambda * mu) = 0 & (1 - nu) + (mu * nu) = 0 & (1 - lambda) + (nu * lambda) = 0 ) by Lm6, A7, B3, H1; ::_thesis: verum
end;
supposeH2: (1 - nu) + (mu * nu) = 0 ; ::_thesis: ( (1 - mu) + (lambda * mu) = 0 & (1 - nu) + (mu * nu) = 0 & (1 - lambda) + (nu * lambda) = 0 )
then  (1 - mu) + (lambda * mu) = 0 by Lm6, A7, B3;
hence  ( (1 - mu) + (lambda * mu) = 0 & (1 - nu) + (mu * nu) = 0 & (1 - lambda) + (nu * lambda) = 0 ) by Lm6, A6, B1, H2; ::_thesis: verum
end;
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, Th18, A2, A3, A4, A5, A6, A7, A10; ::_thesis: verum
end;
assume  ( Line (A,A1) is_parallel_to Line (B,B1) & Line (B,B1) is_parallel_to Line (C,C1) ) ; ::_thesis: ( not Line (C,C1) is_parallel_to Line (A,A1) or ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 )
then B4: ( (1 - mu) + (lambda * mu) = 0 & (1 - nu) + (mu * nu) = 0 ) by A1, A9, Th18, 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 B4 ;
hence  ( not Line (C,C1) is_parallel_to Line (A,A1) or ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 ) by Lm4, A5, A6, A7; ::_thesis: verum
end;

begin

theorem Th10: :: MENELAUS:17
for A1, B, C, B1, A, C1 being Point of (TOP-REAL 2)
for lambda, mu, nu being Real st A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & C1 = ((1 - nu) * A) + (nu * B) holds
the_area_of_polygon3 (A1,B1,C1) = ((((1 - lambda) * (1 - mu)) * (1 - nu)) + ((lambda * mu) * nu)) * (the_area_of_polygon3 (A,B,C))
proof
let A1, B, C, B1, A, C1 be Point of (TOP-REAL 2); ::_thesis: for lambda, mu, nu being Real st A1 = ((1 - lambda) * B) + (lambda * C) & B1 = ((1 - mu) * C) + (mu * A) & C1 = ((1 - nu) * A) + (nu * B) holds
the_area_of_polygon3 (A1,B1,C1) = ((((1 - lambda) * (1 - mu)) * (1 - nu)) + ((lambda * mu) * nu)) * (the_area_of_polygon3 (A,B,C))
let lambda, mu, nu be Real; ::_thesis: ( 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)) )
assume that
A: A1 = ((1 - lambda) * B) + (lambda * C) and
B: B1 = ((1 - mu) * C) + (mu * A) and
C: C1 = ((1 - nu) * A) + (nu * B) ; ::_thesis: the_area_of_polygon3 (A1,B1,C1) = ((((1 - lambda) * (1 - mu)) * (1 - nu)) + ((lambda * mu) * nu)) * (the_area_of_polygon3 (A,B,C))
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, A
.= (- ((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 B
.= (- ((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 C
.= ((((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  the_area_of_polygon3 (A1,B1,C1) = ((((1 - lambda) * (1 - mu)) * (1 - nu)) + ((lambda * mu) * nu)) * (the_area_of_polygon3 (A,B,C)) ; ::_thesis: verum
end;

theorem :: MENELAUS:18
for A, B, C, A1, B1, C1 being Point of (TOP-REAL 2)
for lambda, mu, nu being Real st 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 holds
( A1,B1,C1 is_collinear iff ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = - 1 )
proof
let A, B, C, A1, B1, C1 be Point of (TOP-REAL 2); ::_thesis: for lambda, mu, nu being Real st 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 holds
( A1,B1,C1 is_collinear iff ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = - 1 )
let lambda, mu, nu be Real; ::_thesis: ( 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 is_collinear iff ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = - 1 ) )
assume that
A: A,B,C is_a_triangle and
B: A1 = ((1 - lambda) * B) + (lambda * C) and
C: B1 = ((1 - mu) * C) + (mu * A) and
D: C1 = ((1 - nu) * A) + (nu * B) and
E: ( lambda <> 1 & mu <> 1 & nu <> 1 ) ; ::_thesis: ( A1,B1,C1 is_collinear iff ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = - 1 )
F: the_area_of_polygon3 (A,B,C) <> 0 by Th9, A;
set q = ((1 - lambda) * (1 - mu)) * (1 - nu);
G: ( 1 - lambda <> 0 & 1 - mu <> 0 & 1 - nu <> 0 ) by E;
 ( A1,B1,C1 is_collinear iff the_area_of_polygon3 (A1,B1,C1) = 0 ) by Th9;
then  ( A1,B1,C1 is_collinear iff ((((1 - lambda) * (1 - mu)) * (1 - nu)) + ((lambda * mu) * nu)) * (the_area_of_polygon3 (A,B,C)) = 0 ) by Th10, B, C, D;
then  ( A1,B1,C1 is_collinear iff (1 * (((1 - lambda) * (1 - mu)) * (1 - nu))) + ((lambda * mu) * nu) = 0 ) by F;
then  ( A1,B1,C1 is_collinear iff (((1 - lambda) * (1 - mu)) * (1 - nu)) * (1 + (((lambda * mu) * nu) / (((1 - lambda) * (1 - mu)) * (1 - nu)))) = 0 ) by XCMPLX_1:235, G;
then  ( A1,B1,C1 is_collinear iff 1 + (((lambda * mu) * nu) / (((1 - lambda) * (1 - mu)) * (1 - nu))) = 0 ) by G;
then  ( A1,B1,C1 is_collinear iff - 1 = (lambda * (mu * nu)) / ((1 - lambda) * ((1 - mu) * (1 - nu))) ) ;
then  ( A1,B1,C1 is_collinear iff - 1 = ((lambda / (1 - lambda)) * (mu * nu)) / ((1 - mu) * (1 - nu)) ) by XCMPLX_1:83;
then  ( A1,B1,C1 is_collinear iff - 1 = (lambda / (1 - lambda)) * ((mu * nu) / ((1 - mu) * (1 - nu))) ) by XCMPLX_1:74;
then  ( A1,B1,C1 is_collinear iff - 1 = (lambda / (1 - lambda)) * (((mu / (1 - mu)) * nu) / (1 - nu)) ) by XCMPLX_1:83;
then  ( A1,B1,C1 is_collinear iff - 1 = (lambda / (1 - lambda)) * ((mu / (1 - mu)) * (nu / (1 - nu))) ) by XCMPLX_1:74;
hence  ( A1,B1,C1 is_collinear iff ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = - 1 ) ; ::_thesis: verum
end;

theorem Th16: :: MENELAUS:19
for A, B, C, A1, B1, C1, C2, A2, B2 being Point of (TOP-REAL 2)
for lambda, mu, nu being Real st 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,C2 is_collinear & B,B1,C2 is_collinear & B,B1,A2 is_collinear & C,C1,A2 is_collinear & A,A1,B2 is_collinear & C,C1,B2 is_collinear holds
( (((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
let A, B, C, A1, B1, C1, C2, A2, B2 be Point of (TOP-REAL 2); ::_thesis: for lambda, mu, nu being Real st 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,C2 is_collinear & B,B1,C2 is_collinear & B,B1,A2 is_collinear & C,C1,A2 is_collinear & A,A1,B2 is_collinear & C,C1,B2 is_collinear holds
( (((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)) )
let lambda, mu, nu be Real; ::_thesis: ( 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,C2 is_collinear & B,B1,C2 is_collinear & B,B1,A2 is_collinear & C,C1,A2 is_collinear & A,A1,B2 is_collinear & C,C1,B2 is_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)) ) )
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,C2 is_collinear and
A9: B,B1,C2 is_collinear and
A10: B,B1,A2 is_collinear and
A11: C,C1,A2 is_collinear and
A12: A,A1,B2 is_collinear and
A13: C,C1,B2 is_collinear ; ::_thesis: ( (((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)) )
C2: C,A,B is_a_triangle by Th15, A1;
C3: B,C,A is_a_triangle by Th15, A1;
set q1 = (1 - mu) + (lambda * mu);
set q2 = (1 - lambda) + (nu * lambda);
set q3 = (1 - nu) + (mu * nu);
consider alpha being Real such that
B1: C2 = ((1 - alpha) * A) + (alpha * A1) and
B2: alpha = (1 - mu) / ((1 - mu) + (lambda * mu)) by Lm2, A1, A2, A3, A6, A8, A9;
B7: (1 - mu) + (lambda * mu) <> 0 by Lm2, A1, A2, A3, A6, A8, A9;
consider beta being Real such that
B3: B2 = ((1 - beta) * C) + (beta * C1) and
B4: beta = (1 - lambda) / ((1 - lambda) + (nu * lambda)) by Lm2, C2, A4, A2, A5, A13, A12;
B8: (1 - lambda) + (nu * lambda) <> 0 by Lm2, C2, A4, A2, A5, A13, A12;
consider gamma being Real such that
B5: A2 = ((1 - gamma) * B) + (gamma * B1) and
B6: gamma = (1 - nu) / ((1 - nu) + (mu * nu)) by Lm2, C3, A3, A4, A7, A10, A11;
B9: (1 - nu) + (mu * nu) <> 0 by Lm2, C3, A3, A4, A7, A10, A11;
 1 - alpha = ((1 * ((1 - mu) + (lambda * mu))) - (1 - mu)) / ((1 - mu) + (lambda * mu)) by B2, B7, XCMPLX_1:127;
then C4: 1 - alpha = (lambda * mu) * (1 / ((1 - mu) + (lambda * mu))) by XCMPLX_1:99;
 1 - beta = ((1 * ((1 - lambda) + (nu * lambda))) - (1 - lambda)) / ((1 - lambda) + (nu * lambda)) by B4, B8, XCMPLX_1:127;
then C5: 1 - beta = (nu * lambda) * (1 / ((1 - lambda) + (nu * lambda))) by XCMPLX_1:99;
 1 - gamma = ((1 * ((1 - nu) + (mu * nu))) - (1 - nu)) / ((1 - nu) + (mu * nu)) by B6, B9, XCMPLX_1:127;
then C6: 1 - gamma = (mu * nu) * (1 / ((1 - nu) + (mu * nu))) by XCMPLX_1:99;
C7: alpha = (1 - mu) * (1 / ((1 - mu) + (lambda * mu))) by B2, XCMPLX_1:99;
C8: beta = (1 - lambda) * (1 / ((1 - lambda) + (nu * lambda))) by B4, XCMPLX_1:99;
C9: gamma = (1 - nu) * (1 / ((1 - nu) + (mu * nu))) by B6, XCMPLX_1:99;
thus  (((1 - mu) + (lambda * mu)) * ((1 - lambda) + (nu * lambda))) * ((1 - nu) + (mu * nu)) <> 0 by B7, B8, B9; ::_thesis: 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))
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, B5
.= ((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 B3
.= (- ((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 B1
.= ((- ((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 B3
.= ((- ((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)) * (the_area_of_polygon3 (A,B,C))))) - (((gamma * (1 - mu)) * beta) * (the_area_of_polygon3 (C1,C,C2)))) - ((gamma * mu) * (the_area_of_polygon3 (C2,B2,A))) by B3
.= (((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)) * (the_area_of_polygon3 (A,B,C))))) - (((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) * (the_area_of_polygon3 (A,B,C))) + (beta * (((1 - nu) * (the_area_of_polygon3 (A,A,B))) + (nu * (the_area_of_polygon3 (B,A,B))))))) - ((((alpha * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C))))) - (((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)) * (the_area_of_polygon3 (A,B,C))) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C)))) - (((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)) * (the_area_of_polygon3 (A,B,C))) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C)))) - (((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 B1
.= ((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * (the_area_of_polygon3 (A,B,C))) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C)))) - (((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)) * (the_area_of_polygon3 (A,B,C))) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C)))) - (((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)) * (the_area_of_polygon3 (A,B,C))) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C)))) - (((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)) * (the_area_of_polygon3 (A,B,C))) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C)))) - (((gamma * (1 - mu)) * beta) * ((- ((((1 - nu) * alpha) * (1 - lambda)) * (the_area_of_polygon3 (A,B,C)))) + (nu * (((1 - alpha) * (the_area_of_polygon3 (A,B,C))) + (alpha * (the_area_of_polygon3 ((((1 - lambda) * B) + (lambda * C)),B,C)))))))) - ((gamma * mu) * (the_area_of_polygon3 (C2,B2,A))) by A2, Th7, B1
.= ((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * (the_area_of_polygon3 (A,B,C))) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C)))) - (((gamma * (1 - mu)) * beta) * ((- ((((1 - nu) * alpha) * (1 - lambda)) * (the_area_of_polygon3 (A,B,C)))) + (nu * (((1 - alpha) * (the_area_of_polygon3 (A,B,C))) + (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)) * (the_area_of_polygon3 (A,B,C))) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C)))) + (((((((gamma * (1 - mu)) * beta) * (1 - nu)) * alpha) * (1 - lambda)) * (the_area_of_polygon3 (A,B,C))) - (((((gamma * (1 - mu)) * beta) * nu) * (1 - alpha)) * (the_area_of_polygon3 (A,B,C))))) - ((gamma * mu) * (((1 - alpha) * (the_area_of_polygon3 (A,B2,A))) + (alpha * (the_area_of_polygon3 (A1,B2,A))))) by Th7, B1
.= ((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * (the_area_of_polygon3 (A,B,C))) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C)))) + (((((((gamma * (1 - mu)) * beta) * (1 - nu)) * alpha) * (1 - lambda)) * (the_area_of_polygon3 (A,B,C))) - (((((gamma * (1 - mu)) * beta) * nu) * (1 - alpha)) * (the_area_of_polygon3 (A,B,C))))) - (((gamma * mu) * alpha) * (the_area_of_polygon3 ((((1 - lambda) * B) + (lambda * C)),B2,A))) by A2
.= ((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * (the_area_of_polygon3 (A,B,C))) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C)))) + (((((((gamma * (1 - mu)) * beta) * (1 - nu)) * alpha) * (1 - lambda)) * (the_area_of_polygon3 (A,B,C))) - (((((gamma * (1 - mu)) * beta) * nu) * (1 - alpha)) * (the_area_of_polygon3 (A,B,C))))) - (((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)) * (the_area_of_polygon3 (A,B,C))) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C)))) + (((((((gamma * (1 - mu)) * beta) * (1 - nu)) * alpha) * (1 - lambda)) * (the_area_of_polygon3 (A,B,C))) - (((((gamma * (1 - mu)) * beta) * nu) * (1 - alpha)) * (the_area_of_polygon3 (A,B,C))))) - (((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 B3
.= ((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * (the_area_of_polygon3 (A,B,C))) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C)))) + (((((((gamma * (1 - mu)) * beta) * (1 - nu)) * alpha) * (1 - lambda)) * (the_area_of_polygon3 (A,B,C))) - (((((gamma * (1 - mu)) * beta) * nu) * (1 - alpha)) * (the_area_of_polygon3 (A,B,C))))) - (((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)) * (the_area_of_polygon3 (A,B,C))) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C)))) + (((((((gamma * (1 - mu)) * beta) * (1 - nu)) * alpha) * (1 - lambda)) * (the_area_of_polygon3 (A,B,C))) - (((((gamma * (1 - mu)) * beta) * nu) * (1 - alpha)) * (the_area_of_polygon3 (A,B,C))))) - (((gamma * mu) * alpha) * (((1 - lambda) * (((1 - beta) * (the_area_of_polygon3 (A,B,C))) + (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)) * (the_area_of_polygon3 (A,B,C))) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C)))) + (((((((gamma * (1 - mu)) * beta) * (1 - nu)) * alpha) * (1 - lambda)) * (the_area_of_polygon3 (A,B,C))) - (((((gamma * (1 - mu)) * beta) * nu) * (1 - alpha)) * (the_area_of_polygon3 (A,B,C))))) - (((gamma * mu) * alpha) * ((((1 - lambda) * (1 - beta)) * (the_area_of_polygon3 (A,B,C))) + (lambda * (((1 - beta) * (the_area_of_polygon3 (C,A,C))) + (beta * (the_area_of_polygon3 (C1,A,C))))))) by Th7, B3
.= ((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * (the_area_of_polygon3 (A,B,C))) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C)))) + (((((((gamma * (1 - mu)) * beta) * (1 - nu)) * alpha) * (1 - lambda)) * (the_area_of_polygon3 (A,B,C))) - (((((gamma * (1 - mu)) * beta) * nu) * (1 - alpha)) * (the_area_of_polygon3 (A,B,C))))) - (((gamma * mu) * alpha) * ((((1 - lambda) * (1 - beta)) * (the_area_of_polygon3 (A,B,C))) + ((lambda * beta) * (the_area_of_polygon3 ((((1 - nu) * A) + (nu * B)),A,C))))) by A4
.= ((((((1 - gamma) * (1 - alpha)) * (1 - beta)) * (the_area_of_polygon3 (A,B,C))) - ((((((1 - gamma) * alpha) * lambda) * beta) * (1 - nu)) * (the_area_of_polygon3 (A,B,C)))) + (((((((gamma * (1 - mu)) * beta) * (1 - nu)) * alpha) * (1 - lambda)) * (the_area_of_polygon3 (A,B,C))) - (((((gamma * (1 - mu)) * beta) * nu) * (1 - alpha)) * (the_area_of_polygon3 (A,B,C))))) - (((gamma * mu) * alpha) * ((((1 - lambda) * (1 - beta)) * (the_area_of_polygon3 (A,B,C))) + ((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)))) * (the_area_of_polygon3 (A,B,C))
.= (((((((mu * nu) * (1 / ((1 - nu) + (mu * nu)))) * ((lambda * mu) * (1 / ((1 - mu) + (lambda * mu))))) * ((nu * lambda) * (1 / ((1 - lambda) + (nu * lambda))))) - ((((((mu * nu) * (1 / ((1 - nu) + (mu * nu)))) * ((1 - mu) * (1 / ((1 - mu) + (lambda * mu))))) * lambda) * ((1 - lambda) * (1 / ((1 - lambda) + (nu * lambda))))) * (1 - nu))) + ((((((((1 - nu) * (1 / ((1 - nu) + (mu * nu)))) * (1 - mu)) * ((1 - lambda) * (1 / ((1 - lambda) + (nu * lambda))))) * (1 - nu)) * ((1 - mu) * (1 / ((1 - mu) + (lambda * mu))))) * (1 - lambda)) - ((((((1 - nu) * (1 / ((1 - nu) + (mu * nu)))) * (1 - mu)) * ((1 - lambda) * (1 / ((1 - lambda) + (nu * lambda))))) * nu) * ((lambda * mu) * (1 / ((1 - mu) + (lambda * mu))))))) + ((((((((1 - nu) * (1 / ((1 - nu) + (mu * nu)))) * mu) * ((1 - mu) * (1 / ((1 - mu) + (lambda * mu))))) * lambda) * ((1 - lambda) * (1 / ((1 - lambda) + (nu * lambda))))) * nu) - ((((((1 - nu) * (1 / ((1 - nu) + (mu * nu)))) * mu) * ((1 - mu) * (1 / ((1 - mu) + (lambda * mu))))) * (1 - lambda)) * ((nu * lambda) * (1 / ((1 - lambda) + (nu * lambda))))))) * (the_area_of_polygon3 (A,B,C)) by C4, C7, C5, C8, C6, C9
.= (((((mu * nu) * lambda) - (((1 - mu) * (1 - nu)) * (1 - lambda))) ^2) * (((1 / ((1 - mu) + (lambda * mu))) * (1 / ((1 - lambda) + (nu * lambda)))) * (1 / ((1 - nu) + (mu * nu))))) * (the_area_of_polygon3 (A,B,C))
.= (((((mu * nu) * lambda) - (((1 - mu) * (1 - nu)) * (1 - lambda))) ^2) * ((1 / (((1 - mu) + (lambda * mu)) * ((1 - lambda) + (nu * lambda)))) * (1 / ((1 - nu) + (mu * nu))))) * (the_area_of_polygon3 (A,B,C)) by XCMPLX_1:102
.= (((((mu * nu) * lambda) - (((1 - mu) * (1 - nu)) * (1 - lambda))) ^2) * (1 / ((((1 - mu) + (lambda * mu)) * ((1 - lambda) + (nu * lambda))) * ((1 - nu) + (mu * nu))))) * (the_area_of_polygon3 (A,B,C)) by XCMPLX_1:102 ;
hence  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 XCMPLX_1:99; ::_thesis: verum
end;

theorem :: MENELAUS:20
for A, B, C, A1, B1, C1, C2, A2, B2 being Point of (TOP-REAL 2) st 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,C2 is_collinear & B,B1,C2 is_collinear & B,B1,A2 is_collinear & C,C1,A2 is_collinear & A,A1,B2 is_collinear & C,C1,B2 is_collinear holds
the_area_of_polygon3 (A2,B2,C2) = (the_area_of_polygon3 (A,B,C)) / 7
proof
let A, B, C, A1, B1, C1, C2, A2, B2 be Point of (TOP-REAL 2); ::_thesis: ( 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,C2 is_collinear & B,B1,C2 is_collinear & B,B1,A2 is_collinear & C,C1,A2 is_collinear & A,A1,B2 is_collinear & C,C1,B2 is_collinear implies the_area_of_polygon3 (A2,B2,C2) = (the_area_of_polygon3 (A,B,C)) / 7 )
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,C2 is_collinear & B,B1,C2 is_collinear & B,B1,A2 is_collinear & C,C1,A2 is_collinear & A,A1,B2 is_collinear & C,C1,B2 is_collinear ) ; ::_thesis: the_area_of_polygon3 (A2,B2,C2) = (the_area_of_polygon3 (A,B,C)) / 7
 1 / 3 is Real by XREAL_0:def_1;
then consider lambda, mu, nu being Real such that
B1: ( 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, B1;
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 Th16, A1, A3;
hence  the_area_of_polygon3 (A2,B2,C2) = (the_area_of_polygon3 (A,B,C)) / 7 ; ::_thesis: verum
end;

Lm5:  for A, B, C, A1, B1, C1, C2, A2, B2 being Point of (TOP-REAL 2)
for lambda, mu, nu being Real st 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,C2 is_collinear & B,B1,C2 is_collinear & B,B1,A2 is_collinear & C,C1,A2 is_collinear & A,A1,B2 is_collinear & C,C1,B2 is_collinear holds
( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff A2,B2,C2 is_collinear )
proof
let A, B, C, A1, B1, C1, C2, A2, B2 be Point of (TOP-REAL 2); ::_thesis: for lambda, mu, nu being Real st 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,C2 is_collinear & B,B1,C2 is_collinear & B,B1,A2 is_collinear & C,C1,A2 is_collinear & A,A1,B2 is_collinear & C,C1,B2 is_collinear holds
( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff A2,B2,C2 is_collinear )
let lambda, mu, nu be Real; ::_thesis: ( 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,C2 is_collinear & B,B1,C2 is_collinear & B,B1,A2 is_collinear & C,C1,A2 is_collinear & A,A1,B2 is_collinear & C,C1,B2 is_collinear implies ( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff A2,B2,C2 is_collinear ) )
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,C2 is_collinear and
A9: B,B1,C2 is_collinear and
A10: B,B1,A2 is_collinear and
A11: C,C1,A2 is_collinear and
A12: A,A1,B2 is_collinear and
A13: C,C1,B2 is_collinear ; ::_thesis: ( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff A2,B2,C2 is_collinear )
set q = ((1 - lambda) * (1 - mu)) * (1 - nu);
B2: ( 0 = ((lambda * mu) * nu) - (((1 - lambda) * (1 - mu)) * (1 - nu)) iff ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 ) by Lm4, A5, A6, A7;
B1: ( (((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 Th16, A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, A11, A12, A13;
 the_area_of_polygon3 (A,B,C) <> 0 by Th9, A1;
hence  ( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff A2,B2,C2 is_collinear ) by B1, Th9, B2; ::_thesis: verum
end;

theorem Th19: :: MENELAUS:21
for A, B, C, A1, B1, C1 being Point of (TOP-REAL 2)
for lambda, mu, nu being Real st 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 holds
( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff ex A2 being Point of (TOP-REAL 2) st
( A,A1,A2 is_collinear & B,B1,A2 is_collinear & C,C1,A2 is_collinear ) )
proof
let A, B, C, A1, B1, C1 be Point of (TOP-REAL 2); ::_thesis: for lambda, mu, nu being Real st 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 holds
( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff ex A2 being Point of (TOP-REAL 2) st
( A,A1,A2 is_collinear & B,B1,A2 is_collinear & C,C1,A2 is_collinear ) )
let lambda, mu, nu be Real; ::_thesis: ( 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 being Point of (TOP-REAL 2) st
( A,A1,A2 is_collinear & B,B1,A2 is_collinear & C,C1,A2 is_collinear ) ) )
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: (1 - mu) + (lambda * mu) <> 0 and
A9: (1 - lambda) + (nu * lambda) <> 0 and
A10: (1 - nu) + (mu * nu) <> 0 ; ::_thesis: ( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff ex A2 being Point of (TOP-REAL 2) st
( A,A1,A2 is_collinear & B,B1,A2 is_collinear & C,C1,A2 is_collinear ) )
B2: C,A,B is_a_triangle by Th15, A1;
B3: B,C,A is_a_triangle by Th15, A1;
consider C2 being Point of (TOP-REAL 2) such that
B4: A,A1,C2 is_collinear and
B5: B,B1,C2 is_collinear by Lm3, A1, A2, A3, A8;
consider B2 being Point of (TOP-REAL 2) such that
B6: C,C1,B2 is_collinear and
B7: A,A1,B2 is_collinear by Lm3, B2, A4, A2, A9;
consider A2 being Point of (TOP-REAL 2) such that
B8: B,B1,A2 is_collinear and
B9: C,C1,A2 is_collinear by Lm3, B3, A3, A4, A10;
D1: A <> A1 by Th14, A1, A2;
 C2,A,A1 is_collinear by Th15, B4;
then D2: C2 in Line (A,A1) by D1, Th13;
 B2,A,A1 is_collinear by Th15, B7;
then D3: B2 in Line (A,A1) by D1, Th13;
hereby  ::_thesis: ( ex A2 being Point of (TOP-REAL 2) st
( A,A1,A2 is_collinear & B,B1,A2 is_collinear & C,C1,A2 is_collinear ) implies ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 )
assume C1: ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 ; ::_thesis: ex A2 being Point of (TOP-REAL 2) st
( A,A1,A2 is_collinear & B,B1,A2 is_collinear & C,C1,A2 is_collinear )
percases ( B2 <> C2 or B2 = C2 ) ;
supposeC2: B2 <> C2 ; ::_thesis: ex A2 being Point of (TOP-REAL 2) st
( A,A1,A2 is_collinear & B,B1,A2 is_collinear & C,C1,A2 is_collinear )
take A2 = A2; ::_thesis: ( A,A1,A2 is_collinear & B,B1,A2 is_collinear & C,C1,A2 is_collinear )
 A2,B2,C2 is_collinear by C1, Lm5, A1, A2, A3, A4, A5, A6, A7, B4, B5, B6, B7, B8, B9;
then C3: A2 in Line (B2,C2) by Th13, C2;
 Line (B2,C2) c= Line (A,A1) by EUCLID_4:42, D2, D3;
then  A2,A,A1 is_collinear by Th13, D1, C3;
hence  A,A1,A2 is_collinear by Th15; ::_thesis: ( B,B1,A2 is_collinear & C,C1,A2 is_collinear )
thus  ( B,B1,A2 is_collinear & C,C1,A2 is_collinear ) by B8, B9; ::_thesis: verum
end;
supposeC4: B2 = C2 ; ::_thesis: ex B2 being Point of (TOP-REAL 2) st
( A,A1,B2 is_collinear & B,B1,B2 is_collinear & C,C1,B2 is_collinear )
take B2 = B2; ::_thesis: ( A,A1,B2 is_collinear & B,B1,B2 is_collinear & C,C1,B2 is_collinear )
thus  ( A,A1,B2 is_collinear & B,B1,B2 is_collinear & C,C1,B2 is_collinear ) by C4, B5, B6, B7; ::_thesis: verum
end;
end;
end;
given C3 being Point of (TOP-REAL 2) such that C1: A,A1,C3 is_collinear and
C2: B,B1,C3 is_collinear and
C3: C,C1,C3 is_collinear ; ::_thesis: ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1
C4: C3,B2,C2 is_collinear
proof
percases ( B2 <> C2 or B2 = C2 ) ;
supposeC4: B2 <> C2 ; ::_thesis: C3,B2,C2 is_collinear
 C3,A,A1 is_collinear by Th15, C1;
then C5: C3 in Line (A,A1) by Th13, D1;
 Line (A,A1) c= Line (B2,C2) by EUCLID_4:43, D2, D3, C4;
hence  C3,B2,C2 is_collinear by C4, Th13, C5; ::_thesis: verum
end;
suppose B2 = C2 ; ::_thesis: C3,B2,C2 is_collinear
then  not C3,B2,C2 are_mutually_different by ZFMISC_1:def_5;
hence  C3,B2,C2 is_collinear by EUCLID_6:20; ::_thesis: verum
end;
end;
end;
 C3 = A2
proof
assume C5: C3 <> A2 ; ::_thesis: contradiction
 C,A,B is_a_triangle by Th15, A1;
then C7: C <> C1 by Th14, A4;
then C10: Line (C,C1) is being_line by EUCLID_4:def_4;
 B,C,A is_a_triangle by Th15, A1;
then C8: B <> B1 by Th14, A3;
then C9: Line (B,B1) is being_line by EUCLID_4:def_4;
 C3,B,B1 is_collinear by Th15, C2;
then H1: C3 in Line (B,B1) by Th13, C8;
 A2,B,B1 is_collinear by Th15, B8;
then H2: A2 in Line (B,B1) by Th13, C8;
 A2,C,C1 is_collinear by Th15, B9;
then H3: A2 in Line (C,C1) by Th13, C7;
 C3,C,C1 is_collinear by Th15, C3;
then  C3 in Line (C,C1) by Th13, C7;
then H4: Line (B,B1) = Line (C,C1) by EUCLID_4:44, H1, C5, H2, H3, C9, C10;
H5: 1 - nu <> 0 by A7;
 B in Line (B,B1) by EUCLID_4:41;
then  B,C,C1 is_collinear by Th13, C7, H4;
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 H5;
hence  contradiction by Th9, A1; ::_thesis: verum
end;
hence  ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 by C4, Lm5, A1, A2, A3, A4, A5, A6, A7, B4, B5, B6, B7, B8, B9; ::_thesis: verum
end;

theorem :: MENELAUS:22
for A, B, C, A1, B1, C1 being Point of (TOP-REAL 2)
for lambda, mu, nu being Real st 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 holds
( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff Line (A,A1), Line (B,B1), Line (C,C1) are_concurrent )
proof
let A, B, C, A1, B1, C1 be Point of (TOP-REAL 2); ::_thesis: for lambda, mu, nu being Real st 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 holds
( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff Line (A,A1), Line (B,B1), Line (C,C1) are_concurrent )
let lambda, mu, nu be Real; ::_thesis: ( 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 ) )
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 ; ::_thesis: ( ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 iff Line (A,A1), Line (B,B1), Line (C,C1) are_concurrent )
A8: A <> A1 by Th14, A1, A2;
A9: B,C,A is_a_triangle by Th15, A1;
then A10: B <> B1 by Th14, A3;
A11: C,A,B is_a_triangle by Th15, A1;
then A12: C <> C1 by Th14, A4;
hereby  ::_thesis: ( Line (A,A1), Line (B,B1), Line (C,C1) are_concurrent implies ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 )
assume B1: ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 ; ::_thesis: Line (A,A1), Line (B,B1), Line (C,C1) are_concurrent
percases ( ( (1 - mu) + (lambda * mu) <> 0 & (1 - lambda) + (nu * lambda) <> 0 & (1 - nu) + (mu * nu) <> 0 ) or not (1 - mu) + (lambda * mu) <> 0 or not (1 - lambda) + (nu * lambda) <> 0 or not (1 - nu) + (mu * nu) <> 0 ) ;
suppose ( (1 - mu) + (lambda * mu) <> 0 & (1 - lambda) + (nu * lambda) <> 0 & (1 - nu) + (mu * nu) <> 0 ) ; ::_thesis: Line (A,A1), Line (B,B1), Line (C,C1) are_concurrent
then consider A2 being Point of (TOP-REAL 2) such that
B2: ( A,A1,A2 is_collinear & B,B1,A2 is_collinear & C,C1,A2 is_collinear ) by B1, Th19, A1, A2, A3, A4, A5, A6, A7;
 ( A2,A,A1 is_collinear & A2,B,B1 is_collinear & A2,C,C1 is_collinear ) by Th15, B2;
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 by def2; ::_thesis: verum
end;
suppose ( not (1 - mu) + (lambda * mu) <> 0 or not (1 - lambda) + (nu * lambda) <> 0 or not (1 - nu) + (mu * nu) <> 0 ) ; ::_thesis: Line (A,A1), Line (B,B1), Line (C,C1) are_concurrent
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 B1, Lm7, A1, A2, A3, A4, A5, A6, A7;
hence  Line (A,A1), Line (B,B1), Line (C,C1) are_concurrent by def2; ::_thesis: verum
end;
end;
end;
assume  Line (A,A1), Line (B,B1), Line (C,C1) are_concurrent ; ::_thesis: ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1
percasesthen  ( ( 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) ) or ex C2 being Point of (TOP-REAL 2) st
( C2 in Line (A,A1) & C2 in Line (B,B1) & C2 in Line (C,C1) ) ) by def2;
supposeB1: ( 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) ) ; ::_thesis: ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1
then  ( (1 - mu) + (lambda * mu) = 0 & (1 - nu) + (mu * nu) = 0 & (1 - lambda) + (nu * lambda) = 0 ) by Th18, A1, A9, A11, A2, A3, A4, A5, A6, A7;
hence  ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 by Lm7, B1, A1, A2, A3, A4, A5, A6, A7; ::_thesis: verum
end;
suppose ex C2 being Point of (TOP-REAL 2) st
( C2 in Line (A,A1) & C2 in Line (B,B1) & C2 in Line (C,C1) ) ; ::_thesis: ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1
then consider C2 being Point of (TOP-REAL 2) such that
B2: ( 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 B2, XBOOLE_0:3;
then B3: ( (1 - mu) + (lambda * mu) <> 0 & (1 - nu) + (mu * nu) <> 0 & (1 - lambda) + (nu * lambda) <> 0 ) by Th18, A1, A2, A3, A4, A5, A6, A7, A9, A11;
 ( C2,A,A1 is_collinear & C2,B,B1 is_collinear & C2,C,C1 is_collinear ) by B2, Th13, A8, A10, A12;
then  ( A,A1,C2 is_collinear & B,B1,C2 is_collinear & C,C1,C2 is_collinear ) by Th15;
hence  ((lambda / (1 - lambda)) * (mu / (1 - mu))) * (nu / (1 - nu)) = 1 by B3, Th19, A1, A2, A3, A4, A5, A6, A7; ::_thesis: verum
end;
end;
end;