euclid_3.miz

begin

 reserve z,z1,z2 for Complex;

 reserve r,x1,x2 for Real;

 reserve p0,p,p1,p2,p3,q for Point of ( TOP-REAL 2);

 definition

 let z be Complex;

 :: EUCLID_3:def1

 func cpx2euc (z) -> Point of ( TOP-REAL 2) equals |[( Re z), ( Im z)]|;

 correctness ;

 end

 definition

 let p be Point of ( TOP-REAL 2);

 :: EUCLID_3:def2

 func euc2cpx (p) -> Element of COMPLEX equals ((p `1 ) + ((p `2 ) * ));

 correctness by XCMPLX_0:def 2;

 end

 theorem :: EUCLID_3:1



 Th1: ( euc2cpx ( cpx2euc z)) = z

 proof

 ( |[( Re z), ( Im z)]| `1 ) = ( Re z) & ( |[( Re z), ( Im z)]| `2 ) = ( Im z) by EUCLID: 52;

 hence thesis by COMPLEX1: 13;

 end;

 theorem :: EUCLID_3:2



 Th2: ( cpx2euc ( euc2cpx p)) = p

 proof

 ( Re ((p `1 ) + ((p `2 ) * ))) = (p `1 ) & ( Im ((p `1 ) + ((p `2 ) * ))) = (p `2 ) by COMPLEX1: 12;

 hence thesis by EUCLID: 53;

 end;

 theorem :: EUCLID_3:3

 for z1, z2 st ( cpx2euc z1) = ( cpx2euc z2) holds z1 = z2

 proof

 let z1, z2;

 assume

 A1: ( cpx2euc z1) = ( cpx2euc z2);

 z2 = ( euc2cpx ( cpx2euc z2)) by Th1;

 hence thesis by A1, Th1;

 end;

 theorem :: EUCLID_3:4



 Th4: for p1, p2 st ( euc2cpx p1) = ( euc2cpx p2) holds p1 = p2

 proof

 let p1, p2;

 assume

 A1: ( euc2cpx p1) = ( euc2cpx p2);

 p2 = ( cpx2euc ( euc2cpx p2)) by Th2;

 hence thesis by A1, Th2;

 end;

 theorem :: EUCLID_3:5



 Th5: ( cpx2euc (x1 + (x2 * ))) = |[x1, x2]|

 proof

 ( Re (x1 + (x2 * ))) = x1 by COMPLEX1: 12;

 hence thesis by COMPLEX1: 12;

 end;

 theorem :: EUCLID_3:6



 Th6: |[( Re (z1 + z2)), ( Im (z1 + z2))]| = |[(( Re z1) + ( Re z2)), (( Im z1) + ( Im z2))]|

 proof

 ( |[( Re (z1 + z2)), ( Im (z1 + z2))]| `2 ) = ( Im (z1 + z2)) by EUCLID: 52;

 then

 A1: ( |[( Re (z1 + z2)), ( Im (z1 + z2))]| `2 ) = (( Im z1) + ( Im z2)) by COMPLEX1: 8;

 ( |[( Re (z1 + z2)), ( Im (z1 + z2))]| `1 ) = ( Re (z1 + z2)) by EUCLID: 52;

 then ( |[( Re (z1 + z2)), ( Im (z1 + z2))]| `1 ) = (( Re z1) + ( Re z2)) by COMPLEX1: 8;

 hence thesis by A1, EUCLID: 53;

 end;

 theorem :: EUCLID_3:7



 Th7: ( cpx2euc (z1 + z2)) = (( cpx2euc z1) + ( cpx2euc z2))

 proof

 (( cpx2euc z1) + ( cpx2euc z2)) = |[(( Re z1) + ( Re z2)), (( Im z1) + ( Im z2))]| by EUCLID: 56;

 hence thesis by Th6;

 end;

 theorem :: EUCLID_3:8



 Th8: (((p1 + p2) `1 ) + (((p1 + p2) `2 ) * )) = (((p1 `1 ) + (p2 `1 )) + (((p1 `2 ) + (p2 `2 )) * ))

 proof



 A1: (p1 + p2) = |[((p1 `1 ) + (p2 `1 )), ((p1 `2 ) + (p2 `2 ))]| by EUCLID: 55;



 A2: ( Im (((p1 `1 ) + (p2 `1 )) + (((p1 `2 ) + (p2 `2 )) * ))) = ((p1 `2 ) + (p2 `2 )) by COMPLEX1: 12;



 A3: ( Im (((p1 + p2) `1 ) + (((p1 + p2) `2 ) * ))) = ((p1 + p2) `2 ) & ( Re (((p1 `1 ) + (p2 `1 )) + (((p1 `2 ) + (p2 `2 )) * ))) = ((p1 `1 ) + (p2 `1 )) by COMPLEX1: 12;

 ( Re (((p1 + p2) `1 ) + (((p1 + p2) `2 ) * ))) = ((p1 + p2) `1 ) by COMPLEX1: 12;

 then ( Re (((p1 + p2) `1 ) + (((p1 + p2) `2 ) * ))) = ((p1 `1 ) + (p2 `1 )) by A1, EUCLID: 52;

 hence thesis by A1, A3, A2, EUCLID: 52;

 end;

 theorem :: EUCLID_3:9



 Th9: ( euc2cpx (p1 + p2)) = (( euc2cpx p1) + ( euc2cpx p2))

 proof

 ( euc2cpx (p1 + p2)) = (((p1 `1 ) + (p2 `1 )) + (((p1 `2 ) + (p2 `2 )) * )) by Th8;

 hence thesis;

 end;

 theorem :: EUCLID_3:10



 Th10: |[( Re ( - z)), ( Im ( - z))]| = |[( - ( Re z)), ( - ( Im z))]|

 proof

 ( |[( Re ( - z)), ( Im ( - z))]| `2 ) = ( Im ( - z)) by EUCLID: 52;

 then

 A1: ( |[( Re ( - z)), ( Im ( - z))]| `2 ) = ( - ( Im z)) by COMPLEX1: 17;

 ( |[( Re ( - z)), ( Im ( - z))]| `1 ) = ( Re ( - z)) by EUCLID: 52;

 then ( |[( Re ( - z)), ( Im ( - z))]| `1 ) = ( - ( Re z)) by COMPLEX1: 17;

 hence thesis by A1, EUCLID: 53;

 end;

 theorem :: EUCLID_3:11



 Th11: ( cpx2euc ( - z)) = ( - ( cpx2euc z))

 proof

 ( - ( cpx2euc z)) = |[( - ( Re z)), ( - ( Im z))]| by EUCLID: 60;

 hence thesis by Th10;

 end;

 theorem :: EUCLID_3:12



 Th12: ((( - p) `1 ) + ((( - p) `2 ) * )) = (( - (p `1 )) + (( - (p `2 )) * ))

 proof



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

 (( - (p `1 )) + (( - (p `2 )) * )) = (( - (p `1 )) + (( - (p `2 )) * ));

 then

 A2: ( Re (( - (p `1 )) + ( - ((p `2 ) * )))) = ( - (p `1 )) & ( Im (( - (p `1 )) + ( - ((p `2 ) * )))) = ( - (p `2 )) by COMPLEX1: 12;

 ( Re ((( - p) `1 ) + ((( - p) `2 ) * ))) = (( - p) `1 ) by COMPLEX1: 12;

 then ( Im ((( - p) `1 ) + ((( - p) `2 ) * ))) = (( - p) `2 ) & ( Re ((( - p) `1 ) + ((( - p) `2 ) * ))) = ( - (p `1 )) by A1, COMPLEX1: 12, EUCLID: 52;

 hence thesis by A1, A2, EUCLID: 52;

 end;

 theorem :: EUCLID_3:13



 Th13: ( euc2cpx ( - p)) = ( - ( euc2cpx p))

 proof

 ( - ( euc2cpx p)) = (( - (p `1 )) + (( - (p `2 )) * ));

 hence thesis by Th12;

 end;

 theorem :: EUCLID_3:14

 ( cpx2euc (z1 - z2)) = (( cpx2euc z1) - ( cpx2euc z2))

 proof



 thus ( cpx2euc (z1 - z2)) = ( cpx2euc (z1 + ( - z2)))

 .= (( cpx2euc z1) + ( cpx2euc ( - z2))) by Th7

 .= (( cpx2euc z1) - ( cpx2euc z2)) by Th11;

 end;

 theorem :: EUCLID_3:15



 Th15: ( euc2cpx (p1 - p2)) = (( euc2cpx p1) - ( euc2cpx p2))

 proof



 thus ( euc2cpx (p1 - p2)) = (( euc2cpx p1) + ( euc2cpx ( - p2))) by Th9

 .= (( euc2cpx p1) + ( - ( euc2cpx p2))) by Th13

 .= (( euc2cpx p1) - ( euc2cpx p2));

 end;

 theorem :: EUCLID_3:16



 Th16: ( cpx2euc 0c ) = ( 0. ( TOP-REAL 2)) by COMPLEX1: 4, EUCLID: 54;

 theorem :: EUCLID_3:17



 Th17: ( euc2cpx ( 0. ( TOP-REAL 2))) = 0c by Th1, Th16;

 theorem :: EUCLID_3:18

 ( euc2cpx p) = 0c implies p = ( 0. ( TOP-REAL 2)) by Th2, Th16;

 theorem :: EUCLID_3:19

 ( cpx2euc (r * z)) = (r * ( cpx2euc z))

 proof



 A1: (( cpx2euc z) `1 ) = ( Re z) & (( cpx2euc z) `2 ) = ( Im z) by EUCLID: 52;

 r = (r + ( 0 * ));

 then

 A2: ( Re r) = r & ( Im r) = 0 by COMPLEX1: 12;



 then

 A3: ( Im (r * z)) = ((r * ( Im z)) + ( 0 * ( Re z))) by COMPLEX1: 9

 .= (r * ( Im z));

 ( Re (r * z)) = ((r * ( Re z)) - ( 0 * ( Im z))) by A2, COMPLEX1: 9

 .= (r * ( Re z));

 hence thesis by A3, A1, EUCLID: 57;

 end;

 theorem :: EUCLID_3:20

 ( euc2cpx (r * p)) = (r * ( euc2cpx p))

 proof

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

 then ((r * p) `1 ) = (r * (p `1 )) & ((r * p) `2 ) = (r * (p `2 )) by EUCLID: 52;

 hence thesis;

 end;

 theorem :: EUCLID_3:21



 Th21: |.( euc2cpx p).| = ( sqrt (((p `1 ) ^2 ) + ((p `2 ) ^2 )))

 proof

 ( Re ( euc2cpx p)) = (p `1 ) by COMPLEX1: 12;

 hence thesis by COMPLEX1: 12;

 end;

 theorem :: EUCLID_3:22

 for f be FinSequence of REAL st ( len f) = 2 holds |.f.| = ( sqrt (((f . 1) ^2 ) + ((f . 2) ^2 )))

 proof

 let f be FinSequence of REAL ;



 A1: (( sqr f) . 1) = ((f . 1) ^2 ) & (( sqr f) . 2) = ((f . 2) ^2 ) by VALUED_1: 11;

 ( dom ( sqr f)) = ( dom f) & ( Seg ( len ( sqr f))) = ( dom ( sqr f)) by FINSEQ_1:def 3, VALUED_1: 11;

 then

 A2: ( len ( sqr f)) = ( len f) by FINSEQ_1:def 3;

 reconsider f1 = ((f . 1) ^2 ), f2 = ((f . 2) ^2 ) as Element of REAL by XREAL_0:def 1;

 assume ( len f) = 2;

 then ( sqr f) = <*((f . 1) ^2 ), ((f . 2) ^2 )*> by A1, A2, FINSEQ_1: 44;



 then ( Sum ( sqr f)) = ( Sum ( <*f1*> ^ <*f2*>)) by FINSEQ_1:def 9

 .= (( Sum <*f1*>) + ((f . 2) ^2 )) by RVSUM_1: 74

 .= (((f . 1) ^2 ) + ((f . 2) ^2 )) by RVSUM_1: 73;

 hence thesis;

 end;

 theorem :: EUCLID_3:23

 for f be FinSequence of REAL , p be Point of ( TOP-REAL 2) st ( len f) = 2 & p = f holds |.p.| = |.f.|;

 theorem :: EUCLID_3:24

 |.( cpx2euc z).| = ( sqrt ((( Re z) ^2 ) + (( Im z) ^2 )))

 proof

 ( |[( Re z), ( Im z)]| `1 ) = ( Re z) & ( |[( Re z), ( Im z)]| `2 ) = ( Im z) by EUCLID: 52;

 hence thesis by JGRAPH_3: 1;

 end;

 theorem :: EUCLID_3:25



 Th25: |.( euc2cpx p).| = |.p.|

 proof

 |.p.| = ( sqrt (((p `1 ) ^2 ) + ((p `2 ) ^2 ))) by JGRAPH_3: 1;

 hence thesis by Th21;

 end;

 definition

 let p;

 :: EUCLID_3:def3

 func Arg (p) -> Real equals ( Arg ( euc2cpx p));

 correctness ;

 end

 theorem :: EUCLID_3:26

 for z be Element of COMPLEX , p st z = ( euc2cpx p) or p = ( cpx2euc z) holds ( Arg z) = ( Arg p)

 proof

 let z be Element of COMPLEX , p;

 assume

 A1: z = ( euc2cpx p) or p = ( cpx2euc z);

 per cases by A1;

 suppose z = ( euc2cpx p);

 hence thesis;

 end;

 suppose p = ( cpx2euc z);

 hence thesis by Th1;

 end;

 end;

 theorem :: EUCLID_3:27

 for x1,x2 be Real, p st x1 = ( |.p.| * ( cos ( Arg p))) & x2 = ( |.p.| * ( sin ( Arg p))) holds p = |[x1, x2]|

 proof

 let x1,x2 be Real, p;

 assume x1 = ( |.p.| * ( cos ( Arg p))) & x2 = ( |.p.| * ( sin ( Arg p)));

 then x1 = ( |.( euc2cpx p).| * ( cos ( Arg ( euc2cpx p)))) & x2 = ( |.( euc2cpx p).| * ( sin ( Arg ( euc2cpx p)))) by Th25;

 then ( euc2cpx p) = (x1 + (x2 * )) by COMPTRIG: 62;

 then p = ( cpx2euc (x1 + (x2 * ))) by Th2;

 hence thesis by Th5;

 end;

 theorem :: EUCLID_3:28

 ( Arg ( 0. ( TOP-REAL 2))) = 0 by Th17, COMPTRIG: 35;

 theorem :: EUCLID_3:29

 for p st p <> ( 0. ( TOP-REAL 2)) holds (( Arg p) < PI implies ( Arg ( - p)) = (( Arg p) + PI )) & (( Arg p) >= PI implies ( Arg ( - p)) = (( Arg p) - PI ))

 proof

 let p;

 assume p <> ( 0. ( TOP-REAL 2));

 then

 A1: ( euc2cpx p) <> 0c by Th2, Th16;

 ( Arg ( - p)) = ( Arg ( - ( euc2cpx p))) by Th13;

 hence thesis by A1, COMPLEX2: 13;

 end;

 theorem :: EUCLID_3:30

 for p st ( Arg p) = 0 holds p = |[ |.p.|, 0 ]| & (p `2 ) = 0

 proof

 let p;

 assume ( Arg p) = 0 ;

 then

 A1: ( euc2cpx p) = ( |.( euc2cpx p).| + ( 0 * )) & ( Im ( euc2cpx p)) = 0 by COMPLEX2: 15, COMPLEX2: 21;

 ( cpx2euc ( |.( euc2cpx p).| + ( 0 * ))) = |[ |.( euc2cpx p).|, 0 ]| & |.( euc2cpx p).| = |.p.| by Th5, Th25;

 hence thesis by A1, Th2, COMPLEX1: 12;

 end;

 theorem :: EUCLID_3:31



 Th31: for p st p <> ( 0. ( TOP-REAL 2)) holds (( Arg p) < PI iff ( Arg ( - p)) >= PI )

 proof

 let p;

 assume p <> ( 0. ( TOP-REAL 2));

 then

 A1: ( euc2cpx p) <> 0c by Th2, Th16;

 ( Arg ( - p)) = ( Arg ( - ( euc2cpx p))) by Th13;

 hence thesis by A1, COMPLEX2: 16;

 end;

 theorem :: EUCLID_3:32

 for p1, p2 st p1 <> p2 or (p1 - p2) <> ( 0. ( TOP-REAL 2)) holds (( Arg (p1 - p2)) < PI iff ( Arg (p2 - p1)) >= PI )

 proof

 let p1, p2;

 assume p1 <> p2 or (p1 - p2) <> ( 0. ( TOP-REAL 2));

 then

 A1: (p1 - p2) <> ( 0. ( TOP-REAL 2)) by RLVECT_1: 21;

 ( - (p1 - p2)) = (p2 - p1) by RLVECT_1: 33;

 hence thesis by A1, Th31;

 end;

 theorem :: EUCLID_3:33

 for p holds ( Arg p) in ]. 0 , PI .[ iff (p `2 ) > 0

 proof

 let p;

 ( Im ( euc2cpx p)) = (p `2 ) by COMPLEX1: 12;

 hence thesis by COMPLEX2: 18;

 end;

 theorem :: EUCLID_3:34

 for p1, p2 st ( Arg p1) < PI & ( Arg p2) < PI holds ( Arg (p1 + p2)) < PI

 proof

 let p1, p2;

 assume ( Arg p1) < PI & ( Arg p2) < PI ;

 then ( Arg (( euc2cpx p1) + ( euc2cpx p2))) < PI by COMPLEX2: 20;

 hence thesis by Th9;

 end;

 definition

 let p1, p2, p3;

 :: EUCLID_3:def4

 func angle (p1,p2,p3) -> Real equals ( angle (( euc2cpx p1),( euc2cpx p2),( euc2cpx p3)));

 correctness ;

 end

 theorem :: EUCLID_3:35

 for p1, p2, p3 holds ( angle (p1,p2,p3)) = ( angle ((p1 - p2),( 0. ( TOP-REAL 2)),(p3 - p2)))

 proof

 let p1, p2, p3;

 (( euc2cpx p1) - ( euc2cpx p2)) = ( euc2cpx (p1 - p2)) & (( euc2cpx p3) - ( euc2cpx p2)) = ( euc2cpx (p3 - p2)) by Th15;

 hence thesis by Th17, COMPLEX2: 71;

 end;

 theorem :: EUCLID_3:36

 for p1, p2, p3 st ( angle (p1,p2,p3)) = 0 holds ( Arg (p1 - p2)) = ( Arg (p3 - p2)) & ( angle (p3,p2,p1)) = 0

 proof

 let p1, p2, p3;

 assume

 A1: ( angle (p1,p2,p3)) = 0 ;

 (( euc2cpx p1) - ( euc2cpx p2)) = ( euc2cpx (p1 - p2)) & (( euc2cpx p3) - ( euc2cpx p2)) = ( euc2cpx (p3 - p2)) by Th15;

 hence thesis by A1, COMPLEX2: 74;

 end;

 theorem :: EUCLID_3:37

 for p1, p2, p3 st ( angle (p1,p2,p3)) <> 0 holds ( angle (p3,p2,p1)) = ((2 * PI ) - ( angle (p1,p2,p3)))

 proof

 let p1, p2, p3;

 assume ( angle (p1,p2,p3)) <> 0 ;

 then (( angle (p3,p2,p1)) + ( angle (p1,p2,p3))) = (2 * PI ) by COMPLEX2: 80;

 hence thesis;

 end;

 theorem :: EUCLID_3:38

 for p1, p2, p3 st ( angle (p3,p2,p1)) <> 0 holds ( angle (p3,p2,p1)) = ((2 * PI ) - ( angle (p1,p2,p3)))

 proof

 let p1, p2, p3;

 assume ( angle (p3,p2,p1)) <> 0 ;

 then (( angle (p3,p2,p1)) + ( angle (p1,p2,p3))) = (2 * PI ) by COMPLEX2: 80;

 hence thesis;

 end;

 theorem :: EUCLID_3:39



 Th39: for x,y be Element of COMPLEX holds ( Re (x .|. y)) = ((( Re x) * ( Re y)) + (( Im x) * ( Im y)))

 proof

 let x,y be Element of COMPLEX ;

 (x .|. y) = (((( Re x) * ( Re y)) + (( Im x) * ( Im y))) + ((( - (( Re x) * ( Im y))) + (( Im x) * ( Re y))) * )) by COMPLEX2: 29;

 hence thesis by COMPLEX1: 12;

 end;

 theorem :: EUCLID_3:40



 Th40: for x,y be Element of COMPLEX holds ( Im (x .|. y)) = (( - (( Re x) * ( Im y))) + (( Im x) * ( Re y)))

 proof

 let x,y be Element of COMPLEX ;

 (x .|. y) = (((( Re x) * ( Re y)) + (( Im x) * ( Im y))) + ((( - (( Re x) * ( Im y))) + (( Im x) * ( Re y))) * )) by COMPLEX2: 29;

 hence thesis by COMPLEX1: 12;

 end;

 theorem :: EUCLID_3:41



 Th41: for p, q holds |(p, q)| = (((p `1 ) * (q `1 )) + ((p `2 ) * (q `2 )))

 proof

 let p, q;

 ((p + q) `1 ) = ((p `1 ) + (q `1 )) by TOPREAL3: 2;

 then

 A1: (((p + q) `1 ) ^2 ) = ((((p `1 ) ^2 ) + ((2 * (p `1 )) * (q `1 ))) + ((q `1 ) ^2 )) by SQUARE_1: 4;

 ((p + q) `2 ) = ((p `2 ) + (q `2 )) by TOPREAL3: 2;

 then

 A2: (((p + q) `2 ) ^2 ) = ((((p `2 ) ^2 ) + ((2 * (p `2 )) * (q `2 ))) + ((q `2 ) ^2 )) by SQUARE_1: 4;

 ((p - q) `2 ) = ((p `2 ) - (q `2 )) by TOPREAL3: 3;

 then

 A3: (((p - q) `2 ) ^2 ) = ((((p `2 ) ^2 ) - ((2 * (p `2 )) * (q `2 ))) + ((q `2 ) ^2 )) by SQUARE_1: 5;

 ((p - q) `1 ) = ((p `1 ) - (q `1 )) by TOPREAL3: 3;

 then

 A4: (((p - q) `1 ) ^2 ) = ((((p `1 ) ^2 ) - ((2 * (p `1 )) * (q `1 ))) + ((q `1 ) ^2 )) by SQUARE_1: 5;

 |(p, q)| = ((1 / 4) * (( |.(p + q).| ^2 ) - ( |.(p - q).| ^2 ))) by EUCLID_2: 49

 .= ((1 / 4) * (((((p + q) `1 ) ^2 ) + (((p + q) `2 ) ^2 )) - ( |.(p - q).| ^2 ))) by JGRAPH_3: 1

 .= ((1 / 4) * (((((p + q) `1 ) ^2 ) + (((p + q) `2 ) ^2 )) - ((((p - q) `1 ) ^2 ) + (((p - q) `2 ) ^2 )))) by JGRAPH_3: 1

 .= ((1 / 4) * (((((p + q) `1 ) ^2 ) - (((p - q) `1 ) ^2 )) + ((((p + q) `2 ) ^2 ) - (((p - q) `2 ) ^2 ))));

 hence thesis by A1, A2, A4, A3;

 end;

 theorem :: EUCLID_3:42



 Th42: for p1, p2 holds |(p1, p2)| = ( Re (( euc2cpx p1) .|. ( euc2cpx p2)))

 proof

 let p1, p2;



 A1: (p1 `1 ) = ( Re ( euc2cpx p1)) & (p1 `2 ) = ( Im ( euc2cpx p1)) by COMPLEX1: 12;



 A2: (p2 `1 ) = ( Re ( euc2cpx p2)) & (p2 `2 ) = ( Im ( euc2cpx p2)) by COMPLEX1: 12;



 thus |(p1, p2)| = (((p1 `1 ) * (p2 `1 )) + ((p1 `2 ) * (p2 `2 ))) by Th41

 .= ( Re (( euc2cpx p1) .|. ( euc2cpx p2))) by A1, A2, Th39;

 end;

 theorem :: EUCLID_3:43

 for p1, p2, p3 st p1 <> ( 0. ( TOP-REAL 2)) & p2 <> ( 0. ( TOP-REAL 2)) holds ( |(p1, p2)| = 0 iff ( angle (p1,( 0. ( TOP-REAL 2)),p2)) = ( PI / 2) or ( angle (p1,( 0. ( TOP-REAL 2)),p2)) = ((3 / 2) * PI ))

 proof

 let p1, p2, p3;

 assume p1 <> ( 0. ( TOP-REAL 2)) & p2 <> ( 0. ( TOP-REAL 2));

 then

 A1: ( euc2cpx p1) <> 0c & ( euc2cpx p2) <> 0c by Th2, Th16;

 |(p1, p2)| = ( Re (( euc2cpx p1) .|. ( euc2cpx p2))) by Th42;

 hence thesis by A1, Th17, COMPLEX2: 75;

 end;

 theorem :: EUCLID_3:44

 for p1, p2 st p1 <> ( 0. ( TOP-REAL 2)) & p2 <> ( 0. ( TOP-REAL 2)) holds ((( - ((p1 `1 ) * (p2 `2 ))) + ((p1 `2 ) * (p2 `1 ))) = ( |.p1.| * |.p2.|) or (( - ((p1 `1 ) * (p2 `2 ))) + ((p1 `2 ) * (p2 `1 ))) = ( - ( |.p1.| * |.p2.|)) iff ( angle (p1,( 0. ( TOP-REAL 2)),p2)) = ( PI / 2) or ( angle (p1,( 0. ( TOP-REAL 2)),p2)) = ((3 / 2) * PI ))

 proof

 let p1, p2;



 A1: (p2 `1 ) = ( Re ( euc2cpx p2)) & (p2 `2 ) = ( Im ( euc2cpx p2)) by COMPLEX1: 12;

 (p1 `1 ) = ( Re ( euc2cpx p1)) & (p1 `2 ) = ( Im ( euc2cpx p1)) by COMPLEX1: 12;

 then

 A2: ( Im (( euc2cpx p1) .|. ( euc2cpx p2))) = (( - ((p1 `1 ) * (p2 `2 ))) + ((p1 `2 ) * (p2 `1 ))) by A1, Th40;

 assume p1 <> ( 0. ( TOP-REAL 2)) & p2 <> ( 0. ( TOP-REAL 2));

 then

 A3: ( euc2cpx p1) <> 0c & ( euc2cpx p2) <> 0c by Th2, Th16;

 |.( euc2cpx p1).| = |.p1.| & |.( euc2cpx p2).| = |.p2.| by Th25;

 hence thesis by A3, A2, Th17, COMPLEX2: 76;

 end;

 theorem :: EUCLID_3:45

 for p1, p2, p3 st p1 <> p2 & p3 <> p2 holds ( |((p1 - p2), (p3 - p2))| = 0 iff ( angle (p1,p2,p3)) = ( PI / 2) or ( angle (p1,p2,p3)) = ((3 / 2) * PI ))

 proof

 let p1, p2, p3;

 assume that

 A1: p1 <> p2 and

 A2: p3 <> p2;

 (p1 - p2) <> ( 0. ( TOP-REAL 2)) by A1, RLVECT_1: 21;

 then

 A3: ( euc2cpx (p1 - p2)) <> 0c by Th2, Th16;

 (p3 - p2) <> ( 0. ( TOP-REAL 2)) by A2, RLVECT_1: 21;

 then

 A4: ( euc2cpx (p3 - p2)) <> 0c by Th2, Th16;



 A5: (( euc2cpx p1) - ( euc2cpx p2)) = ( euc2cpx (p1 - p2)) & (( euc2cpx p3) - ( euc2cpx p2)) = ( euc2cpx (p3 - p2)) by Th15;

 hereby

 assume |((p1 - p2), (p3 - p2))| = 0 ;

 then ( Re (( euc2cpx (p1 - p2)) .|. ( euc2cpx (p3 - p2)))) = 0 by Th42;

 then ( angle (( euc2cpx (p1 - p2)), 0c ,( euc2cpx (p3 - p2)))) = ( PI / 2) or ( angle (( euc2cpx (p1 - p2)), 0c ,( euc2cpx (p3 - p2)))) = ((3 / 2) * PI ) by A3, A4, COMPLEX2: 75;

 hence ( angle (p1,p2,p3)) = ( PI / 2) or ( angle (p1,p2,p3)) = ((3 / 2) * PI ) by A5, COMPLEX2: 71;

 end;



 A6: |((p1 - p2), (p3 - p2))| = ( Re (( euc2cpx (p1 - p2)) .|. ( euc2cpx (p3 - p2)))) by Th42;

 assume ( angle (p1,p2,p3)) = ( PI / 2) or ( angle (p1,p2,p3)) = ((3 / 2) * PI );

 then ( angle (( euc2cpx (p1 - p2)), 0c ,( euc2cpx (p3 - p2)))) = ( PI / 2) or ( angle (( euc2cpx (p1 - p2)), 0c ,( euc2cpx (p3 - p2)))) = ((3 / 2) * PI ) by A5, COMPLEX2: 71;

 hence thesis by A6, A3, A4, COMPLEX2: 75;

 end;

 ::$Notion-Name

 theorem :: EUCLID_3:46

 for p1, p2, p3 st p1 <> p2 & p3 <> p2 & (( angle (p1,p2,p3)) = ( PI / 2) or ( angle (p1,p2,p3)) = ((3 / 2) * PI )) holds (( |.(p1 - p2).| ^2 ) + ( |.(p3 - p2).| ^2 )) = ( |.(p1 - p3).| ^2 )

 proof

 let p1, p2, p3;

 assume that

 A1: p1 <> p2 & p3 <> p2 and

 A2: ( angle (p1,p2,p3)) = ( PI / 2) or ( angle (p1,p2,p3)) = ((3 / 2) * PI );



 A3: (( euc2cpx p1) - ( euc2cpx p2)) = ( euc2cpx (p1 - p2)) & (( euc2cpx p3) - ( euc2cpx p2)) = ( euc2cpx (p3 - p2)) by Th15;



 A4: (( euc2cpx p1) - ( euc2cpx p3)) = ( euc2cpx (p1 - p3)) & |.( euc2cpx (p1 - p2)).| = |.(p1 - p2).| by Th15, Th25;



 A5: |.( euc2cpx (p3 - p2)).| = |.(p3 - p2).| & |.( euc2cpx (p1 - p3)).| = |.(p1 - p3).| by Th25;

 ( euc2cpx p1) <> ( euc2cpx p2) & ( euc2cpx p3) <> ( euc2cpx p2) by A1, Th4;

 hence thesis by A2, A3, A4, A5, COMPLEX2: 77;

 end;

 theorem :: EUCLID_3:47

 for p1, p2, p3 st p2 <> p1 & p1 <> p3 & p3 <> p2 & ( angle (p2,p1,p3)) < PI holds ((( angle (p2,p1,p3)) + ( angle (p1,p3,p2))) + ( angle (p3,p2,p1))) = PI

 proof

 let p1, p2, p3;

 assume that

 A1: p2 <> p1 & p1 <> p3 and

 A2: p3 <> p2 and

 A3: ( angle (p2,p1,p3)) < PI ;



 A4: ( euc2cpx p1) <> ( euc2cpx p2) & ( euc2cpx p1) <> ( euc2cpx p3) by A1, Th4;



 A5: ( euc2cpx p3) <> ( euc2cpx p2) by A2, Th4;

 per cases by COMPLEX2: 70;

 suppose

 A6: 0 = ( angle (( euc2cpx p2),( euc2cpx p1),( euc2cpx p3)));

 now

 per cases by A4, A5, A6, COMPLEX2: 87;

 suppose ( angle (( euc2cpx p1),( euc2cpx p3),( euc2cpx p2))) = 0 & ( angle (( euc2cpx p3),( euc2cpx p2),( euc2cpx p1))) = PI ;

 hence thesis by A6;

 end;

 suppose ( angle (( euc2cpx p1),( euc2cpx p3),( euc2cpx p2))) = PI & ( angle (( euc2cpx p3),( euc2cpx p2),( euc2cpx p1))) = 0 ;

 hence thesis by A6;

 end;

 end;

 hence thesis;

 end;

 suppose 0 < ( angle (( euc2cpx p2),( euc2cpx p1),( euc2cpx p3)));

 hence thesis by A3, A4, COMPLEX2: 84;

 end;

 end;

 definition

 let n be Element of NAT , p1,p2,p3 be Point of ( TOP-REAL n);

 :: EUCLID_3:def5

 func Triangle (p1,p2,p3) -> Subset of ( TOP-REAL n) equals ((( LSeg (p1,p2)) \/ ( LSeg (p2,p3))) \/ ( LSeg (p3,p1)));

 correctness ;

 end

 definition

 let n be Element of NAT , p1,p2,p3 be Point of ( TOP-REAL n);

 :: EUCLID_3:def6

 func closed_inside_of_triangle (p1,p2,p3) -> Subset of ( TOP-REAL n) equals { p where p be Point of ( TOP-REAL n) : ex a1,a2,a3 be Real st 0 <= a1 & 0 <= a2 & 0 <= a3 & ((a1 + a2) + a3) = 1 & p = (((a1 * p1) + (a2 * p2)) + (a3 * p3)) };

 correctness

 proof

 defpred P[ set] means ex a1,a2,a3 be Real st 0 <= a1 & 0 <= a2 & 0 <= a3 & ((a1 + a2) + a3) = 1 & $1 = (((a1 * p1) + (a2 * p2)) + (a3 * p3));

 { p where p be Element of ( TOP-REAL n) : P[p] } is Subset of ( TOP-REAL n) from DOMAIN_1:sch 7;

 hence thesis;

 end;

 end

 definition

 let n be Element of NAT , p1,p2,p3 be Point of ( TOP-REAL n);

 :: EUCLID_3:def7

 func inside_of_triangle (p1,p2,p3) -> Subset of ( TOP-REAL n) equals (( closed_inside_of_triangle (p1,p2,p3)) \ ( Triangle (p1,p2,p3)));

 correctness ;

 end

 definition

 let n be Element of NAT , p1,p2,p3 be Point of ( TOP-REAL n);

 :: EUCLID_3:def8

 func outside_of_triangle (p1,p2,p3) -> Subset of ( TOP-REAL n) equals { p where p be Point of ( TOP-REAL n) : ex a1,a2,a3 be Real st ( 0 > a1 or 0 > a2 or 0 > a3) & ((a1 + a2) + a3) = 1 & p = (((a1 * p1) + (a2 * p2)) + (a3 * p3)) };

 correctness

 proof

 defpred P[ set] means ex a1,a2,a3 be Real st ( 0 > a1 or 0 > a2 or 0 > a3) & ((a1 + a2) + a3) = 1 & $1 = (((a1 * p1) + (a2 * p2)) + (a3 * p3));

 { p where p be Point of ( TOP-REAL n) : P[p] } is Subset of ( TOP-REAL n) from DOMAIN_1:sch 7;

 hence thesis;

 end;

 end

 definition

 let n be Element of NAT , p1,p2,p3 be Point of ( TOP-REAL n);

 :: EUCLID_3:def9

 func plane (p1,p2,p3) -> Subset of ( TOP-REAL n) equals (( outside_of_triangle (p1,p2,p3)) \/ ( closed_inside_of_triangle (p1,p2,p3)));

 correctness ;

 end

 theorem :: EUCLID_3:48



 Th48: for n be Element of NAT , p1,p2,p3,p be Point of ( TOP-REAL n) st p in ( plane (p1,p2,p3)) holds ex a1,a2,a3 be Real st ((a1 + a2) + a3) = 1 & p = (((a1 * p1) + (a2 * p2)) + (a3 * p3))

 proof

 let n be Element of NAT , p1,p2,p3,p be Point of ( TOP-REAL n);

 assume

 A1: p in ( plane (p1,p2,p3));

 now

 per cases by A1, XBOOLE_0:def 3;

 case p in ( outside_of_triangle (p1,p2,p3));

 then ex p4 be Point of ( TOP-REAL n) st p4 = p & ex a1,a2,a3 be Real st ( 0 > a1 or 0 > a2 or 0 > a3) & ((a1 + a2) + a3) = 1 & p4 = (((a1 * p1) + (a2 * p2)) + (a3 * p3));

 hence thesis;

 end;

 case p in ( closed_inside_of_triangle (p1,p2,p3));

 then ex p4 be Point of ( TOP-REAL n) st p4 = p & ex a1,a2,a3 be Real st 0 <= a1 & 0 <= a2 & 0 <= a3 & ((a1 + a2) + a3) = 1 & p4 = (((a1 * p1) + (a2 * p2)) + (a3 * p3));

 hence thesis;

 end;

 end;

 hence thesis;

 end;

 theorem :: EUCLID_3:49

 for n be Element of NAT , p1,p2,p3 be Point of ( TOP-REAL n) holds ( Triangle (p1,p2,p3)) c= ( closed_inside_of_triangle (p1,p2,p3))

 proof

 let n be Element of NAT , p1,p2,p3 be Point of ( TOP-REAL n);

 ((( LSeg (p1,p2)) \/ ( LSeg (p2,p3))) \/ ( LSeg (p3,p1))) c= ( closed_inside_of_triangle (p1,p2,p3))

 proof

 let x be object;

 assume

 A1: x in ((( LSeg (p1,p2)) \/ ( LSeg (p2,p3))) \/ ( LSeg (p3,p1)));

 then

 reconsider p0 = x as Point of ( TOP-REAL n);



 A2: x in (( LSeg (p1,p2)) \/ ( LSeg (p2,p3))) or x in ( LSeg (p3,p1)) by A1, XBOOLE_0:def 3;

 now

 per cases by A2, XBOOLE_0:def 3;

 case x in ( LSeg (p1,p2));

 then

 consider lambda be Real such that

 A3: x = (((1 - lambda) * p1) + (lambda * p2)) and

 A4: 0 <= lambda and

 A5: lambda <= 1;



 A6: p0 = ((((1 - lambda) * p1) + (lambda * p2)) + ( 0. ( TOP-REAL n))) by A3, RLVECT_1: 4

 .= ((((1 - lambda) * p1) + (lambda * p2)) + ( 0 * p3)) by RLVECT_1: 10;



 A7: (((1 - lambda) + lambda) + 0 ) = 1;

 (1 - lambda) >= 0 by A5, XREAL_1: 48;

 hence ex a1,a2,a3 be Real st 0 <= a1 & 0 <= a2 & 0 <= a3 & ((a1 + a2) + a3) = 1 & p0 = (((a1 * p1) + (a2 * p2)) + (a3 * p3)) by A4, A7, A6;

 end;

 case x in ( LSeg (p2,p3));

 then

 consider lambda be Real such that

 A8: x = (((1 - lambda) * p2) + (lambda * p3)) and

 A9: 0 <= lambda and

 A10: lambda <= 1;



 A11: p0 = ((( 0. ( TOP-REAL n)) + ((1 - lambda) * p2)) + (lambda * p3)) by A8, RLVECT_1: 4

 .= ((( 0 * p1) + ((1 - lambda) * p2)) + (lambda * p3)) by RLVECT_1: 10;



 A12: (( 0 + (1 - lambda)) + lambda) = 1;

 (1 - lambda) >= 0 by A10, XREAL_1: 48;

 hence ex a1,a2,a3 be Real st 0 <= a1 & 0 <= a2 & 0 <= a3 & ((a1 + a2) + a3) = 1 & p0 = (((a1 * p1) + (a2 * p2)) + (a3 * p3)) by A9, A12, A11;

 end;

 case x in ( LSeg (p3,p1));

 then

 consider lambda be Real such that

 A13: x = (((1 - lambda) * p3) + (lambda * p1)) and

 A14: 0 <= lambda and

 A15: lambda <= 1;



 A16: p0 = (((lambda * p1) + ( 0. ( TOP-REAL n))) + ((1 - lambda) * p3)) by A13, RLVECT_1: 4

 .= (((lambda * p1) + ( 0 * p2)) + ((1 - lambda) * p3)) by RLVECT_1: 10;



 A17: ((lambda + 0 ) + (1 - lambda)) = 1;

 (1 - lambda) >= 0 by A15, XREAL_1: 48;

 hence ex a1,a2,a3 be Real st 0 <= a1 & 0 <= a2 & 0 <= a3 & ((a1 + a2) + a3) = 1 & p0 = (((a1 * p1) + (a2 * p2)) + (a3 * p3)) by A14, A17, A16;

 end;

 end;

 hence thesis;

 end;

 hence thesis;

 end;

 definition

 let n be Element of NAT , q1,q2 be Point of ( TOP-REAL n);

 :: EUCLID_3:def10

 pred q1,q2 are_lindependent2 means for a1,a2 be Real st ((a1 * q1) + (a2 * q2)) = ( 0. ( TOP-REAL n)) holds a1 = 0 & a2 = 0 ;

 end

 notation

 let n be Element of NAT , q1,q2 be Point of ( TOP-REAL n);

 antonym q1,q2 are_ldependent2 for q1,q2 are_lindependent2 ;

 end

 theorem :: EUCLID_3:50



 Th50: for n be Element of NAT , q1,q2 be Point of ( TOP-REAL n) st (q1,q2) are_lindependent2 holds q1 <> q2 & q1 <> ( 0. ( TOP-REAL n)) & q2 <> ( 0. ( TOP-REAL n))

 proof

 let n be Element of NAT , q1,q2 be Point of ( TOP-REAL n);

 assume

 A1: (q1,q2) are_lindependent2 ;

 assume

 A2: q1 = q2 or q1 = ( 0. ( TOP-REAL n)) or q2 = ( 0. ( TOP-REAL n));

 now

 per cases by A2;

 case

 A3: q1 = q2;

 ((1 * q1) + (( - 1) * q2)) = ((1 * q1) + ( - q2)) by RLVECT_1: 16

 .= (q1 + ( - q2)) by RLVECT_1:def 8

 .= ( 0. ( TOP-REAL n)) by A3, RLVECT_1: 5;

 hence contradiction by A1;

 end;

 case q1 = ( 0. ( TOP-REAL n));



 then ((1 * q1) + ( 0 * q2)) = (( 0. ( TOP-REAL n)) + ( 0 * q2)) by RLVECT_1: 10

 .= (( 0. ( TOP-REAL n)) + ( 0. ( TOP-REAL n))) by RLVECT_1: 10

 .= ( 0. ( TOP-REAL n)) by RLVECT_1: 4;

 hence contradiction by A1;

 end;

 case q2 = ( 0. ( TOP-REAL n));



 then (( 0 * q1) + (1 * q2)) = (( 0 * q1) + ( 0. ( TOP-REAL n))) by RLVECT_1: 10

 .= (( 0. ( TOP-REAL n)) + ( 0. ( TOP-REAL n))) by RLVECT_1: 10

 .= ( 0. ( TOP-REAL n)) by RLVECT_1: 4;

 hence contradiction by A1;

 end;

 end;

 hence contradiction;

 end;

 theorem :: EUCLID_3:51



 Th51: for n be Element of NAT , p1,p2,p3,p0 be Point of ( TOP-REAL n) st ((p2 - p1),(p3 - p1)) are_lindependent2 & p0 in ( plane (p1,p2,p3)) holds ex a1,a2,a3 be Real st p0 = (((a1 * p1) + (a2 * p2)) + (a3 * p3)) & ((a1 + a2) + a3) = 1 & for b1,b2,b3 be Real st p0 = (((b1 * p1) + (b2 * p2)) + (b3 * p3)) & ((b1 + b2) + b3) = 1 holds b1 = a1 & b2 = a2 & b3 = a3

 proof

 let n be Element of NAT , p1,p2,p3,p0 be Point of ( TOP-REAL n);

 assume that

 A1: ((p2 - p1),(p3 - p1)) are_lindependent2 and

 A2: p0 in ( plane (p1,p2,p3));

 set q2 = (p2 - p1), q3 = (p3 - p1);

 consider a01,a02,a03 be Real such that

 A3: ((a01 + a02) + a03) = 1 and

 A4: p0 = (((a01 * p1) + (a02 * p2)) + (a03 * p3)) by A2, Th48;

 for b1,b2,b3 be Real st p0 = (((b1 * p1) + (b2 * p2)) + (b3 * p3)) & ((b1 + b2) + b3) = 1 holds b1 = a01 & b2 = a02 & b3 = a03

 proof



 A5: (p0 + ( - p1)) = ((((a01 * p1) + (a02 * p2)) + (a03 * p3)) + ( - (((a01 + a02) + a03) * p1))) by A3, A4, RLVECT_1:def 8

 .= ((((a01 * p1) + (a02 * p2)) + (a03 * p3)) + ( - (((a01 + a02) * p1) + (a03 * p1)))) by RLVECT_1:def 6

 .= ((((a01 * p1) + (a02 * p2)) + (a03 * p3)) + ( - (((a01 * p1) + (a02 * p1)) + (a03 * p1)))) by RLVECT_1:def 6

 .= ((((a01 * p1) + (a02 * p2)) + (a03 * p3)) + (( - ((a01 * p1) + (a02 * p1))) - (a03 * p1))) by RLVECT_1: 30

 .= ((((a01 * p1) + (a02 * p2)) + (a03 * p3)) + ((( - (a01 * p1)) - (a02 * p1)) - (a03 * p1))) by RLVECT_1: 30

 .= (((a01 * p1) + ((a02 * p2) + (a03 * p3))) + ((( - (a01 * p1)) + ( - (a02 * p1))) + ( - (a03 * p1)))) by RLVECT_1:def 3

 .= (((a01 * p1) + ((a02 * p2) + (a03 * p3))) + (( - (a01 * p1)) + (( - (a02 * p1)) + ( - (a03 * p1))))) by RLVECT_1:def 3

 .= (((((a02 * p2) + (a03 * p3)) + (a01 * p1)) - (a01 * p1)) + (( - (a02 * p1)) + ( - (a03 * p1)))) by RLVECT_1:def 3

 .= (((a02 * p2) + (a03 * p3)) + (( - (a02 * p1)) + ( - (a03 * p1)))) by RLVECT_4: 1

 .= ((((a02 * p2) + (a03 * p3)) + ( - (a02 * p1))) + ( - (a03 * p1))) by RLVECT_1:def 3

 .= ((((a02 * p2) + ( - (a02 * p1))) + (a03 * p3)) + ( - (a03 * p1))) by RLVECT_1:def 3

 .= ((((a02 * p2) + (a02 * ( - p1))) + (a03 * p3)) + ( - (a03 * p1))) by RLVECT_1: 25

 .= (((a02 * (p2 + ( - p1))) + (a03 * p3)) + ( - (a03 * p1))) by RLVECT_1:def 5

 .= ((a02 * (p2 + ( - p1))) + ((a03 * p3) + ( - (a03 * p1)))) by RLVECT_1:def 3

 .= ((a02 * (p2 + ( - p1))) + ((a03 * p3) + (a03 * ( - p1)))) by RLVECT_1: 25

 .= ((a02 * q2) + (a03 * q3)) by RLVECT_1:def 5;

 let b1,b2,b3 be Real;

 assume that

 A6: p0 = (((b1 * p1) + (b2 * p2)) + (b3 * p3)) and

 A7: ((b1 + b2) + b3) = 1;

 (p0 + ( - p1)) = ((((b1 * p1) + (b2 * p2)) + (b3 * p3)) + ( - (((b1 + b2) + b3) * p1))) by A6, A7, RLVECT_1:def 8

 .= ((((b1 * p1) + (b2 * p2)) + (b3 * p3)) + ( - (((b1 + b2) * p1) + (b3 * p1)))) by RLVECT_1:def 6

 .= ((((b1 * p1) + (b2 * p2)) + (b3 * p3)) + ( - (((b1 * p1) + (b2 * p1)) + (b3 * p1)))) by RLVECT_1:def 6

 .= ((((b1 * p1) + (b2 * p2)) + (b3 * p3)) + (( - ((b1 * p1) + (b2 * p1))) - (b3 * p1))) by RLVECT_1: 30

 .= ((((b1 * p1) + (b2 * p2)) + (b3 * p3)) + ((( - (b1 * p1)) - (b2 * p1)) - (b3 * p1))) by RLVECT_1: 30

 .= (((b1 * p1) + ((b2 * p2) + (b3 * p3))) + ((( - (b1 * p1)) + ( - (b2 * p1))) + ( - (b3 * p1)))) by RLVECT_1:def 3

 .= (((b1 * p1) + ((b2 * p2) + (b3 * p3))) + (( - (b1 * p1)) + (( - (b2 * p1)) + ( - (b3 * p1))))) by RLVECT_1:def 3

 .= (((((b2 * p2) + (b3 * p3)) + (b1 * p1)) - (b1 * p1)) + (( - (b2 * p1)) + ( - (b3 * p1)))) by RLVECT_1:def 3

 .= (((b2 * p2) + (b3 * p3)) + (( - (b2 * p1)) + ( - (b3 * p1)))) by RLVECT_4: 1

 .= ((((b2 * p2) + (b3 * p3)) + ( - (b2 * p1))) + ( - (b3 * p1))) by RLVECT_1:def 3

 .= ((((b2 * p2) + ( - (b2 * p1))) + (b3 * p3)) + ( - (b3 * p1))) by RLVECT_1:def 3

 .= ((((b2 * p2) + (b2 * ( - p1))) + (b3 * p3)) + ( - (b3 * p1))) by RLVECT_1: 25

 .= (((b2 * (p2 + ( - p1))) + (b3 * p3)) + ( - (b3 * p1))) by RLVECT_1:def 5

 .= ((b2 * (p2 + ( - p1))) + ((b3 * p3) + ( - (b3 * p1)))) by RLVECT_1:def 3

 .= ((b2 * (p2 + ( - p1))) + ((b3 * p3) + (b3 * ( - p1)))) by RLVECT_1: 25

 .= ((b2 * q2) + (b3 * q3)) by RLVECT_1:def 5;

 then (((b2 * q2) + (b3 * q3)) + ( - ((a02 * q2) + (a03 * q3)))) = ( 0. ( TOP-REAL n)) by A5, RLVECT_1: 5;

 then (((b2 * q2) + (b3 * q3)) + (( - (a02 * q2)) - (a03 * q3))) = ( 0. ( TOP-REAL n)) by RLVECT_1: 30;

 then ((((b2 * q2) + (b3 * q3)) + ( - (a02 * q2))) + ( - (a03 * q3))) = ( 0. ( TOP-REAL n)) by RLVECT_1:def 3;

 then ((((b2 * q2) + ( - (a02 * q2))) + (b3 * q3)) + ( - (a03 * q3))) = ( 0. ( TOP-REAL n)) by RLVECT_1:def 3;

 then ((((b2 * q2) + (( - a02) * q2)) + (b3 * q3)) + ( - (a03 * q3))) = ( 0. ( TOP-REAL n)) by RLVECT_1: 79;

 then ((((b2 + ( - a02)) * q2) + (b3 * q3)) + ( - (a03 * q3))) = ( 0. ( TOP-REAL n)) by RLVECT_1:def 6;

 then (((b2 + ( - a02)) * q2) + ((b3 * q3) + ( - (a03 * q3)))) = ( 0. ( TOP-REAL n)) by RLVECT_1:def 3;

 then (((b2 + ( - a02)) * q2) + ((b3 * q3) + (( - a03) * q3))) = ( 0. ( TOP-REAL n)) by RLVECT_1: 79;

 then (((b2 + ( - a02)) * q2) + ((b3 + ( - a03)) * q3)) = ( 0. ( TOP-REAL n)) by RLVECT_1:def 6;

 then ((b2 - a02) + a02) = ( 0 + a02) & (b3 + ( - a03)) = 0 by A1;

 hence thesis by A3, A7;

 end;

 hence thesis by A3, A4;

 end;

 theorem :: EUCLID_3:52



 Th52: for n be Element of NAT , p1,p2,p3,p0 be Point of ( TOP-REAL n) st (ex a1,a2,a3 be Real st p0 = (((a1 * p1) + (a2 * p2)) + (a3 * p3)) & ((a1 + a2) + a3) = 1) holds p0 in ( plane (p1,p2,p3))

 proof

 let n be Element of NAT , p1,p2,p3,p0 be Point of ( TOP-REAL n);

 given a1,a2,a3 be Real such that

 A1: p0 = (((a1 * p1) + (a2 * p2)) + (a3 * p3)) & ((a1 + a2) + a3) = 1;

 now

 per cases ;

 case 0 > a1 or 0 > a2 or 0 > a3;

 then p0 in ( outside_of_triangle (p1,p2,p3)) by A1;

 hence thesis by XBOOLE_0:def 3;

 end;

 case 0 <= a1 & 0 <= a2 & 0 <= a3;

 then p0 in ( closed_inside_of_triangle (p1,p2,p3)) by A1;

 hence thesis by XBOOLE_0:def 3;

 end;

 end;

 hence thesis;

 end;

 theorem :: EUCLID_3:53

 for n be Element of NAT , p1,p2,p3 be Point of ( TOP-REAL n) holds ( plane (p1,p2,p3)) = { p where p be Point of ( TOP-REAL n) : ex a1,a2,a3 be Real st ((a1 + a2) + a3) = 1 & p = (((a1 * p1) + (a2 * p2)) + (a3 * p3)) }

 proof

 let n be Element of NAT , p1,p2,p3 be Point of ( TOP-REAL n);

 thus ( plane (p1,p2,p3)) c= { p where p be Point of ( TOP-REAL n) : ex a1,a2,a3 be Real st ((a1 + a2) + a3) = 1 & p = (((a1 * p1) + (a2 * p2)) + (a3 * p3)) }

 proof

 let x be object;

 assume

 A1: x in ( plane (p1,p2,p3));

 then

 reconsider p0 = x as Point of ( TOP-REAL n);

 ex a1,a2,a3 be Real st ((a1 + a2) + a3) = 1 & p0 = (((a1 * p1) + (a2 * p2)) + (a3 * p3)) by A1, Th48;

 hence thesis;

 end;

 let x be object;

 assume x in { p where p be Point of ( TOP-REAL n) : ex a1,a2,a3 be Real st ((a1 + a2) + a3) = 1 & p = (((a1 * p1) + (a2 * p2)) + (a3 * p3)) };

 then ex p be Point of ( TOP-REAL n) st p = x & ex a1,a2,a3 be Real st ((a1 + a2) + a3) = 1 & p = (((a1 * p1) + (a2 * p2)) + (a3 * p3));

 hence thesis by Th52;

 end;

 theorem :: EUCLID_3:54



 Th54: for p1, p2, p3 st ((p2 - p1),(p3 - p1)) are_lindependent2 holds ( plane (p1,p2,p3)) = ( REAL 2)

 proof

 let p1, p2, p3;

 assume

 A1: ((p2 - p1),(p3 - p1)) are_lindependent2 ;

 the carrier of ( TOP-REAL 2) = ( REAL 2) by EUCLID: 22;

 hence ( plane (p1,p2,p3)) c= ( REAL 2);

 let x be object;

 assume x in ( REAL 2);

 then

 reconsider p0 = x as Point of ( TOP-REAL 2) by EUCLID: 22;

 set q2 = (p2 - p1), q3 = (p3 - p1), p = (p0 - p1);



 A2: q3 <> ( 0. ( TOP-REAL 2)) by A1, Th50;

 now

 per cases by A2, EUCLID: 53, EUCLID: 54;

 case

 A3: (q3 `1 ) <> 0 ;

 A4:

 now

 assume (((q2 `2 ) * (q3 `1 )) - ((q2 `1 ) * (q3 `2 ))) = 0 ;

 then (q2 `2 ) = (((q2 `1 ) * (q3 `2 )) / (q3 `1 )) by A3, XCMPLX_1: 89;



 then q2 = |[(q2 `1 ), (((q2 `1 ) * (q3 `2 )) / (q3 `1 ))]| by EUCLID: 53

 .= |[((q2 `1 ) * 1), (((q2 `1 ) * (q3 `2 )) * ((q3 `1 ) " ))]| by XCMPLX_0:def 9

 .= |[((q2 `1 ) * 1), ((q2 `1 ) * ((q3 `2 ) * ((q3 `1 ) " )))]|

 .= ((q2 `1 ) * |[1, ((q3 `2 ) * ((q3 `1 ) " ))]|) by EUCLID: 58

 .= ((q2 `1 ) * |[(((q3 `1 ) " ) * (q3 `1 )), (((q3 `1 ) " ) * (q3 `2 ))]|) by A3, XCMPLX_0:def 7

 .= ((q2 `1 ) * (((q3 `1 ) " ) * |[(q3 `1 ), (q3 `2 )]|)) by EUCLID: 58

 .= ((q2 `1 ) * (((q3 `1 ) " ) * q3)) by EUCLID: 53

 .= (((q2 `1 ) * ((q3 `1 ) " )) * q3) by RLVECT_1:def 7;

 then (q2 + ( - (((q2 `1 ) * ((q3 `1 ) " )) * q3))) = ( 0. ( TOP-REAL 2)) by RLVECT_1: 5;

 then ((1 * q2) + ( - (((q2 `1 ) * ((q3 `1 ) " )) * q3))) = ( 0. ( TOP-REAL 2)) by RLVECT_1:def 8;

 then ((1 * q2) + (( - ((q2 `1 ) * ((q3 `1 ) " ))) * q3)) = ( 0. ( TOP-REAL 2)) by RLVECT_1: 79;

 hence contradiction by A1;

 end;

 set a = ((((p `2 ) * (q3 `1 )) - ((q3 `2 ) * (p `1 ))) / (((q2 `2 ) * (q3 `1 )) - ((q2 `1 ) * (q3 `2 ))));

 set b = (((p `1 ) - (a * (q2 `1 ))) / (q3 `1 ));



 A5: ((a * (q2 `1 )) + (b * (q3 `1 ))) = ((a * (q2 `1 )) + ((p `1 ) - (a * (q2 `1 )))) by A3, XCMPLX_1: 87

 .= (p `1 );



 A6: ((a * (q2 `2 )) + (b * (q3 `2 ))) = ((a * (q2 `2 )) + ((((p `1 ) / (q3 `1 )) - ((a * (q2 `1 )) / (q3 `1 ))) * (q3 `2 ))) by XCMPLX_1: 120

 .= (((a * (q2 `2 )) - (((a * (q2 `1 )) / (q3 `1 )) * (q3 `2 ))) + (((p `1 ) / (q3 `1 )) * (q3 `2 )))

 .= (((a * (q2 `2 )) - (((a * (q2 `1 )) * ((q3 `1 ) " )) * (q3 `2 ))) + (((p `1 ) / (q3 `1 )) * (q3 `2 ))) by XCMPLX_0:def 9

 .= ((a * ((q2 `2 ) - (((q2 `1 ) * ((q3 `1 ) " )) * (q3 `2 )))) + (((p `1 ) / (q3 `1 )) * (q3 `2 )))

 .= ((a * ((q2 `2 ) - (((q2 `1 ) / (q3 `1 )) * (q3 `2 )))) + (((p `1 ) / (q3 `1 )) * (q3 `2 ))) by XCMPLX_0:def 9

 .= ((a * ((((q2 `2 ) / (q3 `1 )) * (q3 `1 )) - (((q2 `1 ) / (q3 `1 )) * (q3 `2 )))) + (((p `1 ) / (q3 `1 )) * (q3 `2 ))) by A3, XCMPLX_1: 87

 .= ((a * ((((q3 `1 ) / (q3 `1 )) * (q2 `2 )) - (((q2 `1 ) / (q3 `1 )) * (q3 `2 )))) + (((p `1 ) / (q3 `1 )) * (q3 `2 ))) by XCMPLX_1: 75

 .= ((a * ((((q3 `1 ) * ((q3 `1 ) " )) * (q2 `2 )) - (((q2 `1 ) / (q3 `1 )) * (q3 `2 )))) + (((p `1 ) / (q3 `1 )) * (q3 `2 ))) by XCMPLX_0:def 9

 .= ((a * (((q2 `2 ) * ((q3 `1 ) * ((q3 `1 ) " ))) - ((((q3 `1 ) " ) * (q2 `1 )) * (q3 `2 )))) + (((p `1 ) / (q3 `1 )) * (q3 `2 ))) by XCMPLX_0:def 9

 .= (((a * (((q2 `2 ) * (q3 `1 )) - ((q2 `1 ) * (q3 `2 )))) * ((q3 `1 ) " )) + (((p `1 ) / (q3 `1 )) * (q3 `2 )))

 .= (((((p `2 ) * (q3 `1 )) - ((q3 `2 ) * (p `1 ))) * ((q3 `1 ) " )) + (((p `1 ) / (q3 `1 )) * (q3 `2 ))) by A4, XCMPLX_1: 87

 .= (((((p `2 ) * (q3 `1 )) - ((q3 `2 ) * (p `1 ))) * ((q3 `1 ) " )) + ((((q3 `1 ) " ) * (p `1 )) * (q3 `2 ))) by XCMPLX_0:def 9

 .= (((((p `2 ) * (q3 `1 )) - ((q3 `2 ) * (p `1 ))) + ((q3 `2 ) * (p `1 ))) * ((q3 `1 ) " ))

 .= (((p `2 ) * (q3 `1 )) / (q3 `1 )) by XCMPLX_0:def 9

 .= (p `2 ) by A3, XCMPLX_1: 89;



 A7: ((a * q2) + (b * q3)) = (((a * p2) - (a * p1)) + (b * (p3 - p1))) by RLVECT_1: 34

 .= (((a * p2) + ( - (a * p1))) + ((b * p3) - (b * p1))) by RLVECT_1: 34

 .= (((a * p2) + ( - (a * p1))) + ((b * p3) + (( - b) * p1))) by RLVECT_1: 79

 .= (((a * p2) + (( - a) * p1)) + ((( - b) * p1) + (b * p3))) by RLVECT_1: 79

 .= ((((a * p2) + (( - a) * p1)) + (( - b) * p1)) + (b * p3)) by RLVECT_1:def 3

 .= (((a * p2) + ((( - a) * p1) + (( - b) * p1))) + (b * p3)) by RLVECT_1:def 3

 .= ((((( - a) + ( - b)) * p1) + (a * p2)) + (b * p3)) by RLVECT_1:def 6;

 ((a * q2) + (b * q3)) = ((a * |[(q2 `1 ), (q2 `2 )]|) + (b * q3)) by EUCLID: 53

 .= ((a * |[(q2 `1 ), (q2 `2 )]|) + (b * |[(q3 `1 ), (q3 `2 )]|)) by EUCLID: 53

 .= ( |[(a * (q2 `1 )), (a * (q2 `2 ))]| + (b * |[(q3 `1 ), (q3 `2 )]|)) by EUCLID: 58

 .= ( |[(a * (q2 `1 )), (a * (q2 `2 ))]| + |[(b * (q3 `1 )), (b * (q3 `2 ))]|) by EUCLID: 58

 .= |[((a * (q2 `1 )) + (b * (q3 `1 ))), ((a * (q2 `2 )) + (b * (q3 `2 )))]| by EUCLID: 56

 .= p by A5, A6, EUCLID: 53;



 then

 A8: p0 = (p1 + ((((( - a) + ( - b)) * p1) + (a * p2)) + (b * p3))) by A7, RLVECT_4: 1

 .= ((p1 + (((( - a) + ( - b)) * p1) + (a * p2))) + (b * p3)) by RLVECT_1:def 3

 .= (((p1 + ((( - a) + ( - b)) * p1)) + (a * p2)) + (b * p3)) by RLVECT_1:def 3

 .= ((((1 * p1) + ((( - a) + ( - b)) * p1)) + (a * p2)) + (b * p3)) by RLVECT_1:def 8

 .= ((((1 + (( - a) + ( - b))) * p1) + (a * p2)) + (b * p3)) by RLVECT_1:def 6;

 (((1 + (( - a) + ( - b))) + a) + b) = 1;

 hence thesis by A8, Th52;

 end;

 case

 A9: (q3 `2 ) <> 0 ;

 now

 assume (((q2 `2 ) * (q3 `1 )) - ((q2 `1 ) * (q3 `2 ))) = 0 ;

 then (q2 `1 ) = (((q2 `2 ) * (q3 `1 )) / (q3 `2 )) by A9, XCMPLX_1: 89;



 then q2 = |[(((q2 `2 ) * (q3 `1 )) / (q3 `2 )), (q2 `2 )]| by EUCLID: 53

 .= |[(((q2 `2 ) * (q3 `1 )) * ((q3 `2 ) " )), ((q2 `2 ) * 1)]| by XCMPLX_0:def 9

 .= |[((q2 `2 ) * ((q3 `1 ) * ((q3 `2 ) " ))), ((q2 `2 ) * 1)]|

 .= ((q2 `2 ) * |[((q3 `1 ) * ((q3 `2 ) " )), 1]|) by EUCLID: 58

 .= ((q2 `2 ) * |[(((q3 `2 ) " ) * (q3 `1 )), (((q3 `2 ) " ) * (q3 `2 ))]|) by A9, XCMPLX_0:def 7

 .= ((q2 `2 ) * (((q3 `2 ) " ) * |[(q3 `1 ), (q3 `2 )]|)) by EUCLID: 58

 .= ((q2 `2 ) * (((q3 `2 ) " ) * q3)) by EUCLID: 53

 .= (((q2 `2 ) * ((q3 `2 ) " )) * q3) by RLVECT_1:def 7;

 then (q2 + ( - (((q2 `2 ) * ((q3 `2 ) " )) * q3))) = ( 0. ( TOP-REAL 2)) by RLVECT_1: 5;

 then ((1 * q2) + ( - (((q2 `2 ) * ((q3 `2 ) " )) * q3))) = ( 0. ( TOP-REAL 2)) by RLVECT_1:def 8;

 then ((1 * q2) + (( - ((q2 `2 ) * ((q3 `2 ) " ))) * q3)) = ( 0. ( TOP-REAL 2)) by RLVECT_1: 79;

 hence contradiction by A1;

 end;

 then

 A10: ( - (((q2 `2 ) * (q3 `1 )) + ( - ((q2 `1 ) * (q3 `2 ))))) <> ( - 0 );

 set a = ((((p `1 ) * (q3 `2 )) - ((q3 `1 ) * (p `2 ))) / (((q2 `1 ) * (q3 `2 )) - ((q2 `2 ) * (q3 `1 ))));

 set b = (((p `2 ) - (a * (q2 `2 ))) / (q3 `2 ));



 A11: ((a * (q2 `2 )) + (b * (q3 `2 ))) = ((a * (q2 `2 )) + ((p `2 ) - (a * (q2 `2 )))) by A9, XCMPLX_1: 87

 .= (p `2 );



 A12: ((a * (q2 `1 )) + (b * (q3 `1 ))) = ((a * (q2 `1 )) + ((((p `2 ) / (q3 `2 )) - ((a * (q2 `2 )) / (q3 `2 ))) * (q3 `1 ))) by XCMPLX_1: 120

 .= (((a * (q2 `1 )) - (((a * (q2 `2 )) / (q3 `2 )) * (q3 `1 ))) + (((p `2 ) / (q3 `2 )) * (q3 `1 )))

 .= (((a * (q2 `1 )) - (((a * (q2 `2 )) * ((q3 `2 ) " )) * (q3 `1 ))) + (((p `2 ) / (q3 `2 )) * (q3 `1 ))) by XCMPLX_0:def 9

 .= ((a * ((q2 `1 ) - (((q2 `2 ) * ((q3 `2 ) " )) * (q3 `1 )))) + (((p `2 ) / (q3 `2 )) * (q3 `1 )))

 .= ((a * ((q2 `1 ) - (((q2 `2 ) / (q3 `2 )) * (q3 `1 )))) + (((p `2 ) / (q3 `2 )) * (q3 `1 ))) by XCMPLX_0:def 9

 .= ((a * ((((q2 `1 ) / (q3 `2 )) * (q3 `2 )) - (((q2 `2 ) / (q3 `2 )) * (q3 `1 )))) + (((p `2 ) / (q3 `2 )) * (q3 `1 ))) by A9, XCMPLX_1: 87

 .= ((a * ((((q3 `2 ) / (q3 `2 )) * (q2 `1 )) - (((q2 `2 ) / (q3 `2 )) * (q3 `1 )))) + (((p `2 ) / (q3 `2 )) * (q3 `1 ))) by XCMPLX_1: 75

 .= ((a * ((((q3 `2 ) * ((q3 `2 ) " )) * (q2 `1 )) - (((q2 `2 ) / (q3 `2 )) * (q3 `1 )))) + (((p `2 ) / (q3 `2 )) * (q3 `1 ))) by XCMPLX_0:def 9

 .= ((a * (((q2 `1 ) * ((q3 `2 ) * ((q3 `2 ) " ))) - ((((q3 `2 ) " ) * (q2 `2 )) * (q3 `1 )))) + (((p `2 ) / (q3 `2 )) * (q3 `1 ))) by XCMPLX_0:def 9

 .= (((a * (((q2 `1 ) * (q3 `2 )) - ((q2 `2 ) * (q3 `1 )))) * ((q3 `2 ) " )) + (((p `2 ) / (q3 `2 )) * (q3 `1 )))

 .= (((((p `1 ) * (q3 `2 )) - ((q3 `1 ) * (p `2 ))) * ((q3 `2 ) " )) + (((p `2 ) / (q3 `2 )) * (q3 `1 ))) by A10, XCMPLX_1: 87

 .= (((((p `1 ) * (q3 `2 )) - ((q3 `1 ) * (p `2 ))) * ((q3 `2 ) " )) + ((((q3 `2 ) " ) * (p `2 )) * (q3 `1 ))) by XCMPLX_0:def 9

 .= (((((p `1 ) * (q3 `2 )) - ((q3 `1 ) * (p `2 ))) + ((q3 `1 ) * (p `2 ))) * ((q3 `2 ) " ))

 .= (((p `1 ) * (q3 `2 )) / (q3 `2 )) by XCMPLX_0:def 9

 .= (p `1 ) by A9, XCMPLX_1: 89;



 A13: ((a * q2) + (b * q3)) = (((a * p2) - (a * p1)) + (b * (p3 - p1))) by RLVECT_1: 34

 .= (((a * p2) + ( - (a * p1))) + ((b * p3) - (b * p1))) by RLVECT_1: 34

 .= (((a * p2) + ( - (a * p1))) + ((b * p3) + (( - b) * p1))) by RLVECT_1: 79

 .= (((a * p2) + (( - a) * p1)) + ((( - b) * p1) + (b * p3))) by RLVECT_1: 79

 .= ((((a * p2) + (( - a) * p1)) + (( - b) * p1)) + (b * p3)) by RLVECT_1:def 3

 .= (((a * p2) + ((( - a) * p1) + (( - b) * p1))) + (b * p3)) by RLVECT_1:def 3

 .= ((((( - a) + ( - b)) * p1) + (a * p2)) + (b * p3)) by RLVECT_1:def 6;

 ((a * q2) + (b * q3)) = ((a * |[(q2 `1 ), (q2 `2 )]|) + (b * q3)) by EUCLID: 53

 .= ((a * |[(q2 `1 ), (q2 `2 )]|) + (b * |[(q3 `1 ), (q3 `2 )]|)) by EUCLID: 53

 .= ( |[(a * (q2 `1 )), (a * (q2 `2 ))]| + (b * |[(q3 `1 ), (q3 `2 )]|)) by EUCLID: 58

 .= ( |[(a * (q2 `1 )), (a * (q2 `2 ))]| + |[(b * (q3 `1 )), (b * (q3 `2 ))]|) by EUCLID: 58

 .= |[((a * (q2 `1 )) + (b * (q3 `1 ))), ((a * (q2 `2 )) + (b * (q3 `2 )))]| by EUCLID: 56

 .= p by A11, A12, EUCLID: 53;



 then

 A14: p0 = (p1 + ((((( - a) + ( - b)) * p1) + (a * p2)) + (b * p3))) by A13, RLVECT_4: 1

 .= ((p1 + (((( - a) + ( - b)) * p1) + (a * p2))) + (b * p3)) by RLVECT_1:def 3

 .= (((p1 + ((( - a) + ( - b)) * p1)) + (a * p2)) + (b * p3)) by RLVECT_1:def 3

 .= ((((1 * p1) + ((( - a) + ( - b)) * p1)) + (a * p2)) + (b * p3)) by RLVECT_1:def 8

 .= ((((1 + (( - a) + ( - b))) * p1) + (a * p2)) + (b * p3)) by RLVECT_1:def 6;

 (((1 + (( - a) + ( - b))) + a) + b) = 1;

 hence thesis by A14, Th52;

 end;

 end;

 hence thesis;

 end;

 definition

 let n be Element of NAT , p1,p2,p3,p be Point of ( TOP-REAL n);

 assume

 A1: ((p2 - p1),(p3 - p1)) are_lindependent2 & p in ( plane (p1,p2,p3));

 :: EUCLID_3:def11

 func tricord1 (p1,p2,p3,p) -> Real means

 : Def11: ex a2,a3 be Real st ((it + a2) + a3) = 1 & p = (((it * p1) + (a2 * p2)) + (a3 * p3));

 existence

 proof

 ex a01,a02,a03 be Real st p = (((a01 * p1) + (a02 * p2)) + (a03 * p3)) & ((a01 + a02) + a03) = 1 & for b1,b2,b3 be Real st p = (((b1 * p1) + (b2 * p2)) + (b3 * p3)) & ((b1 + b2) + b3) = 1 holds b1 = a01 & b2 = a02 & b3 = a03 by A1, Th51;

 hence thesis;

 end;

 uniqueness

 proof

 let a1,b1 be Real;

 assume that

 A2: ex a2,a3 be Real st ((a1 + a2) + a3) = 1 & p = (((a1 * p1) + (a2 * p2)) + (a3 * p3)) and

 A3: ex a2,a3 be Real st ((b1 + a2) + a3) = 1 & p = (((b1 * p1) + (a2 * p2)) + (a3 * p3));

 consider a001,a002,a003 be Real such that p = (((a001 * p1) + (a002 * p2)) + (a003 * p3)) and ((a001 + a002) + a003) = 1 and

 A4: for b01,b02,b03 be Real st p = (((b01 * p1) + (b02 * p2)) + (b03 * p3)) & ((b01 + b02) + b03) = 1 holds b01 = a001 & b02 = a002 & b03 = a003 by A1, Th51;

 a1 = a001 by A2, A4;

 hence thesis by A3, A4;

 end;

 end

 definition

 let n be Element of NAT , p1,p2,p3,p be Point of ( TOP-REAL n);

 assume

 A1: ((p2 - p1),(p3 - p1)) are_lindependent2 & p in ( plane (p1,p2,p3));

 :: EUCLID_3:def12

 func tricord2 (p1,p2,p3,p) -> Real means

 : Def12: ex a1,a3 be Real st ((a1 + it ) + a3) = 1 & p = (((a1 * p1) + (it * p2)) + (a3 * p3));

 existence

 proof

 ex a01,a02,a03 be Real st p = (((a01 * p1) + (a02 * p2)) + (a03 * p3)) & ((a01 + a02) + a03) = 1 & for b1,b2,b3 be Real st p = (((b1 * p1) + (b2 * p2)) + (b3 * p3)) & ((b1 + b2) + b3) = 1 holds b1 = a01 & b2 = a02 & b3 = a03 by A1, Th51;

 hence thesis;

 end;

 uniqueness

 proof

 let a2,b2 be Real;

 assume that

 A2: ex a1,a3 be Real st ((a1 + a2) + a3) = 1 & p = (((a1 * p1) + (a2 * p2)) + (a3 * p3)) and

 A3: ex a1,a3 be Real st ((a1 + b2) + a3) = 1 & p = (((a1 * p1) + (b2 * p2)) + (a3 * p3));

 consider a001,a002,a003 be Real such that p = (((a001 * p1) + (a002 * p2)) + (a003 * p3)) and ((a001 + a002) + a003) = 1 and

 A4: for b01,b02,b03 be Real st p = (((b01 * p1) + (b02 * p2)) + (b03 * p3)) & ((b01 + b02) + b03) = 1 holds b01 = a001 & b02 = a002 & b03 = a003 by A1, Th51;

 a2 = a002 by A2, A4;

 hence thesis by A3, A4;

 end;

 end

 definition

 let n be Element of NAT , p1,p2,p3,p be Point of ( TOP-REAL n);

 assume

 A1: ((p2 - p1),(p3 - p1)) are_lindependent2 & p in ( plane (p1,p2,p3));

 :: EUCLID_3:def13

 func tricord3 (p1,p2,p3,p) -> Real means

 : Def13: ex a1,a2 be Real st ((a1 + a2) + it ) = 1 & p = (((a1 * p1) + (a2 * p2)) + (it * p3));

 existence

 proof

 ex a01,a02,a03 be Real st p = (((a01 * p1) + (a02 * p2)) + (a03 * p3)) & ((a01 + a02) + a03) = 1 & for b1,b2,b3 be Real st p = (((b1 * p1) + (b2 * p2)) + (b3 * p3)) & ((b1 + b2) + b3) = 1 holds b1 = a01 & b2 = a02 & b3 = a03 by A1, Th51;

 hence thesis;

 end;

 uniqueness

 proof

 let a3,b3 be Real;

 assume that

 A2: ex a1,a2 be Real st ((a1 + a2) + a3) = 1 & p = (((a1 * p1) + (a2 * p2)) + (a3 * p3)) and

 A3: ex a1,a2 be Real st ((a1 + a2) + b3) = 1 & p = (((a1 * p1) + (a2 * p2)) + (b3 * p3));

 consider a001,a002,a003 be Real such that p = (((a001 * p1) + (a002 * p2)) + (a003 * p3)) and ((a001 + a002) + a003) = 1 and

 A4: for b01,b02,b03 be Real st p = (((b01 * p1) + (b02 * p2)) + (b03 * p3)) & ((b01 + b02) + b03) = 1 holds b01 = a001 & b02 = a002 & b03 = a003 by A1, Th51;

 a3 = a003 by A2, A4;

 hence thesis by A3, A4;

 end;

 end

 definition

 let p1, p2, p3;

 :: EUCLID_3:def14

 func trcmap1 (p1,p2,p3) -> Function of ( TOP-REAL 2), R^1 means for p holds (it . p) = ( tricord1 (p1,p2,p3,p));

 existence

 proof

 defpred P[ object, object] means for p st p = $1 holds $2 = ( tricord1 (p1,p2,p3,p));

 set X = the carrier of ( TOP-REAL 2), Y = the carrier of R^1 ;



 A1: for x be object st x in X holds ex y be object st y in Y & P[x, y]

 proof

 let x be object;

 assume x in X;

 then

 reconsider p0 = x as Point of ( TOP-REAL 2);



 A2: ( tricord1 (p1,p2,p3,p0)) in REAL by XREAL_0:def 1;

 P[x, ( tricord1 (p1,p2,p3,p0))];

 hence thesis by A2, TOPMETR: 17;

 end;

 ex f be Function of X, Y st for x be object st x in X holds P[x, (f . x)] from FUNCT_2:sch 1( A1);

 then

 consider g be Function of X, Y such that

 A3: for x be object st x in X holds for p st p = x holds (g . x) = ( tricord1 (p1,p2,p3,p));

 reconsider f0 = g as Function of ( TOP-REAL 2), R^1 ;

 for p holds (f0 . p) = ( tricord1 (p1,p2,p3,p)) by A3;

 hence thesis;

 end;

 uniqueness

 proof

 let f1,f2 be Function of ( TOP-REAL 2), R^1 ;

 assume that

 A4: for p holds (f1 . p) = ( tricord1 (p1,p2,p3,p)) and

 A5: for p holds (f2 . p) = ( tricord1 (p1,p2,p3,p));



 A6: for x be object st x in ( dom f1) holds (f1 . x) = (f2 . x)

 proof

 let x be object;

 assume x in ( dom f1);

 then

 reconsider p0 = x as Point of ( TOP-REAL 2) by FUNCT_2:def 1;

 (f1 . p0) = ( tricord1 (p1,p2,p3,p0)) by A4;

 hence thesis by A5;

 end;

 ( dom f1) = the carrier of ( TOP-REAL 2) by FUNCT_2:def 1;

 then ( dom f1) = ( dom f2) by FUNCT_2:def 1;

 hence f1 = f2 by A6, FUNCT_1: 2;

 end;

 end

 definition

 let p1, p2, p3;

 :: EUCLID_3:def15

 func trcmap2 (p1,p2,p3) -> Function of ( TOP-REAL 2), R^1 means for p holds (it . p) = ( tricord2 (p1,p2,p3,p));

 existence

 proof

 defpred P[ object, object] means for p st p = $1 holds $2 = ( tricord2 (p1,p2,p3,p));

 set X = the carrier of ( TOP-REAL 2), Y = the carrier of R^1 ;



 A1: for x be object st x in X holds ex y be object st y in Y & P[x, y]

 proof

 let x be object;

 assume x in X;

 then

 reconsider p0 = x as Point of ( TOP-REAL 2);

 reconsider t = ( tricord2 (p1,p2,p3,p0)) as Element of REAL by XREAL_0:def 1;

 P[x, t];

 hence thesis by TOPMETR: 17;

 end;

 ex f be Function of X, Y st for x be object st x in X holds P[x, (f . x)] from FUNCT_2:sch 1( A1);

 then

 consider g be Function of X, Y such that

 A2: for x be object st x in X holds for p st p = x holds (g . x) = ( tricord2 (p1,p2,p3,p));

 reconsider f0 = g as Function of ( TOP-REAL 2), R^1 ;

 for p holds (f0 . p) = ( tricord2 (p1,p2,p3,p)) by A2;

 hence thesis;

 end;

 uniqueness

 proof

 let f1,f2 be Function of ( TOP-REAL 2), R^1 ;

 assume that

 A3: for p holds (f1 . p) = ( tricord2 (p1,p2,p3,p)) and

 A4: for p holds (f2 . p) = ( tricord2 (p1,p2,p3,p));



 A5: for x be object st x in ( dom f1) holds (f1 . x) = (f2 . x)

 proof

 let x be object;

 assume x in ( dom f1);

 then

 reconsider p0 = x as Point of ( TOP-REAL 2) by FUNCT_2:def 1;

 (f1 . p0) = ( tricord2 (p1,p2,p3,p0)) by A3;

 hence thesis by A4;

 end;

 ( dom f1) = the carrier of ( TOP-REAL 2) by FUNCT_2:def 1;

 then ( dom f1) = ( dom f2) by FUNCT_2:def 1;

 hence f1 = f2 by A5, FUNCT_1: 2;

 end;

 end

 definition

 let p1, p2, p3;

 :: EUCLID_3:def16

 func trcmap3 (p1,p2,p3) -> Function of ( TOP-REAL 2), R^1 means for p holds (it . p) = ( tricord3 (p1,p2,p3,p));

 existence

 proof

 defpred P[ object, object] means for p st p = $1 holds $2 = ( tricord3 (p1,p2,p3,p));

 set X = the carrier of ( TOP-REAL 2), Y = the carrier of R^1 ;



 A1: for x be object st x in X holds ex y be object st y in Y & P[x, y]

 proof

 let x be object;

 assume x in X;

 then

 reconsider p0 = x as Point of ( TOP-REAL 2);



 A2: ( tricord3 (p1,p2,p3,p0)) in REAL by XREAL_0:def 1;

 P[x, ( tricord3 (p1,p2,p3,p0))];

 hence thesis by A2, TOPMETR: 17;

 end;

 ex f be Function of X, Y st for x be object st x in X holds P[x, (f . x)] from FUNCT_2:sch 1( A1);

 then

 consider g be Function of X, Y such that

 A3: for x be object st x in X holds for p st p = x holds (g . x) = ( tricord3 (p1,p2,p3,p));

 reconsider f0 = g as Function of ( TOP-REAL 2), R^1 ;

 for p holds (f0 . p) = ( tricord3 (p1,p2,p3,p)) by A3;

 hence thesis;

 end;

 uniqueness

 proof

 let f1,f2 be Function of ( TOP-REAL 2), R^1 ;

 assume that

 A4: for p holds (f1 . p) = ( tricord3 (p1,p2,p3,p)) and

 A5: for p holds (f2 . p) = ( tricord3 (p1,p2,p3,p));



 A6: for x be object st x in ( dom f1) holds (f1 . x) = (f2 . x)

 proof

 let x be object;

 assume x in ( dom f1);

 then

 reconsider p0 = x as Point of ( TOP-REAL 2) by FUNCT_2:def 1;

 (f1 . p0) = ( tricord3 (p1,p2,p3,p0)) by A4;

 hence thesis by A5;

 end;

 ( dom f1) = the carrier of ( TOP-REAL 2) by FUNCT_2:def 1;

 then ( dom f1) = ( dom f2) by FUNCT_2:def 1;

 hence f1 = f2 by A6, FUNCT_1: 2;

 end;

 end

 theorem :: EUCLID_3:55

 for p1, p2, p3, p st ((p2 - p1),(p3 - p1)) are_lindependent2 holds p in ( outside_of_triangle (p1,p2,p3)) iff ( tricord1 (p1,p2,p3,p)) < 0 or ( tricord2 (p1,p2,p3,p)) < 0 or ( tricord3 (p1,p2,p3,p)) < 0

 proof

 let p1, p2, p3, p;

 set i1 = ( tricord1 (p1,p2,p3,p)), i2 = ( tricord2 (p1,p2,p3,p)), i3 = ( tricord3 (p1,p2,p3,p));

 assume

 A1: ((p2 - p1),(p3 - p1)) are_lindependent2 ;

 thus p in ( outside_of_triangle (p1,p2,p3)) implies ( tricord1 (p1,p2,p3,p)) < 0 or ( tricord2 (p1,p2,p3,p)) < 0 or ( tricord3 (p1,p2,p3,p)) < 0

 proof

 assume

 A2: p in ( outside_of_triangle (p1,p2,p3));

 p in the carrier of ( TOP-REAL 2);

 then p in ( REAL 2) by EUCLID: 22;

 then

 A3: p in ( plane (p1,p2,p3)) by A1, Th54;

 consider p0 such that

 A4: p0 = p and

 A5: ex a1,a2,a3 be Real st ( 0 > a1 or 0 > a2 or 0 > a3) & ((a1 + a2) + a3) = 1 & p0 = (((a1 * p1) + (a2 * p2)) + (a3 * p3)) by A2;

 ex a1,a2,a3 be Real st ( 0 > a1 or 0 > a2 or 0 > a3) & ((a1 + a2) + a3) = 1 & p0 = (((a1 * p1) + (a2 * p2)) + (a3 * p3)) by A5;

 hence thesis by A1, A3, Def11, Def12, Def13, A4;

 end;

 p in the carrier of ( TOP-REAL 2);

 then p in ( REAL 2) by EUCLID: 22;

 then

 A6: p in ( plane (p1,p2,p3)) by A1, Th54;

 then

 consider a2,a3 be Real such that

 A7: ((i1 + a2) + a3) = 1 & p = (((i1 * p1) + (a2 * p2)) + (a3 * p3)) by A1, Def11;

 assume

 A8: ( tricord1 (p1,p2,p3,p)) < 0 or ( tricord2 (p1,p2,p3,p)) < 0 or ( tricord3 (p1,p2,p3,p)) < 0 ;

 a2 = i2 & a3 = i3 by A1, A6, A7, Def12, Def13;

 hence thesis by A8, A7;

 end;

 theorem :: EUCLID_3:56



 Th56: for p1, p2, p3, p st ((p2 - p1),(p3 - p1)) are_lindependent2 holds p in ( Triangle (p1,p2,p3)) iff ( tricord1 (p1,p2,p3,p)) >= 0 & ( tricord2 (p1,p2,p3,p)) >= 0 & ( tricord3 (p1,p2,p3,p)) >= 0 & (( tricord1 (p1,p2,p3,p)) = 0 or ( tricord2 (p1,p2,p3,p)) = 0 or ( tricord3 (p1,p2,p3,p)) = 0 )

 proof

 let p1, p2, p3, p;

 assume

 A1: ((p2 - p1),(p3 - p1)) are_lindependent2 ;



 A2: for p0 holds p0 in ( Triangle (p1,p2,p3)) iff p0 in ( LSeg (p1,p2)) or p0 in ( LSeg (p2,p3)) or p0 in ( LSeg (p3,p1))

 proof

 let p0;

 p0 in ( Triangle (p1,p2,p3)) iff p0 in (( LSeg (p1,p2)) \/ ( LSeg (p2,p3))) or p0 in ( LSeg (p3,p1)) by XBOOLE_0:def 3;

 hence thesis by XBOOLE_0:def 3;

 end;

 thus p in ( Triangle (p1,p2,p3)) implies ( tricord1 (p1,p2,p3,p)) >= 0 & ( tricord2 (p1,p2,p3,p)) >= 0 & ( tricord3 (p1,p2,p3,p)) >= 0 & (( tricord1 (p1,p2,p3,p)) = 0 or ( tricord2 (p1,p2,p3,p)) = 0 or ( tricord3 (p1,p2,p3,p)) = 0 )

 proof

 set x = p;

 assume

 A3: p in ( Triangle (p1,p2,p3));

 A4:

 now

 per cases by A2, A3;

 case x in ( LSeg (p1,p2));

 then

 consider lambda be Real such that

 A5: x = (((1 - lambda) * p1) + (lambda * p2)) and

 A6: 0 <= lambda and

 A7: lambda <= 1;



 A8: p = ((((1 - lambda) * p1) + (lambda * p2)) + ( 0. ( TOP-REAL 2))) by A5, RLVECT_1: 4

 .= ((((1 - lambda) * p1) + (lambda * p2)) + ( 0 * p3)) by RLVECT_1: 10;



 A9: (((1 - lambda) + lambda) + 0 ) = 1;

 (1 - lambda) >= 0 by A7, XREAL_1: 48;

 hence ex a1,a2,a3 be Real st 0 <= a1 & 0 <= a2 & 0 <= a3 & ((a1 + a2) + a3) = 1 & (a1 = 0 or a2 = 0 or a3 = 0 ) & p = (((a1 * p1) + (a2 * p2)) + (a3 * p3)) by A6, A9, A8;

 end;

 case x in ( LSeg (p2,p3));

 then

 consider lambda be Real such that

 A10: x = (((1 - lambda) * p2) + (lambda * p3)) and

 A11: 0 <= lambda and

 A12: lambda <= 1;



 A13: p = ((( 0. ( TOP-REAL 2)) + ((1 - lambda) * p2)) + (lambda * p3)) by A10, RLVECT_1: 4

 .= ((( 0 * p1) + ((1 - lambda) * p2)) + (lambda * p3)) by RLVECT_1: 10;



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

 (1 - lambda) >= 0 by A12, XREAL_1: 48;

 hence ex a1,a2,a3 be Real st 0 <= a1 & 0 <= a2 & 0 <= a3 & ((a1 + a2) + a3) = 1 & (a1 = 0 or a2 = 0 or a3 = 0 ) & p = (((a1 * p1) + (a2 * p2)) + (a3 * p3)) by A11, A14, A13;

 end;

 case x in ( LSeg (p3,p1));

 then

 consider lambda be Real such that

 A15: x = (((1 - lambda) * p3) + (lambda * p1)) and

 A16: 0 <= lambda and

 A17: lambda <= 1;



 A18: p = (((lambda * p1) + ( 0. ( TOP-REAL 2))) + ((1 - lambda) * p3)) by A15, RLVECT_1: 4

 .= (((lambda * p1) + ( 0 * p2)) + ((1 - lambda) * p3)) by RLVECT_1: 10;



 A19: ((lambda + 0 ) + (1 - lambda)) = 1;

 (1 - lambda) >= 0 by A17, XREAL_1: 48;

 hence ex a1,a2,a3 be Real st 0 <= a1 & 0 <= a2 & 0 <= a3 & ((a1 + a2) + a3) = 1 & (a1 = 0 or a2 = 0 or a3 = 0 ) & p = (((a1 * p1) + (a2 * p2)) + (a3 * p3)) by A16, A19, A18;

 end;

 end;

 p in the carrier of ( TOP-REAL 2);

 then p in ( REAL 2) by EUCLID: 22;

 then p in ( plane (p1,p2,p3)) by A1, Th54;

 hence thesis by A1, A4, Def11, Def12, Def13;

 end;

 thus ( tricord1 (p1,p2,p3,p)) >= 0 & ( tricord2 (p1,p2,p3,p)) >= 0 & ( tricord3 (p1,p2,p3,p)) >= 0 & (( tricord1 (p1,p2,p3,p)) = 0 or ( tricord2 (p1,p2,p3,p)) = 0 or ( tricord3 (p1,p2,p3,p)) = 0 ) implies p in ( Triangle (p1,p2,p3))

 proof

 set p0 = p;

 assume that

 A20: ( tricord1 (p1,p2,p3,p)) >= 0 and

 A21: ( tricord2 (p1,p2,p3,p)) >= 0 and

 A22: ( tricord3 (p1,p2,p3,p)) >= 0 and

 A23: ( tricord1 (p1,p2,p3,p)) = 0 or ( tricord2 (p1,p2,p3,p)) = 0 or ( tricord3 (p1,p2,p3,p)) = 0 ;

 set i01 = ( tricord1 (p1,p2,p3,p0)), i02 = ( tricord2 (p1,p2,p3,p0)), i03 = ( tricord3 (p1,p2,p3,p0));

 p0 in the carrier of ( TOP-REAL 2);

 then p0 in ( REAL 2) by EUCLID: 22;

 then

 A24: p0 in ( plane (p1,p2,p3)) by A1, Th54;

 now

 per cases by A23;

 case ( tricord1 (p1,p2,p3,p)) = 0 ;

 then

 consider a2,a3 be Real such that

 A25: (( 0 + a2) + a3) = 1 and

 A26: p = ((( 0 * p1) + (a2 * p2)) + (a3 * p3)) by A1, A24, Def11;

 a2 = i02 by A1, A24, A25, A26, Def12;

 then

 A27: ((1 - a3) + a3) >= ( 0 + a3) by A21, A25, XREAL_1: 7;



 A28: p = ((( 0. ( TOP-REAL 2)) + (a2 * p2)) + (a3 * p3)) by A26, RLVECT_1: 10

 .= ((a2 * p2) + (a3 * p3)) by RLVECT_1: 4;

 a3 = i03 by A1, A24, A25, A26, Def13;

 hence p in ( LSeg (p1,p2)) or p in ( LSeg (p2,p3)) or p in ( LSeg (p3,p1)) by A22, A25, A28, A27;

 end;

 case ( tricord2 (p1,p2,p3,p)) = 0 ;

 then

 consider a1,a3 be Real such that

 A29: ((a1 + 0 ) + a3) = 1 and

 A30: p = (((a1 * p1) + ( 0 * p2)) + (a3 * p3)) by A1, A24, Def12;

 a1 = i01 by A1, A24, A29, A30, Def11;

 then

 A31: ((1 - a3) + a3) >= ( 0 + a3) by A20, A29, XREAL_1: 7;



 A32: p = (((a1 * p1) + ( 0. ( TOP-REAL 2))) + (a3 * p3)) by A30, RLVECT_1: 10

 .= ((a1 * p1) + (a3 * p3)) by RLVECT_1: 4;

 a3 = i03 by A1, A24, A29, A30, Def13;

 then p in { (((1 - lambda) * p1) + (lambda * p3)) where lambda be Real : 0 <= lambda & lambda <= 1 } by A22, A29, A32, A31;

 hence p in ( LSeg (p1,p2)) or p in ( LSeg (p2,p3)) or p in ( LSeg (p3,p1)) by RLTOPSP1:def 2;

 end;

 case ( tricord3 (p1,p2,p3,p)) = 0 ;

 then

 consider a1,a2 be Real such that

 A33: ((a1 + a2) + 0 ) = 1 and

 A34: p = (((a1 * p1) + (a2 * p2)) + ( 0 * p3)) by A1, A24, Def13;

 a1 = i01 by A1, A24, A33, A34, Def11;

 then

 A35: ((1 - a2) + a2) >= ( 0 + a2) by A20, A33, XREAL_1: 7;



 A36: p = (((a1 * p1) + (a2 * p2)) + ( 0. ( TOP-REAL 2))) by A34, RLVECT_1: 10

 .= ((a1 * p1) + (a2 * p2)) by RLVECT_1: 4;

 a2 = i02 by A1, A24, A33, A34, Def12;

 hence p in ( LSeg (p1,p2)) or p in ( LSeg (p2,p3)) or p in ( LSeg (p3,p1)) by A21, A33, A36, A35;

 end;

 end;

 hence thesis by A2;

 end;

 end;

 theorem :: EUCLID_3:57

 for p1, p2, p3, p st ((p2 - p1),(p3 - p1)) are_lindependent2 holds p in ( Triangle (p1,p2,p3)) iff ( tricord1 (p1,p2,p3,p)) = 0 & ( tricord2 (p1,p2,p3,p)) >= 0 & ( tricord3 (p1,p2,p3,p)) >= 0 or ( tricord1 (p1,p2,p3,p)) >= 0 & ( tricord2 (p1,p2,p3,p)) = 0 & ( tricord3 (p1,p2,p3,p)) >= 0 or ( tricord1 (p1,p2,p3,p)) >= 0 & ( tricord2 (p1,p2,p3,p)) >= 0 & ( tricord3 (p1,p2,p3,p)) = 0 by Th56;

 theorem :: EUCLID_3:58



 Th58: for p1, p2, p3, p st ((p2 - p1),(p3 - p1)) are_lindependent2 holds p in ( inside_of_triangle (p1,p2,p3)) iff ( tricord1 (p1,p2,p3,p)) > 0 & ( tricord2 (p1,p2,p3,p)) > 0 & ( tricord3 (p1,p2,p3,p)) > 0

 proof

 let p1, p2, p3, p;

 assume

 A1: ((p2 - p1),(p3 - p1)) are_lindependent2 ;



 A2: ( inside_of_triangle (p1,p2,p3)) c= { p0 where p0 be Point of ( TOP-REAL 2) : ex a1,a2,a3 be Real st ( 0 < a1 & 0 < a2 & 0 < a3) & ((a1 + a2) + a3) = 1 & p0 = (((a1 * p1) + (a2 * p2)) + (a3 * p3)) }

 proof

 let x be object;

 assume

 A3: x in ( inside_of_triangle (p1,p2,p3));

 then

 A4: not x in ( Triangle (p1,p2,p3)) by XBOOLE_0:def 5;

 x in ( closed_inside_of_triangle (p1,p2,p3)) by A3, XBOOLE_0:def 5;

 then

 consider p0 be Point of ( TOP-REAL 2) such that

 A5: p0 = x and

 A6: ex a1,a2,a3 be Real st 0 <= a1 & 0 <= a2 & 0 <= a3 & ((a1 + a2) + a3) = 1 & p0 = (((a1 * p1) + (a2 * p2)) + (a3 * p3));

 reconsider i01 = ( tricord1 (p1,p2,p3,p0)), i02 = ( tricord2 (p1,p2,p3,p0)), i03 = ( tricord3 (p1,p2,p3,p0)) as Real;

 consider a1,a2,a3 be Real such that

 A7: 0 <= a1 and

 A8: 0 <= a2 and

 A9: 0 <= a3 and

 A10: ((a1 + a2) + a3) = 1 & p0 = (((a1 * p1) + (a2 * p2)) + (a3 * p3)) by A6;

 p0 in the carrier of ( TOP-REAL 2);

 then p0 in ( REAL 2) by EUCLID: 22;

 then

 A11: p0 in ( plane (p1,p2,p3)) by A1, Th54;

 then

 A12: a1 = i01 by A1, A10, Def11;



 A13: a3 = i03 by A1, A10, A11, Def13;

 then

 A14: i02 <> 0 by A1, A4, A5, A7, A9, A12, Th56;



 A15: a2 = i02 by A1, A10, A11, Def12;

 then

 A16: i03 <> 0 by A1, A4, A5, A7, A8, A12, Th56;

 i01 <> 0 by A1, A4, A5, A8, A9, A15, A13, Th56;

 hence thesis by A5, A7, A8, A9, A10, A12, A15, A13, A14, A16;

 end;

 thus p in ( inside_of_triangle (p1,p2,p3)) implies ( tricord1 (p1,p2,p3,p)) > 0 & ( tricord2 (p1,p2,p3,p)) > 0 & ( tricord3 (p1,p2,p3,p)) > 0

 proof

 p in the carrier of ( TOP-REAL 2);

 then p in ( REAL 2) by EUCLID: 22;

 then

 A17: p in ( plane (p1,p2,p3)) by A1, Th54;

 assume

 A18: p in ( inside_of_triangle (p1,p2,p3));

 then p in ( closed_inside_of_triangle (p1,p2,p3)) by XBOOLE_0:def 5;

 then

 consider p0 be Point of ( TOP-REAL 2) such that

 A19: p0 = p and

 A20: ex a1,a2,a3 be Real st 0 <= a1 & 0 <= a2 & 0 <= a3 & ((a1 + a2) + a3) = 1 & p0 = (((a1 * p1) + (a2 * p2)) + (a3 * p3));

 not p in ( Triangle (p1,p2,p3)) by A18, XBOOLE_0:def 5;

 then not (( tricord1 (p1,p2,p3,p0)) >= 0 & ( tricord2 (p1,p2,p3,p0)) >= 0 & ( tricord3 (p1,p2,p3,p0)) >= 0 & (( tricord1 (p1,p2,p3,p0)) = 0 or ( tricord2 (p1,p2,p3,p0)) = 0 or ( tricord3 (p1,p2,p3,p0)) = 0 )) by A1, A19, Th56;

 hence thesis by A1, A19, A17, A20, Def11, Def12, Def13;

 end;

 { p0 where p0 be Point of ( TOP-REAL 2) : ex a1,a2,a3 be Real st 0 < a1 & 0 < a2 & 0 < a3 & ((a1 + a2) + a3) = 1 & p0 = (((a1 * p1) + (a2 * p2)) + (a3 * p3)) } c= ( inside_of_triangle (p1,p2,p3))

 proof

 let x be object;

 assume x in { p0 where p0 be Point of ( TOP-REAL 2) : ex a1,a2,a3 be Real st ( 0 < a1 & 0 < a2 & 0 < a3) & ((a1 + a2) + a3) = 1 & p0 = (((a1 * p1) + (a2 * p2)) + (a3 * p3)) };

 then

 consider p0 be Point of ( TOP-REAL 2) such that

 A21: x = p0 and

 A22: ex a1,a2,a3 be Real st 0 < a1 & 0 < a2 & 0 < a3 & ((a1 + a2) + a3) = 1 & p0 = (((a1 * p1) + (a2 * p2)) + (a3 * p3));



 A23: x in ( closed_inside_of_triangle (p1,p2,p3)) by A21, A22;

 set i01 = ( tricord1 (p1,p2,p3,p0)), i02 = ( tricord2 (p1,p2,p3,p0)), i03 = ( tricord3 (p1,p2,p3,p0));

 consider a01,a02,a03 be Real such that

 A24: 0 < a01 & 0 < a02 & 0 < a03 and

 A25: ((a01 + a02) + a03) = 1 & p0 = (((a01 * p1) + (a02 * p2)) + (a03 * p3)) by A22;

 p0 in the carrier of ( TOP-REAL 2);

 then p0 in ( REAL 2) by EUCLID: 22;

 then

 A26: p0 in ( plane (p1,p2,p3)) by A1, Th54;

 then

 A27: a03 = i03 by A1, A25, Def13;

 a01 = i01 & a02 = i02 by A1, A25, A26, Def11, Def12;

 then not x in ( Triangle (p1,p2,p3)) by A1, A21, A24, A27, Th56;

 hence thesis by A23, XBOOLE_0:def 5;

 end;

 then

 A28: ( inside_of_triangle (p1,p2,p3)) = { p0 where p0 be Point of ( TOP-REAL 2) : ex a1,a2,a3 be Real st ( 0 < a1 & 0 < a2 & 0 < a3) & ((a1 + a2) + a3) = 1 & p0 = (((a1 * p1) + (a2 * p2)) + (a3 * p3)) } by A2;

 thus ( tricord1 (p1,p2,p3,p)) > 0 & ( tricord2 (p1,p2,p3,p)) > 0 & ( tricord3 (p1,p2,p3,p)) > 0 implies p in ( inside_of_triangle (p1,p2,p3))

 proof

 reconsider i1 = ( tricord1 (p1,p2,p3,p)), i2 = ( tricord2 (p1,p2,p3,p)), i3 = ( tricord3 (p1,p2,p3,p)) as Real;

 assume

 A29: ( tricord1 (p1,p2,p3,p)) > 0 & ( tricord2 (p1,p2,p3,p)) > 0 & ( tricord3 (p1,p2,p3,p)) > 0 ;

 p in the carrier of ( TOP-REAL 2);

 then p in ( REAL 2) by EUCLID: 22;

 then

 A30: p in ( plane (p1,p2,p3)) by A1, Th54;

 then

 consider a2,a3 be Real such that

 A31: ((i1 + a2) + a3) = 1 & p = (((i1 * p1) + (a2 * p2)) + (a3 * p3)) by A1, Def11;

 a2 = i2 & a3 = i3 by A1, A30, A31, Def12, Def13;

 hence thesis by A28, A29, A31;

 end;

 end;

 theorem :: EUCLID_3:59

 for p1, p2, p3 st ((p2 - p1),(p3 - p1)) are_lindependent2 holds ( inside_of_triangle (p1,p2,p3)) is non empty

 proof

 let p1, p2, p3;

 assume

 A1: ((p2 - p1),(p3 - p1)) are_lindependent2 ;

 set p0 = ((((1 / 3) * p1) + ((1 / 3) * p2)) + ((1 / 3) * p3));

 set i01 = ( tricord1 (p1,p2,p3,p0)), i02 = ( tricord2 (p1,p2,p3,p0)), i03 = ( tricord3 (p1,p2,p3,p0));

 p0 in the carrier of ( TOP-REAL 2);

 then p0 in ( REAL 2) by EUCLID: 22;

 then

 A2: (((1 / 3) + (1 / 3)) + (1 / 3)) = 1 & p0 in ( plane (p1,p2,p3)) by A1, Th54;

 then

 A3: (1 / 3) = i03 by A1, Def13;

 (1 / 3) = i01 & (1 / 3) = i02 by A1, A2, Def11, Def12;

 hence thesis by A1, A3, Th58;

 end;