:: Angle and Triangle in {E}uclidian Topological Space
:: by Akihiro Kubo and Yatsuka Nakamura
::
:: Received May 29, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users


begin

definition
let z be complex number ;
func cpx2euc z ->  Point of (TOP-REAL 2) equals :: EUCLID_3:def 1
|[(Re z),(Im z)]|;
correctness
coherence
|[(Re z),(Im z)]| is Point of (TOP-REAL 2);
;
end;

:: deftheorem  defines cpx2euc EUCLID_3:def_1_:_
 for z being complex number holds cpx2euc z = |[(Re z),(Im z)]|;

definition
let p be Point of (TOP-REAL 2);
func euc2cpx p ->  Element of COMPLEX  equals :: EUCLID_3:def 2
(p `1) + ((p `2) * <i>);
correctness
coherence
(p `1) + ((p `2) * <i>) is Element of COMPLEX ;
by XCMPLX_0:def_2;
end;

:: deftheorem  defines euc2cpx EUCLID_3:def_2_:_
 for p being Point of (TOP-REAL 2) holds euc2cpx p = (p `1) + ((p `2) * <i>);

theorem Th1: :: EUCLID_3:1
for z being complex number holds euc2cpx (cpx2euc z) = z
proofend;

theorem Th2: :: EUCLID_3:2
for p being Point of (TOP-REAL 2) holds cpx2euc (euc2cpx p) = p
proofend;

theorem :: EUCLID_3:3
for z1, z2 being complex number st cpx2euc z1 = cpx2euc z2 holds
z1 = z2
proofend;

theorem Th4: :: EUCLID_3:4
for p1, p2 being Point of (TOP-REAL 2) st euc2cpx p1 = euc2cpx p2 holds
p1 = p2
proofend;

theorem Th5: :: EUCLID_3:5
for x1, x2 being Real holds cpx2euc (x1 + (x2 * <i>)) = |[x1,x2]|
proofend;

theorem Th6: :: EUCLID_3:6
for z1, z2 being complex number holds |[(Re (z1 + z2)),(Im (z1 + z2))]| = |[((Re z1) + (Re z2)),((Im z1) + (Im z2))]|
proofend;

theorem Th7: :: EUCLID_3:7
for z1, z2 being complex number holds cpx2euc (z1 + z2) = (cpx2euc z1) + (cpx2euc z2)
proofend;

theorem Th8: :: EUCLID_3:8
for p1, p2 being Point of (TOP-REAL 2) holds ((p1 + p2) `1) + (((p1 + p2) `2) * <i>) = ((p1 `1) + (p2 `1)) + (((p1 `2) + (p2 `2)) * <i>)
proofend;

theorem Th9: :: EUCLID_3:9
for p1, p2 being Point of (TOP-REAL 2) holds euc2cpx (p1 + p2) = (euc2cpx p1) + (euc2cpx p2)
proofend;

theorem Th10: :: EUCLID_3:10
for z being complex number holds |[(Re (- z)),(Im (- z))]| = |[(- (Re z)),(- (Im z))]|
proofend;

theorem Th11: :: EUCLID_3:11
for z being complex number holds cpx2euc (- z) = - (cpx2euc z)
proofend;

theorem Th12: :: EUCLID_3:12
for p being Point of (TOP-REAL 2) holds ((- p) `1) + (((- p) `2) * <i>) = (- (p `1)) + ((- (p `2)) * <i>)
proofend;

theorem Th13: :: EUCLID_3:13
for p being Point of (TOP-REAL 2) holds euc2cpx (- p) = - (euc2cpx p)
proofend;

theorem :: EUCLID_3:14
for z1, z2 being complex number holds cpx2euc (z1 - z2) = (cpx2euc z1) - (cpx2euc z2)
proofend;

theorem Th15: :: EUCLID_3:15
for p1, p2 being Point of (TOP-REAL 2) holds euc2cpx (p1 - p2) = (euc2cpx p1) - (euc2cpx p2)
proofend;

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

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

theorem :: EUCLID_3:18
for p being Point of (TOP-REAL 2) st euc2cpx p = 0c holds
p = 0. (TOP-REAL 2) by Th2, Th16;

theorem :: EUCLID_3:19
for z being complex number
for r being Real holds cpx2euc (r * z) = r * (cpx2euc z)
proofend;

theorem :: EUCLID_3:20
for r being Real
for p being Point of (TOP-REAL 2) holds euc2cpx (r * p) = r * (euc2cpx p)
proofend;

theorem Th21: :: EUCLID_3:21
for p being Point of (TOP-REAL 2) holds |.(euc2cpx p).| = sqrt (((p `1) ^2) + ((p `2) ^2))
proofend;

theorem :: EUCLID_3:22
for f being FinSequence of REAL st len f = 2 holds
|.f.| = sqrt (((f . 1) ^2) + ((f . 2) ^2))
proofend;

theorem :: EUCLID_3:23
for f being FinSequence of REAL
for p being Point of (TOP-REAL 2) st len f = 2 &amp; p = f holds
|.p.| = |.f.| ;

theorem :: EUCLID_3:24
for z being complex number holds |.(cpx2euc z).| = sqrt (((Re z) ^2) + ((Im z) ^2))
proofend;

theorem Th25: :: EUCLID_3:25
for p being Point of (TOP-REAL 2) holds |.(euc2cpx p).| = |.p.|
proofend;

definition
let p be Point of (TOP-REAL 2);
func Arg p ->  Real equals :: EUCLID_3:def 3
 Arg (euc2cpx p);
correctness
coherence
Arg (euc2cpx p) is Real;
;
end;

:: deftheorem  defines Arg EUCLID_3:def_3_:_
 for p being Point of (TOP-REAL 2) holds Arg p = Arg (euc2cpx p);

theorem :: EUCLID_3:26
for z being Element of COMPLEX
for p being Point of (TOP-REAL 2) st ( z = euc2cpx p or p = cpx2euc z ) holds
Arg z = Arg p
proofend;

theorem :: EUCLID_3:27
for x1, x2 being Real
for p being Point of (TOP-REAL 2) st x1 = |.p.| * (cos (Arg p)) &amp; x2 = |.p.| * (sin (Arg p)) holds
p = |[x1,x2]|
proofend;

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

theorem :: EUCLID_3:29
for p being Point of (TOP-REAL 2) st p <> 0. (TOP-REAL 2) holds
( ( Arg p < PI implies Arg (- p) = (Arg p) + PI ) &amp; ( Arg p >= PI implies Arg (- p) = (Arg p) - PI ) )
proofend;

theorem :: EUCLID_3:30
for p being Point of (TOP-REAL 2) st Arg p = 0 holds
( p = |[|.p.|,0]| &amp; p `2 = 0 )
proofend;

theorem Th31: :: EUCLID_3:31
for p being Point of (TOP-REAL 2) st p <> 0. (TOP-REAL 2) holds
( Arg p < PI iff Arg (- p) >= PI )
proofend;

theorem :: EUCLID_3:32
for p1, p2 being Point of (TOP-REAL 2) st ( p1 <> p2 or p1 - p2 <> 0. (TOP-REAL 2) ) holds
( Arg (p1 - p2) < PI iff Arg (p2 - p1) >= PI )
proofend;

theorem :: EUCLID_3:33
for p being Point of (TOP-REAL 2) holds
( Arg p in ].0,PI.[ iff p `2 > 0 )
proofend;

theorem :: EUCLID_3:34
for p1, p2 being Point of (TOP-REAL 2) st Arg p1 < PI &amp; Arg p2 < PI holds
Arg (p1 + p2) < PI
proofend;

definition
let p1, p2, p3 be Point of (TOP-REAL 2);
func angle (p1,p2,p3) ->  Real equals :: EUCLID_3:def 4
 angle ((euc2cpx p1),(euc2cpx p2),(euc2cpx p3));
correctness
coherence
angle ((euc2cpx p1),(euc2cpx p2),(euc2cpx p3)) is Real;
by XREAL_0:def_1;
end;

:: deftheorem  defines angle EUCLID_3:def_4_:_
 for p1, p2, p3 being Point of (TOP-REAL 2) holds angle (p1,p2,p3) = angle ((euc2cpx p1),(euc2cpx p2),(euc2cpx p3));

theorem :: EUCLID_3:35
for p1, p2, p3 being Point of (TOP-REAL 2) holds angle (p1,p2,p3) = angle ((p1 - p2),(0. (TOP-REAL 2)),(p3 - p2))
proofend;

theorem :: EUCLID_3:36
for p1, p2, p3 being Point of (TOP-REAL 2) st angle (p1,p2,p3) = 0 holds
( Arg (p1 - p2) = Arg (p3 - p2) &amp; angle (p3,p2,p1) = 0 )
proofend;

theorem :: EUCLID_3:37
for p1, p2, p3 being Point of (TOP-REAL 2) st angle (p1,p2,p3) <> 0 holds
angle (p3,p2,p1) = (2 * PI) - (angle (p1,p2,p3))
proofend;

theorem :: EUCLID_3:38
for p1, p2, p3 being Point of (TOP-REAL 2) st angle (p3,p2,p1) <> 0 holds
angle (p3,p2,p1) = (2 * PI) - (angle (p1,p2,p3))
proofend;

theorem Th39: :: EUCLID_3:39
for x, y being Element of COMPLEX holds Re (x .|. y) = ((Re x) * (Re y)) + ((Im x) * (Im y))
proofend;

theorem Th40: :: EUCLID_3:40
for x, y being Element of COMPLEX holds Im (x .|. y) = (- ((Re x) * (Im y))) + ((Im x) * (Re y))
proofend;

theorem Th41: :: EUCLID_3:41
for p, q being Point of (TOP-REAL 2) holds |(p,q)| = ((p `1) * (q `1)) + ((p `2) * (q `2))
proofend;

theorem Th42: :: EUCLID_3:42
for p1, p2 being Point of (TOP-REAL 2) holds |(p1,p2)| = Re ((euc2cpx p1) .|. (euc2cpx p2))
proofend;

theorem :: EUCLID_3:43
for p1, p2, p3 being Point of (TOP-REAL 2) st p1 <> 0. (TOP-REAL 2) &amp; 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 ) )
proofend;

theorem :: EUCLID_3:44
for p1, p2 being Point of (TOP-REAL 2) st p1 <> 0. (TOP-REAL 2) &amp; p2 <> 0. (TOP-REAL 2) holds
( ( ( not (- ((p1 `1) * (p2 `2))) + ((p1 `2) * (p2 `1)) = |.p1.| * |.p2.| &amp; not (- ((p1 `1) * (p2 `2))) + ((p1 `2) * (p2 `1)) = - (|.p1.| * |.p2.|) ) or angle (p1,(0. (TOP-REAL 2)),p2) = PI / 2 or angle (p1,(0. (TOP-REAL 2)),p2) = (3 / 2) * PI ) &amp; ( ( not angle (p1,(0. (TOP-REAL 2)),p2) = PI / 2 &amp; not angle (p1,(0. (TOP-REAL 2)),p2) = (3 / 2) * PI ) or (- ((p1 `1) * (p2 `2))) + ((p1 `2) * (p2 `1)) = |.p1.| * |.p2.| or (- ((p1 `1) * (p2 `2))) + ((p1 `2) * (p2 `1)) = - (|.p1.| * |.p2.|) ) )
proofend;

theorem :: EUCLID_3:45
for p1, p2, p3 being Point of (TOP-REAL 2) st p1 <> p2 &amp; p3 <> p2 holds
( |((p1 - p2),(p3 - p2))| = 0 iff ( angle (p1,p2,p3) = PI / 2 or angle (p1,p2,p3) = (3 / 2) * PI ) )
proofend;

:: [WP: ] Pythagorean_Theorem
theorem :: EUCLID_3:46
for p1, p2, p3 being Point of (TOP-REAL 2) st p1 <> p2 &amp; p3 <> p2 &amp; ( angle (p1,p2,p3) = PI / 2 or angle (p1,p2,p3) = (3 / 2) * PI ) holds
(|.(p1 - p2).| ^2) + (|.(p3 - p2).| ^2) = |.(p1 - p3).| ^2
proofend;

theorem :: EUCLID_3:47
for p1, p2, p3 being Point of (TOP-REAL 2) st p2 <> p1 &amp; p1 <> p3 &amp; p3 <> p2 &amp; angle (p2,p1,p3) < PI holds
((angle (p2,p1,p3)) + (angle (p1,p3,p2))) + (angle (p3,p2,p1)) = PI
proofend;

definition
let n be Element of NAT ;
let p1, p2, p3 be Point of (TOP-REAL n);
func Triangle (p1,p2,p3) ->  Subset of (TOP-REAL n) equals :: EUCLID_3:def 5
((LSeg (p1,p2)) \/ (LSeg (p2,p3))) \/ (LSeg (p3,p1));
correctness
coherence
((LSeg (p1,p2)) \/ (LSeg (p2,p3))) \/ (LSeg (p3,p1)) is Subset of (TOP-REAL n);
;
end;

:: deftheorem  defines Triangle EUCLID_3:def_5_:_
 for n being Element of NAT
for p1, p2, p3 being Point of (TOP-REAL n) holds Triangle (p1,p2,p3) = ((LSeg (p1,p2)) \/ (LSeg (p2,p3))) \/ (LSeg (p3,p1));

definition
let n be Element of NAT ;
let p1, p2, p3 be Point of (TOP-REAL n);
func closed_inside_of_triangle (p1,p2,p3) ->  Subset of (TOP-REAL n) equals :: EUCLID_3:def 6
 {  p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st
( 0 <= a1 &amp; 0 <= a2 &amp; 0 <= a3 &amp; (a1 + a2) + a3 = 1 &amp; p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )  }  ;
correctness
coherence
{  p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st
( 0 <= a1 &amp; 0 <= a2 &amp; 0 <= a3 &amp; (a1 + a2) + a3 = 1 &amp; p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )  }  is Subset of (TOP-REAL n);
proofend;
end;

:: deftheorem  defines closed_inside_of_triangle EUCLID_3:def_6_:_
 for n being Element of NAT
for p1, p2, p3 being Point of (TOP-REAL n) holds closed_inside_of_triangle (p1,p2,p3) =  {  p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st
( 0 <= a1 &amp; 0 <= a2 &amp; 0 <= a3 &amp; (a1 + a2) + a3 = 1 &amp; p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )  }  ;

definition
let n be Element of NAT ;
let p1, p2, p3 be Point of (TOP-REAL n);
func inside_of_triangle (p1,p2,p3) ->  Subset of (TOP-REAL n) equals :: EUCLID_3:def 7
(closed_inside_of_triangle (p1,p2,p3)) \ (Triangle (p1,p2,p3));
correctness
coherence
(closed_inside_of_triangle (p1,p2,p3)) \ (Triangle (p1,p2,p3)) is Subset of (TOP-REAL n);
;
end;

:: deftheorem  defines inside_of_triangle EUCLID_3:def_7_:_
 for n being Element of NAT
for p1, p2, p3 being Point of (TOP-REAL n) holds inside_of_triangle (p1,p2,p3) = (closed_inside_of_triangle (p1,p2,p3)) \ (Triangle (p1,p2,p3));

definition
let n be Element of NAT ;
let p1, p2, p3 be Point of (TOP-REAL n);
func outside_of_triangle (p1,p2,p3) ->  Subset of (TOP-REAL n) equals :: EUCLID_3:def 8
 {  p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st
( ( 0 > a1 or 0 > a2 or 0 > a3 ) &amp; (a1 + a2) + a3 = 1 &amp; p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )  }  ;
correctness
coherence
{  p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st
( ( 0 > a1 or 0 > a2 or 0 > a3 ) &amp; (a1 + a2) + a3 = 1 &amp; p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )  }  is Subset of (TOP-REAL n);
proofend;
end;

:: deftheorem  defines outside_of_triangle EUCLID_3:def_8_:_
 for n being Element of NAT
for p1, p2, p3 being Point of (TOP-REAL n) holds outside_of_triangle (p1,p2,p3) =  {  p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st
( ( 0 > a1 or 0 > a2 or 0 > a3 ) &amp; (a1 + a2) + a3 = 1 &amp; p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )  }  ;

definition
let n be Element of NAT ;
let p1, p2, p3 be Point of (TOP-REAL n);
func plane (p1,p2,p3) ->  Subset of (TOP-REAL n) equals :: EUCLID_3:def 9
(outside_of_triangle (p1,p2,p3)) \/ (closed_inside_of_triangle (p1,p2,p3));
correctness
coherence
(outside_of_triangle (p1,p2,p3)) \/ (closed_inside_of_triangle (p1,p2,p3)) is Subset of (TOP-REAL n);
;
end;

:: deftheorem  defines plane EUCLID_3:def_9_:_
 for n being Element of NAT
for p1, p2, p3 being Point of (TOP-REAL n) holds plane (p1,p2,p3) = (outside_of_triangle (p1,p2,p3)) \/ (closed_inside_of_triangle (p1,p2,p3));

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

theorem :: EUCLID_3:49
for n being Element of NAT
for p1, p2, p3 being Point of (TOP-REAL n) holds Triangle (p1,p2,p3) c= closed_inside_of_triangle (p1,p2,p3)
proofend;

definition
let n be Element of NAT ;
let q1, q2 be Point of (TOP-REAL n);
predq1,q2 are_lindependent2  means :Def10: :: EUCLID_3:def 10
 for a1, a2 being Real st (a1 * q1) + (a2 * q2) = 0. (TOP-REAL n) holds
( a1 = 0 &amp; a2 = 0 );
end;

:: deftheorem Def10 defines are_lindependent2 EUCLID_3:def_10_:_
 for n being Element of NAT
for q1, q2 being Point of (TOP-REAL n) holds
( q1,q2 are_lindependent2 iff for a1, a2 being Real st (a1 * q1) + (a2 * q2) = 0. (TOP-REAL n) holds
( a1 = 0 &amp; a2 = 0 ) );

notation
let n be Element of NAT ;
let q1, q2 be Point of (TOP-REAL n);
antonym q1,q2 are_ldependent2 for q1,q2 are_lindependent2 ;
end;

theorem Th50: :: EUCLID_3:50
for n being Element of NAT
for q1, q2 being Point of (TOP-REAL n) st q1,q2 are_lindependent2 holds
( q1 <> q2 &amp; q1 <> 0. (TOP-REAL n) &amp; q2 <> 0. (TOP-REAL n) )
proofend;

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

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

theorem :: EUCLID_3:53
for n being Element of NAT
for p1, p2, p3 being Point of (TOP-REAL n) holds plane (p1,p2,p3) =  {  p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 &amp; p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )  }
proofend;

theorem Th54: :: EUCLID_3:54
for p1, p2, p3 being Point of (TOP-REAL 2) st p2 - p1,p3 - p1 are_lindependent2 holds
plane (p1,p2,p3) = REAL 2
proofend;

definition
let n be Element of NAT ;
let p1, p2, p3, p be Point of (TOP-REAL n);
assume A1: ( p2 - p1,p3 - p1 are_lindependent2 &amp; p in plane (p1,p2,p3) ) ;
func tricord1 (p1,p2,p3,p) ->  Real means :Def11: :: EUCLID_3:def 11
 ex a2, a3 being Real st
( (it + a2) + a3 = 1 &amp; p = ((it * p1) + (a2 * p2)) + (a3 * p3) );
existence
 ex b1, a2, a3 being Real st
( (b1 + a2) + a3 = 1 &amp; p = ((b1 * p1) + (a2 * p2)) + (a3 * p3) )
proofend;
uniqueness
 for b1, b2 being Real st ex a2, a3 being Real st
( (b1 + a2) + a3 = 1 &amp; p = ((b1 * p1) + (a2 * p2)) + (a3 * p3) ) &amp; ex a2, a3 being Real st
( (b2 + a2) + a3 = 1 &amp; p = ((b2 * p1) + (a2 * p2)) + (a3 * p3) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def11 defines tricord1 EUCLID_3:def_11_:_
 for n being Element of NAT
for p1, p2, p3, p being Point of (TOP-REAL n) st p2 - p1,p3 - p1 are_lindependent2 &amp; p in plane (p1,p2,p3) holds
for b6 being Real holds
( b6 = tricord1 (p1,p2,p3,p) iff ex a2, a3 being Real st
( (b6 + a2) + a3 = 1 &amp; p = ((b6 * p1) + (a2 * p2)) + (a3 * p3) ) );

definition
let n be Element of NAT ;
let p1, p2, p3, p be Point of (TOP-REAL n);
assume A1: ( p2 - p1,p3 - p1 are_lindependent2 &amp; p in plane (p1,p2,p3) ) ;
func tricord2 (p1,p2,p3,p) ->  Real means :Def12: :: EUCLID_3:def 12
 ex a1, a3 being Real st
( (a1 + it) + a3 = 1 &amp; p = ((a1 * p1) + (it * p2)) + (a3 * p3) );
existence
 ex b1, a1, a3 being Real st
( (a1 + b1) + a3 = 1 &amp; p = ((a1 * p1) + (b1 * p2)) + (a3 * p3) )
proofend;
uniqueness
 for b1, b2 being Real st ex a1, a3 being Real st
( (a1 + b1) + a3 = 1 &amp; p = ((a1 * p1) + (b1 * p2)) + (a3 * p3) ) &amp; ex a1, a3 being Real st
( (a1 + b2) + a3 = 1 &amp; p = ((a1 * p1) + (b2 * p2)) + (a3 * p3) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def12 defines tricord2 EUCLID_3:def_12_:_
 for n being Element of NAT
for p1, p2, p3, p being Point of (TOP-REAL n) st p2 - p1,p3 - p1 are_lindependent2 &amp; p in plane (p1,p2,p3) holds
for b6 being Real holds
( b6 = tricord2 (p1,p2,p3,p) iff ex a1, a3 being Real st
( (a1 + b6) + a3 = 1 &amp; p = ((a1 * p1) + (b6 * p2)) + (a3 * p3) ) );

definition
let n be Element of NAT ;
let p1, p2, p3, p be Point of (TOP-REAL n);
assume A1: ( p2 - p1,p3 - p1 are_lindependent2 &amp; p in plane (p1,p2,p3) ) ;
func tricord3 (p1,p2,p3,p) ->  Real means :Def13: :: EUCLID_3:def 13
 ex a1, a2 being Real st
( (a1 + a2) + it = 1 &amp; p = ((a1 * p1) + (a2 * p2)) + (it * p3) );
existence
 ex b1, a1, a2 being Real st
( (a1 + a2) + b1 = 1 &amp; p = ((a1 * p1) + (a2 * p2)) + (b1 * p3) )
proofend;
uniqueness
 for b1, b2 being Real st ex a1, a2 being Real st
( (a1 + a2) + b1 = 1 &amp; p = ((a1 * p1) + (a2 * p2)) + (b1 * p3) ) &amp; ex a1, a2 being Real st
( (a1 + a2) + b2 = 1 &amp; p = ((a1 * p1) + (a2 * p2)) + (b2 * p3) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def13 defines tricord3 EUCLID_3:def_13_:_
 for n being Element of NAT
for p1, p2, p3, p being Point of (TOP-REAL n) st p2 - p1,p3 - p1 are_lindependent2 &amp; p in plane (p1,p2,p3) holds
for b6 being Real holds
( b6 = tricord3 (p1,p2,p3,p) iff ex a1, a2 being Real st
( (a1 + a2) + b6 = 1 &amp; p = ((a1 * p1) + (a2 * p2)) + (b6 * p3) ) );

definition
let p1, p2, p3 be Point of (TOP-REAL 2);
func trcmap1 (p1,p2,p3) ->  Function of (TOP-REAL 2),R^1 means :: EUCLID_3:def 14
 for p being Point of (TOP-REAL 2) holds it . p = tricord1 (p1,p2,p3,p);
existence
 ex b1 being Function of (TOP-REAL 2),R^1 st
for p being Point of (TOP-REAL 2) holds b1 . p = tricord1 (p1,p2,p3,p)
proofend;
uniqueness
 for b1, b2 being Function of (TOP-REAL 2),R^1 st ( for p being Point of (TOP-REAL 2) holds b1 . p = tricord1 (p1,p2,p3,p) ) &amp; ( for p being Point of (TOP-REAL 2) holds b2 . p = tricord1 (p1,p2,p3,p) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines trcmap1 EUCLID_3:def_14_:_
 for p1, p2, p3 being Point of (TOP-REAL 2)
for b4 being Function of (TOP-REAL 2),R^1 holds
( b4 = trcmap1 (p1,p2,p3) iff for p being Point of (TOP-REAL 2) holds b4 . p = tricord1 (p1,p2,p3,p) );

definition
let p1, p2, p3 be Point of (TOP-REAL 2);
func trcmap2 (p1,p2,p3) ->  Function of (TOP-REAL 2),R^1 means :: EUCLID_3:def 15
 for p being Point of (TOP-REAL 2) holds it . p = tricord2 (p1,p2,p3,p);
existence
 ex b1 being Function of (TOP-REAL 2),R^1 st
for p being Point of (TOP-REAL 2) holds b1 . p = tricord2 (p1,p2,p3,p)
proofend;
uniqueness
 for b1, b2 being Function of (TOP-REAL 2),R^1 st ( for p being Point of (TOP-REAL 2) holds b1 . p = tricord2 (p1,p2,p3,p) ) &amp; ( for p being Point of (TOP-REAL 2) holds b2 . p = tricord2 (p1,p2,p3,p) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines trcmap2 EUCLID_3:def_15_:_
 for p1, p2, p3 being Point of (TOP-REAL 2)
for b4 being Function of (TOP-REAL 2),R^1 holds
( b4 = trcmap2 (p1,p2,p3) iff for p being Point of (TOP-REAL 2) holds b4 . p = tricord2 (p1,p2,p3,p) );

definition
let p1, p2, p3 be Point of (TOP-REAL 2);
func trcmap3 (p1,p2,p3) ->  Function of (TOP-REAL 2),R^1 means :: EUCLID_3:def 16
 for p being Point of (TOP-REAL 2) holds it . p = tricord3 (p1,p2,p3,p);
existence
 ex b1 being Function of (TOP-REAL 2),R^1 st
for p being Point of (TOP-REAL 2) holds b1 . p = tricord3 (p1,p2,p3,p)
proofend;
uniqueness
 for b1, b2 being Function of (TOP-REAL 2),R^1 st ( for p being Point of (TOP-REAL 2) holds b1 . p = tricord3 (p1,p2,p3,p) ) &amp; ( for p being Point of (TOP-REAL 2) holds b2 . p = tricord3 (p1,p2,p3,p) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines trcmap3 EUCLID_3:def_16_:_
 for p1, p2, p3 being Point of (TOP-REAL 2)
for b4 being Function of (TOP-REAL 2),R^1 holds
( b4 = trcmap3 (p1,p2,p3) iff for p being Point of (TOP-REAL 2) holds b4 . p = tricord3 (p1,p2,p3,p) );

theorem :: EUCLID_3:55
for p1, p2, p3, p being Point of (TOP-REAL 2) 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 ) )
proofend;

theorem Th56: :: EUCLID_3:56
for p1, p2, p3, p being Point of (TOP-REAL 2) st p2 - p1,p3 - p1 are_lindependent2 holds
( p in Triangle (p1,p2,p3) iff ( tricord1 (p1,p2,p3,p) >= 0 &amp; tricord2 (p1,p2,p3,p) >= 0 &amp; tricord3 (p1,p2,p3,p) >= 0 &amp; ( tricord1 (p1,p2,p3,p) = 0 or tricord2 (p1,p2,p3,p) = 0 or tricord3 (p1,p2,p3,p) = 0 ) ) )
proofend;

theorem :: EUCLID_3:57
for p1, p2, p3, p being Point of (TOP-REAL 2) st p2 - p1,p3 - p1 are_lindependent2 holds
( p in Triangle (p1,p2,p3) iff ( ( tricord1 (p1,p2,p3,p) = 0 &amp; tricord2 (p1,p2,p3,p) >= 0 &amp; tricord3 (p1,p2,p3,p) >= 0 ) or ( tricord1 (p1,p2,p3,p) >= 0 &amp; tricord2 (p1,p2,p3,p) = 0 &amp; tricord3 (p1,p2,p3,p) >= 0 ) or ( tricord1 (p1,p2,p3,p) >= 0 &amp; tricord2 (p1,p2,p3,p) >= 0 &amp; tricord3 (p1,p2,p3,p) = 0 ) ) ) by Th56;

theorem Th58: :: EUCLID_3:58
for p1, p2, p3, p being Point of (TOP-REAL 2) st p2 - p1,p3 - p1 are_lindependent2 holds
( p in inside_of_triangle (p1,p2,p3) iff ( tricord1 (p1,p2,p3,p) > 0 &amp; tricord2 (p1,p2,p3,p) > 0 &amp; tricord3 (p1,p2,p3,p) > 0 ) )
proofend;

theorem :: EUCLID_3:59
for p1, p2, p3 being Point of (TOP-REAL 2) st p2 - p1,p3 - p1 are_lindependent2 holds
not inside_of_triangle (p1,p2,p3) is empty
proofend;