:: EUCLID_3 semantic presentation

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
proof
let z be complex number ; ::_thesis: euc2cpx (cpx2euc z) = z
 ( |[(Re z),(Im z)]| `1 = Re z & |[(Re z),(Im z)]| `2 = Im z ) by EUCLID:52;
hence  euc2cpx (cpx2euc z) = z by COMPLEX1:13; ::_thesis: verum
end;

theorem Th2: :: EUCLID_3:2
for p being Point of (TOP-REAL 2) holds cpx2euc (euc2cpx p) = p
proof
let p be Point of (TOP-REAL 2); ::_thesis: cpx2euc (euc2cpx p) = p
 ( Re ((p `1) + ((p `2) * <i>)) = p `1 & Im ((p `1) + ((p `2) * <i>)) = p `2 ) by COMPLEX1:12;
hence  cpx2euc (euc2cpx p) = p by EUCLID:53; ::_thesis: verum
end;

theorem :: EUCLID_3:3
for z1, z2 being complex number st cpx2euc z1 = cpx2euc z2 holds
z1 = z2
proof
let z1, z2 be complex number ; ::_thesis: ( cpx2euc z1 = cpx2euc z2 implies z1 = z2 )
assume A1: cpx2euc z1 = cpx2euc z2 ; ::_thesis: z1 = z2
 z2 = euc2cpx (cpx2euc z2) by Th1;
hence  z1 = z2 by A1, Th1; ::_thesis: verum
end;

theorem Th4: :: EUCLID_3:4
for p1, p2 being Point of (TOP-REAL 2) st euc2cpx p1 = euc2cpx p2 holds
p1 = p2
proof
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( euc2cpx p1 = euc2cpx p2 implies p1 = p2 )
assume A1: euc2cpx p1 = euc2cpx p2 ; ::_thesis: p1 = p2
 p2 = cpx2euc (euc2cpx p2) by Th2;
hence  p1 = p2 by A1, Th2; ::_thesis: verum
end;

theorem Th5: :: EUCLID_3:5
for x1, x2 being Real holds cpx2euc (x1 + (x2 * <i>)) = |[x1,x2]|
proof
let x1, x2 be Real; ::_thesis: cpx2euc (x1 + (x2 * <i>)) = |[x1,x2]|
 Re (x1 + (x2 * <i>)) = x1 by COMPLEX1:12;
hence  cpx2euc (x1 + (x2 * <i>)) = |[x1,x2]| by COMPLEX1:12; ::_thesis: verum
end;

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))]|
proof
let z1, z2 be complex number ; ::_thesis: |[(Re (z1 + z2)),(Im (z1 + z2))]| = |[((Re z1) + (Re z2)),((Im z1) + (Im z2))]|
 |[(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  |[(Re (z1 + z2)),(Im (z1 + z2))]| = |[((Re z1) + (Re z2)),((Im z1) + (Im z2))]| by A1, EUCLID:53; ::_thesis: verum
end;

theorem Th7: :: EUCLID_3:7
for z1, z2 being complex number holds cpx2euc (z1 + z2) = (cpx2euc z1) + (cpx2euc z2)
proof
let z1, z2 be complex number ; ::_thesis: cpx2euc (z1 + z2) = (cpx2euc z1) + (cpx2euc z2)
 (cpx2euc z1) + (cpx2euc z2) = |[((Re z1) + (Re z2)),((Im z1) + (Im z2))]| by EUCLID:56;
hence  cpx2euc (z1 + z2) = (cpx2euc z1) + (cpx2euc z2) by Th6; ::_thesis: verum
end;

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>)
proof
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ((p1 + p2) `1) + (((p1 + p2) `2) * <i>) = ((p1 `1) + (p2 `1)) + (((p1 `2) + (p2 `2)) * <i>)
A1: p1 + p2 = |[((p1 `1) + (p2 `1)),((p1 `2) + (p2 `2))]| by EUCLID:55;
A2: Im (((p1 `1) + (p2 `1)) + (((p1 `2) + (p2 `2)) * <i>)) = (p1 `2) + (p2 `2) by COMPLEX1:12;
A3: ( Im (((p1 + p2) `1) + (((p1 + p2) `2) * <i>)) = (p1 + p2) `2 & Re (((p1 `1) + (p2 `1)) + (((p1 `2) + (p2 `2)) * <i>)) = (p1 `1) + (p2 `1) ) by COMPLEX1:12;
 Re (((p1 + p2) `1) + (((p1 + p2) `2) * <i>)) = (p1 + p2) `1 by COMPLEX1:12;
then  Re (((p1 + p2) `1) + (((p1 + p2) `2) * <i>)) = (p1 `1) + (p2 `1) by A1, EUCLID:52;
hence  ((p1 + p2) `1) + (((p1 + p2) `2) * <i>) = ((p1 `1) + (p2 `1)) + (((p1 `2) + (p2 `2)) * <i>) by A1, A3, A2, COMPLEX1:3, EUCLID:52; ::_thesis: verum
end;

theorem Th9: :: EUCLID_3:9
for p1, p2 being Point of (TOP-REAL 2) holds euc2cpx (p1 + p2) = (euc2cpx p1) + (euc2cpx p2)
proof
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: euc2cpx (p1 + p2) = (euc2cpx p1) + (euc2cpx p2)
 euc2cpx (p1 + p2) = ((p1 `1) + (p2 `1)) + (((p1 `2) + (p2 `2)) * <i>) by Th8;
hence  euc2cpx (p1 + p2) = (euc2cpx p1) + (euc2cpx p2) ; ::_thesis: verum
end;

theorem Th10: :: EUCLID_3:10
for z being complex number holds |[(Re (- z)),(Im (- z))]| = |[(- (Re z)),(- (Im z))]|
proof
let z be complex number ; ::_thesis: |[(Re (- z)),(Im (- z))]| = |[(- (Re z)),(- (Im z))]|
 |[(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  |[(Re (- z)),(Im (- z))]| = |[(- (Re z)),(- (Im z))]| by A1, EUCLID:53; ::_thesis: verum
end;

theorem Th11: :: EUCLID_3:11
for z being complex number holds cpx2euc (- z) = - (cpx2euc z)
proof
let z be complex number ; ::_thesis: cpx2euc (- z) = - (cpx2euc z)
 - (cpx2euc z) = |[(- (Re z)),(- (Im z))]| by EUCLID:60;
hence  cpx2euc (- z) = - (cpx2euc z) by Th10; ::_thesis: verum
end;

theorem Th12: :: EUCLID_3:12
for p being Point of (TOP-REAL 2) holds ((- p) `1) + (((- p) `2) * <i>) = (- (p `1)) + ((- (p `2)) * <i>)
proof
let p be Point of (TOP-REAL 2); ::_thesis: ((- p) `1) + (((- p) `2) * <i>) = (- (p `1)) + ((- (p `2)) * <i>)
A1: - p = |[(- (p `1)),(- (p `2))]| by EUCLID:59;
 (- (p `1)) + ((- (p `2)) * <i>) = (- (p `1)) + ((- (p `2)) * <i>) ;
then A2: ( Re ((- (p `1)) + (- ((p `2) * <i>))) = - (p `1) & Im ((- (p `1)) + (- ((p `2) * <i>))) = - (p `2) ) by COMPLEX1:12;
 Re (((- p) `1) + (((- p) `2) * <i>)) = (- p) `1 by COMPLEX1:12;
then  ( Im (((- p) `1) + (((- p) `2) * <i>)) = (- p) `2 & Re (((- p) `1) + (((- p) `2) * <i>)) = - (p `1) ) by A1, COMPLEX1:12, EUCLID:52;
hence  ((- p) `1) + (((- p) `2) * <i>) = (- (p `1)) + ((- (p `2)) * <i>) by A1, A2, COMPLEX1:3, EUCLID:52; ::_thesis: verum
end;

theorem Th13: :: EUCLID_3:13
for p being Point of (TOP-REAL 2) holds euc2cpx (- p) = - (euc2cpx p)
proof
let p be Point of (TOP-REAL 2); ::_thesis: euc2cpx (- p) = - (euc2cpx p)
 - (euc2cpx p) = (- (p `1)) + ((- (p `2)) * <i>) ;
hence  euc2cpx (- p) = - (euc2cpx p) by Th12; ::_thesis: verum
end;

theorem :: EUCLID_3:14
for z1, z2 being complex number holds cpx2euc (z1 - z2) = (cpx2euc z1) - (cpx2euc z2)
proof
let z1, z2 be complex number ; ::_thesis: cpx2euc (z1 - z2) = (cpx2euc z1) - (cpx2euc z2)
thus  cpx2euc (z1 - z2) = cpx2euc (z1 + (- z2))
.= (cpx2euc z1) + (cpx2euc (- z2)) by Th7
.= (cpx2euc z1) - (cpx2euc z2) by Th11 ; ::_thesis: verum
end;

theorem Th15: :: EUCLID_3:15
for p1, p2 being Point of (TOP-REAL 2) holds euc2cpx (p1 - p2) = (euc2cpx p1) - (euc2cpx p2)
proof
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: euc2cpx (p1 - p2) = (euc2cpx p1) - (euc2cpx p2)
thus  euc2cpx (p1 - p2) = (euc2cpx p1) + (euc2cpx (- p2)) by Th9
.= (euc2cpx p1) + (- (euc2cpx p2)) by Th13
.= (euc2cpx p1) - (euc2cpx p2) ; ::_thesis: verum
end;

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)
proof
let z be complex number ; ::_thesis: for r being Real holds cpx2euc (r * z) = r * (cpx2euc z)
let r be Real; ::_thesis: cpx2euc (r * z) = r * (cpx2euc z)
A1: ( (cpx2euc z) `1 = Re z & (cpx2euc z) `2 = Im z ) by EUCLID:52;
 r = r + (0 * <i>) ;
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  cpx2euc (r * z) = r * (cpx2euc z) by A3, A1, EUCLID:57; ::_thesis: verum
end;

theorem :: EUCLID_3:20
for r being Real
for p being Point of (TOP-REAL 2) holds euc2cpx (r * p) = r * (euc2cpx p)
proof
let r be Real; ::_thesis: for p being Point of (TOP-REAL 2) holds euc2cpx (r * p) = r * (euc2cpx p)
let p be Point of (TOP-REAL 2); ::_thesis: euc2cpx (r * p) = r * (euc2cpx p)
 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  euc2cpx (r * p) = r * (euc2cpx p) ; ::_thesis: verum
end;

theorem Th21: :: EUCLID_3:21
for p being Point of (TOP-REAL 2) holds |.(euc2cpx p).| = sqrt (((p `1) ^2) + ((p `2) ^2))
proof
let p be Point of (TOP-REAL 2); ::_thesis: |.(euc2cpx p).| = sqrt (((p `1) ^2) + ((p `2) ^2))
 Re (euc2cpx p) = p `1 by COMPLEX1:12;
hence  |.(euc2cpx p).| = sqrt (((p `1) ^2) + ((p `2) ^2)) by COMPLEX1:12; ::_thesis: verum
end;

theorem :: EUCLID_3:22
for f being FinSequence of REAL st len f = 2 holds
|.f.| = sqrt (((f . 1) ^2) + ((f . 2) ^2))
proof
let f be FinSequence of REAL ; ::_thesis: ( len f = 2 implies |.f.| = sqrt (((f . 1) ^2) + ((f . 2) ^2)) )
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;
assume  len f = 2 ; ::_thesis: |.f.| = sqrt (((f . 1) ^2) + ((f . 2) ^2))
then  sqr f = <*((f . 1) ^2),((f . 2) ^2)*> by A1, A2, FINSEQ_1:44;
then  Sum (sqr f) = Sum (<*((f . 1) ^2)*> ^ <*((f . 2) ^2)*>) by FINSEQ_1:def_9
.= (Sum <*((f . 1) ^2)*>) + ((f . 2) ^2) by RVSUM_1:74
.= ((f . 1) ^2) + ((f . 2) ^2) by RVSUM_1:73 ;
hence  |.f.| = sqrt (((f . 1) ^2) + ((f . 2) ^2)) ; ::_thesis: verum
end;

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

theorem :: EUCLID_3:24
for z being complex number holds |.(cpx2euc z).| = sqrt (((Re z) ^2) + ((Im z) ^2))
proof
let z be complex number ; ::_thesis: |.(cpx2euc z).| = sqrt (((Re z) ^2) + ((Im z) ^2))
 ( |[(Re z),(Im z)]| `1 = Re z & |[(Re z),(Im z)]| `2 = Im z ) by EUCLID:52;
hence  |.(cpx2euc z).| = sqrt (((Re z) ^2) + ((Im z) ^2)) by JGRAPH_3:1; ::_thesis: verum
end;

theorem Th25: :: EUCLID_3:25
for p being Point of (TOP-REAL 2) holds |.(euc2cpx p).| = |.p.|
proof
let p be Point of (TOP-REAL 2); ::_thesis: |.(euc2cpx p).| = |.p.|
 |.p.| = sqrt (((p `1) ^2) + ((p `2) ^2)) by JGRAPH_3:1;
hence  |.(euc2cpx p).| = |.p.| by Th21; ::_thesis: verum
end;

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
proof
let z be Element of COMPLEX ; ::_thesis: for p being Point of (TOP-REAL 2) st ( z = euc2cpx p or p = cpx2euc z ) holds
Arg z = Arg p
let p be Point of (TOP-REAL 2); ::_thesis: ( ( z = euc2cpx p or p = cpx2euc z ) implies Arg z = Arg p )
assume A1: ( z = euc2cpx p or p = cpx2euc z ) ; ::_thesis: Arg z = Arg p
percases ( z = euc2cpx p or p = cpx2euc z ) by A1;
suppose z = euc2cpx p ; ::_thesis: Arg z = Arg p
hence  Arg z = Arg p ; ::_thesis: verum
end;
suppose p = cpx2euc z ; ::_thesis: Arg z = Arg p
hence  Arg z = Arg p by Th1; ::_thesis: verum
end;
end;
end;

theorem :: EUCLID_3:27
for x1, x2 being Real
for p being Point of (TOP-REAL 2) st x1 = |.p.| * (cos (Arg p)) & x2 = |.p.| * (sin (Arg p)) holds
p = |[x1,x2]|
proof
let x1, x2 be Real; ::_thesis: for p being Point of (TOP-REAL 2) st x1 = |.p.| * (cos (Arg p)) & x2 = |.p.| * (sin (Arg p)) holds
p = |[x1,x2]|
let p be Point of (TOP-REAL 2); ::_thesis: ( x1 = |.p.| * (cos (Arg p)) & x2 = |.p.| * (sin (Arg p)) implies p = |[x1,x2]| )
assume  ( x1 = |.p.| * (cos (Arg p)) & x2 = |.p.| * (sin (Arg p)) ) ; ::_thesis: p = |[x1,x2]|
then  ( x1 = |.(euc2cpx p).| * (cos (Arg (euc2cpx p))) & x2 = |.(euc2cpx p).| * (sin (Arg (euc2cpx p))) ) by Th25;
then  euc2cpx p = x1 + (x2 * <i>) by COMPLEX2:12;
then  p = cpx2euc (x1 + (x2 * <i>)) by Th2;
hence  p = |[x1,x2]| by Th5; ::_thesis: verum
end;

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 ) & ( Arg p >= PI implies Arg (- p) = (Arg p) - PI ) )
proof
let p be Point of (TOP-REAL 2); ::_thesis: ( p <> 0. (TOP-REAL 2) implies ( ( Arg p < PI implies Arg (- p) = (Arg p) + PI ) & ( Arg p >= PI implies Arg (- p) = (Arg p) - PI ) ) )
assume  p <> 0. (TOP-REAL 2) ; ::_thesis: ( ( Arg p < PI implies Arg (- p) = (Arg p) + PI ) & ( Arg p >= PI implies Arg (- p) = (Arg p) - PI ) )
then A1: euc2cpx p <> 0c by Th2, Th16;
 Arg (- p) = Arg (- (euc2cpx p)) by Th13;
hence  ( ( Arg p < PI implies Arg (- p) = (Arg p) + PI ) & ( Arg p >= PI implies Arg (- p) = (Arg p) - PI ) ) by A1, COMPLEX2:13; ::_thesis: verum
end;

theorem :: EUCLID_3:30
for p being Point of (TOP-REAL 2) st Arg p = 0 holds
( p = |[|.p.|,0]| & p `2 = 0 )
proof
let p be Point of (TOP-REAL 2); ::_thesis: ( Arg p = 0 implies ( p = |[|.p.|,0]| & p `2 = 0 ) )
assume  Arg p = 0 ; ::_thesis: ( p = |[|.p.|,0]| & p `2 = 0 )
then A1: ( euc2cpx p = |.(euc2cpx p).| + (0 * <i>) & Im (euc2cpx p) = 0 ) by COMPLEX2:15, COMPLEX2:21;
 ( cpx2euc (|.(euc2cpx p).| + (0 * <i>)) = |[|.(euc2cpx p).|,0]| & |.(euc2cpx p).| = |.p.| ) by Th5, Th25;
hence  ( p = |[|.p.|,0]| & p `2 = 0 ) by A1, Th2, COMPLEX1:12; ::_thesis: verum
end;

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 )
proof
let p be Point of (TOP-REAL 2); ::_thesis: ( p <> 0. (TOP-REAL 2) implies ( Arg p < PI iff Arg (- p) >= PI ) )
assume  p <> 0. (TOP-REAL 2) ; ::_thesis: ( Arg p < PI iff Arg (- p) >= PI )
then A1: euc2cpx p <> 0c by Th2, Th16;
 Arg (- p) = Arg (- (euc2cpx p)) by Th13;
hence  ( Arg p < PI iff Arg (- p) >= PI ) by A1, COMPLEX2:16; ::_thesis: verum
end;

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 )
proof
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( ( p1 <> p2 or p1 - p2 <> 0. (TOP-REAL 2) ) implies ( Arg (p1 - p2) < PI iff Arg (p2 - p1) >= PI ) )
assume  ( p1 <> p2 or p1 - p2 <> 0. (TOP-REAL 2) ) ; ::_thesis: ( Arg (p1 - p2) < PI iff Arg (p2 - p1) >= PI )
then A1: p1 - p2 <> 0. (TOP-REAL 2) by EUCLID:43;
 - (p1 - p2) = p2 - p1 by EUCLID:44;
hence  ( Arg (p1 - p2) < PI iff Arg (p2 - p1) >= PI ) by A1, Th31; ::_thesis: verum
end;

theorem :: EUCLID_3:33
for p being Point of (TOP-REAL 2) holds
( Arg p in ].0,PI.[ iff p `2 > 0 )
proof
let p be Point of (TOP-REAL 2); ::_thesis: ( Arg p in ].0,PI.[ iff p `2 > 0 )
 Im (euc2cpx p) = p `2 by COMPLEX1:12;
hence  ( Arg p in ].0,PI.[ iff p `2 > 0 ) by COMPLEX2:18; ::_thesis: verum
end;

theorem :: EUCLID_3:34
for p1, p2 being Point of (TOP-REAL 2) st Arg p1 < PI & Arg p2 < PI holds
Arg (p1 + p2) < PI
proof
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( Arg p1 < PI & Arg p2 < PI implies Arg (p1 + p2) < PI )
assume  ( Arg p1 < PI & Arg p2 < PI ) ; ::_thesis: Arg (p1 + p2) < PI
then  Arg ((euc2cpx p1) + (euc2cpx p2)) < PI by COMPLEX2:20;
hence  Arg (p1 + p2) < PI by Th9; ::_thesis: verum
end;

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))
proof
let p1, p2, p3 be Point of (TOP-REAL 2); ::_thesis: angle (p1,p2,p3) = angle ((p1 - p2),(0. (TOP-REAL 2)),(p3 - p2))
 ( (euc2cpx p1) - (euc2cpx p2) = euc2cpx (p1 - p2) & (euc2cpx p3) - (euc2cpx p2) = euc2cpx (p3 - p2) ) by Th15;
hence  angle (p1,p2,p3) = angle ((p1 - p2),(0. (TOP-REAL 2)),(p3 - p2)) by Th17, COMPLEX2:71; ::_thesis: verum
end;

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) & angle (p3,p2,p1) = 0 )
proof
let p1, p2, p3 be Point of (TOP-REAL 2); ::_thesis: ( angle (p1,p2,p3) = 0 implies ( Arg (p1 - p2) = Arg (p3 - p2) & angle (p3,p2,p1) = 0 ) )
assume A1: angle (p1,p2,p3) = 0 ; ::_thesis: ( Arg (p1 - p2) = Arg (p3 - p2) & angle (p3,p2,p1) = 0 )
 ( (euc2cpx p1) - (euc2cpx p2) = euc2cpx (p1 - p2) & (euc2cpx p3) - (euc2cpx p2) = euc2cpx (p3 - p2) ) by Th15;
hence  ( Arg (p1 - p2) = Arg (p3 - p2) & angle (p3,p2,p1) = 0 ) by A1, COMPLEX2:74; ::_thesis: verum
end;

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))
proof
let p1, p2, p3 be Point of (TOP-REAL 2); ::_thesis: ( angle (p1,p2,p3) <> 0 implies angle (p3,p2,p1) = (2 * PI) - (angle (p1,p2,p3)) )
assume  angle (p1,p2,p3) <> 0 ; ::_thesis: angle (p3,p2,p1) = (2 * PI) - (angle (p1,p2,p3))
then  (angle (p3,p2,p1)) + (angle (p1,p2,p3)) = 2 * PI by COMPLEX2:80;
hence  angle (p3,p2,p1) = (2 * PI) - (angle (p1,p2,p3)) ; ::_thesis: verum
end;

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))
proof
let p1, p2, p3 be Point of (TOP-REAL 2); ::_thesis: ( angle (p3,p2,p1) <> 0 implies angle (p3,p2,p1) = (2 * PI) - (angle (p1,p2,p3)) )
assume  angle (p3,p2,p1) <> 0 ; ::_thesis: angle (p3,p2,p1) = (2 * PI) - (angle (p1,p2,p3))
then  (angle (p3,p2,p1)) + (angle (p1,p2,p3)) = 2 * PI by COMPLEX2:80;
hence  angle (p3,p2,p1) = (2 * PI) - (angle (p1,p2,p3)) ; ::_thesis: verum
end;

theorem Th39: :: EUCLID_3:39
for x, y being Element of COMPLEX holds Re (x .|. y) = ((Re x) * (Re y)) + ((Im x) * (Im y))
proof
let x, y be Element of COMPLEX ; ::_thesis: Re (x .|. y) = ((Re x) * (Re y)) + ((Im x) * (Im y))
 x .|. y = (((Re x) * (Re y)) + ((Im x) * (Im y))) + (((- ((Re x) * (Im y))) + ((Im x) * (Re y))) * <i>) by COMPLEX2:29;
hence  Re (x .|. y) = ((Re x) * (Re y)) + ((Im x) * (Im y)) by COMPLEX1:12; ::_thesis: verum
end;

theorem Th40: :: EUCLID_3:40
for x, y being Element of COMPLEX holds Im (x .|. y) = (- ((Re x) * (Im y))) + ((Im x) * (Re y))
proof
let x, y be Element of COMPLEX ; ::_thesis: Im (x .|. y) = (- ((Re x) * (Im y))) + ((Im x) * (Re y))
 x .|. y = (((Re x) * (Re y)) + ((Im x) * (Im y))) + (((- ((Re x) * (Im y))) + ((Im x) * (Re y))) * <i>) by COMPLEX2:29;
hence  Im (x .|. y) = (- ((Re x) * (Im y))) + ((Im x) * (Re y)) by COMPLEX1:12; ::_thesis: verum
end;

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))
proof
let p, q be Point of (TOP-REAL 2); ::_thesis: |(p,q)| = ((p `1) * (q `1)) + ((p `2) * (q `2))
 (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  |(p,q)| = ((p `1) * (q `1)) + ((p `2) * (q `2)) by A1, A2, A4, A3; ::_thesis: verum
end;

theorem Th42: :: EUCLID_3:42
for p1, p2 being Point of (TOP-REAL 2) holds |(p1,p2)| = Re ((euc2cpx p1) .|. (euc2cpx p2))
proof
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: |(p1,p2)| = Re ((euc2cpx p1) .|. (euc2cpx 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 ; ::_thesis: verum
end;

theorem :: EUCLID_3:43
for p1, p2, p3 being Point of (TOP-REAL 2) 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 be Point of (TOP-REAL 2); ::_thesis: ( p1 <> 0. (TOP-REAL 2) & p2 <> 0. (TOP-REAL 2) implies ( |(p1,p2)| = 0 iff ( angle (p1,(0. (TOP-REAL 2)),p2) = PI / 2 or angle (p1,(0. (TOP-REAL 2)),p2) = (3 / 2) * PI ) ) )
assume  ( p1 <> 0. (TOP-REAL 2) & p2 <> 0. (TOP-REAL 2) ) ; ::_thesis: ( |(p1,p2)| = 0 iff ( angle (p1,(0. (TOP-REAL 2)),p2) = PI / 2 or angle (p1,(0. (TOP-REAL 2)),p2) = (3 / 2) * PI ) )
then A1: ( euc2cpx p1 <> 0c & euc2cpx p2 <> 0c ) by Th2, Th16;
 |(p1,p2)| = Re ((euc2cpx p1) .|. (euc2cpx p2)) by Th42;
hence  ( |(p1,p2)| = 0 iff ( angle (p1,(0. (TOP-REAL 2)),p2) = PI / 2 or angle (p1,(0. (TOP-REAL 2)),p2) = (3 / 2) * PI ) ) by A1, Th17, COMPLEX2:75; ::_thesis: verum
end;

theorem :: EUCLID_3:44
for p1, p2 being Point of (TOP-REAL 2) st p1 <> 0. (TOP-REAL 2) & p2 <> 0. (TOP-REAL 2) holds
( ( ( not (- ((p1 `1) * (p2 `2))) + ((p1 `2) * (p2 `1)) = |.p1.| * |.p2.| & 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 ) & ( ( not angle (p1,(0. (TOP-REAL 2)),p2) = PI / 2 & 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.|) ) )
proof
let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( p1 <> 0. (TOP-REAL 2) & p2 <> 0. (TOP-REAL 2) implies ( ( ( not (- ((p1 `1) * (p2 `2))) + ((p1 `2) * (p2 `1)) = |.p1.| * |.p2.| & 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 ) & ( ( not angle (p1,(0. (TOP-REAL 2)),p2) = PI / 2 & 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.|) ) ) )
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) ) ; ::_thesis: ( ( ( not (- ((p1 `1) * (p2 `2))) + ((p1 `2) * (p2 `1)) = |.p1.| * |.p2.| & 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 ) & ( ( not angle (p1,(0. (TOP-REAL 2)),p2) = PI / 2 & 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.|) ) )
then A3: ( euc2cpx p1 <> 0c & euc2cpx p2 <> 0c ) by Th2, Th16;
 ( |.(euc2cpx p1).| = |.p1.| & |.(euc2cpx p2).| = |.p2.| ) by Th25;
hence  ( ( ( not (- ((p1 `1) * (p2 `2))) + ((p1 `2) * (p2 `1)) = |.p1.| * |.p2.| & 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 ) & ( ( not angle (p1,(0. (TOP-REAL 2)),p2) = PI / 2 & 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.|) ) ) by A3, A2, Th17, COMPLEX2:76; ::_thesis: verum
end;

theorem :: EUCLID_3:45
for p1, p2, p3 being Point of (TOP-REAL 2) 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 be Point of (TOP-REAL 2); ::_thesis: ( p1 <> p2 & p3 <> p2 implies ( |((p1 - p2),(p3 - p2))| = 0 iff ( angle (p1,p2,p3) = PI / 2 or angle (p1,p2,p3) = (3 / 2) * PI ) ) )
assume that
A1: p1 <> p2 and
A2: p3 <> p2 ; ::_thesis: ( |((p1 - p2),(p3 - p2))| = 0 iff ( angle (p1,p2,p3) = PI / 2 or angle (p1,p2,p3) = (3 / 2) * PI ) )
 p1 - p2 <> 0. (TOP-REAL 2) by A1, EUCLID:43;
then A3: euc2cpx (p1 - p2) <> 0c by Th2, Th16;
 p3 - p2 <> 0. (TOP-REAL 2) by A2, EUCLID:43;
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  ::_thesis: ( ( angle (p1,p2,p3) = PI / 2 or angle (p1,p2,p3) = (3 / 2) * PI ) implies |((p1 - p2),(p3 - p2))| = 0 )
assume  |((p1 - p2),(p3 - p2))| = 0 ; ::_thesis: ( angle (p1,p2,p3) = PI / 2 or angle (p1,p2,p3) = (3 / 2) * PI )
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; ::_thesis: verum
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 ) ; ::_thesis: |((p1 - p2),(p3 - p2))| = 0
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  |((p1 - p2),(p3 - p2))| = 0 by A6, A3, A4, COMPLEX2:75; ::_thesis: verum
end;

theorem :: EUCLID_3:46
for p1, p2, p3 being Point of (TOP-REAL 2) 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 be Point of (TOP-REAL 2); ::_thesis: ( p1 <> p2 & p3 <> p2 & ( angle (p1,p2,p3) = PI / 2 or angle (p1,p2,p3) = (3 / 2) * PI ) implies (|.(p1 - p2).| ^2) + (|.(p3 - p2).| ^2) = |.(p1 - p3).| ^2 )
assume that
A1: ( p1 <> p2 & p3 <> p2 ) and
A2: ( angle (p1,p2,p3) = PI / 2 or angle (p1,p2,p3) = (3 / 2) * PI ) ; ::_thesis: (|.(p1 - p2).| ^2) + (|.(p3 - p2).| ^2) = |.(p1 - p3).| ^2
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  (|.(p1 - p2).| ^2) + (|.(p3 - p2).| ^2) = |.(p1 - p3).| ^2 by A2, A3, A4, A5, COMPLEX2:77; ::_thesis: verum
end;

theorem :: EUCLID_3:47
for p1, p2, p3 being Point of (TOP-REAL 2) 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 be Point of (TOP-REAL 2); ::_thesis: ( p2 <> p1 & p1 <> p3 & p3 <> p2 & angle (p2,p1,p3) < PI implies ((angle (p2,p1,p3)) + (angle (p1,p3,p2))) + (angle (p3,p2,p1)) = PI )
assume that
A1: ( p2 <> p1 & p1 <> p3 ) and
A2: p3 <> p2 and
A3: angle (p2,p1,p3) < PI ; ::_thesis: ((angle (p2,p1,p3)) + (angle (p1,p3,p2))) + (angle (p3,p2,p1)) = PI
A4: ( euc2cpx p1 <> euc2cpx p2 & euc2cpx p1 <> euc2cpx p3 ) by A1, Th4;
A5: euc2cpx p3 <> euc2cpx p2 by A2, Th4;
percases ( 0 = angle ((euc2cpx p2),(euc2cpx p1),(euc2cpx p3)) or 0 < angle ((euc2cpx p2),(euc2cpx p1),(euc2cpx p3)) ) by COMPLEX2:70;
supposeA6: 0 = angle ((euc2cpx p2),(euc2cpx p1),(euc2cpx p3)) ; ::_thesis: ((angle (p2,p1,p3)) + (angle (p1,p3,p2))) + (angle (p3,p2,p1)) = PI
now__::_thesis:_((angle_(p2,p1,p3))_+_(angle_(p1,p3,p2)))_+_(angle_(p3,p2,p1))_=_PI
percases ( ( angle ((euc2cpx p1),(euc2cpx p3),(euc2cpx p2)) = 0 & angle ((euc2cpx p3),(euc2cpx p2),(euc2cpx p1)) = PI ) or ( angle ((euc2cpx p1),(euc2cpx p3),(euc2cpx p2)) = PI & angle ((euc2cpx p3),(euc2cpx p2),(euc2cpx p1)) = 0 ) ) by A4, A5, A6, COMPLEX2:87;
suppose ( angle ((euc2cpx p1),(euc2cpx p3),(euc2cpx p2)) = 0 & angle ((euc2cpx p3),(euc2cpx p2),(euc2cpx p1)) = PI ) ; ::_thesis: ((angle (p2,p1,p3)) + (angle (p1,p3,p2))) + (angle (p3,p2,p1)) = PI
hence  ((angle (p2,p1,p3)) + (angle (p1,p3,p2))) + (angle (p3,p2,p1)) = PI by A6; ::_thesis: verum
end;
suppose ( angle ((euc2cpx p1),(euc2cpx p3),(euc2cpx p2)) = PI & angle ((euc2cpx p3),(euc2cpx p2),(euc2cpx p1)) = 0 ) ; ::_thesis: ((angle (p2,p1,p3)) + (angle (p1,p3,p2))) + (angle (p3,p2,p1)) = PI
hence  ((angle (p2,p1,p3)) + (angle (p1,p3,p2))) + (angle (p3,p2,p1)) = PI by A6; ::_thesis: verum
end;
end;
end;
hence  ((angle (p2,p1,p3)) + (angle (p1,p3,p2))) + (angle (p3,p2,p1)) = PI ; ::_thesis: verum
end;
suppose 0 < angle ((euc2cpx p2),(euc2cpx p1),(euc2cpx p3)) ; ::_thesis: ((angle (p2,p1,p3)) + (angle (p1,p3,p2))) + (angle (p3,p2,p1)) = PI
hence  ((angle (p2,p1,p3)) + (angle (p1,p3,p2))) + (angle (p3,p2,p1)) = PI by A3, A4, COMPLEX2:84; ::_thesis: verum
end;
end;
end;

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 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & 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 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )  }  is Subset of (TOP-REAL n);
proof
defpred S1[ set ] means  ex a1, a2, a3 being Real st
( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & $1 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) );
  {  p where p is Element of (TOP-REAL n) : S1[p]  }  is Subset of (TOP-REAL n) from DOMAIN_1:sch_7();
hence   {  p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st
( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )  }  is Subset of (TOP-REAL n) ; ::_thesis: verum
end;
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 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & 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 ) & (a1 + a2) + a3 = 1 & 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 ) & (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )  }  is Subset of (TOP-REAL n);
proof
defpred S1[ set ] means  ex a1, a2, a3 being Real st
( ( 0 > a1 or 0 > a2 or 0 > a3 ) & (a1 + a2) + a3 = 1 & $1 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) );
  {  p where p is Point of (TOP-REAL n) : S1[p]  }  is Subset of (TOP-REAL n) from DOMAIN_1:sch_7();
hence   {  p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st
( ( 0 > a1 or 0 > a2 or 0 > a3 ) & (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )  }  is Subset of (TOP-REAL n) ; ::_thesis: verum
end;
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 ) & (a1 + a2) + a3 = 1 & 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 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )
proof
let n be Element of NAT ; ::_thesis: 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 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )
let p1, p2, p3, p be Point of (TOP-REAL n); ::_thesis: ( p in plane (p1,p2,p3) implies ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) )
assume A1: p in plane (p1,p2,p3) ; ::_thesis: ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )
now__::_thesis:_(_(_p_in_outside_of_triangle_(p1,p2,p3)_&_ex_a1,_a2,_a3_being_Real_st_
(_(a1_+_a2)_+_a3_=_1_&_p_=_((a1_*_p1)_+_(a2_*_p2))_+_(a3_*_p3)_)_)_or_(_p_in_closed_inside_of_triangle_(p1,p2,p3)_&_ex_a1,_a2,_a3_being_Real_st_
(_(a1_+_a2)_+_a3_=_1_&_p_=_((a1_*_p1)_+_(a2_*_p2))_+_(a3_*_p3)_)_)_)
percases ( p in outside_of_triangle (p1,p2,p3) or p in closed_inside_of_triangle (p1,p2,p3) ) by A1, XBOOLE_0:def_3;
case p in outside_of_triangle (p1,p2,p3) ; ::_thesis: ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )
then  ex p4 being Point of (TOP-REAL n) st
( p4 = p & ex a1, a2, a3 being Real st
( ( 0 > a1 or 0 > a2 or 0 > a3 ) & (a1 + a2) + a3 = 1 & p4 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) ) ;
hence  ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) ; ::_thesis: verum
end;
case p in closed_inside_of_triangle (p1,p2,p3) ; ::_thesis: ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )
then  ex p4 being Point of (TOP-REAL n) st
( p4 = p & ex a1, a2, a3 being Real st
( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & p4 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) ) ;
hence  ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) ; ::_thesis: verum
end;
end;
end;
hence  ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) ; ::_thesis: verum
end;

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)
proof
let n be Element of NAT ; ::_thesis: for p1, p2, p3 being Point of (TOP-REAL n) holds Triangle (p1,p2,p3) c= closed_inside_of_triangle (p1,p2,p3)
let p1, p2, p3 be Point of (TOP-REAL n); ::_thesis: Triangle (p1,p2,p3) c= closed_inside_of_triangle (p1,p2,p3)
 ((LSeg (p1,p2)) \/ (LSeg (p2,p3))) \/ (LSeg (p3,p1)) c= closed_inside_of_triangle (p1,p2,p3)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((LSeg (p1,p2)) \/ (LSeg (p2,p3))) \/ (LSeg (p3,p1)) or x in closed_inside_of_triangle (p1,p2,p3) )
assume A1: x in ((LSeg (p1,p2)) \/ (LSeg (p2,p3))) \/ (LSeg (p3,p1)) ; ::_thesis: x in closed_inside_of_triangle (p1,p2,p3)
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__::_thesis:_(_(_x_in_LSeg_(p1,p2)_&_ex_a1,_a2,_a3_being_Real_st_
(_0_<=_a1_&_0_<=_a2_&_0_<=_a3_&_(a1_+_a2)_+_a3_=_1_&_p0_=_((a1_*_p1)_+_(a2_*_p2))_+_(a3_*_p3)_)_)_or_(_x_in_LSeg_(p2,p3)_&_ex_a1,_a2,_a3_being_Real_st_
(_0_<=_a1_&_0_<=_a2_&_0_<=_a3_&_(a1_+_a2)_+_a3_=_1_&_p0_=_((a1_*_p1)_+_(a2_*_p2))_+_(a3_*_p3)_)_)_or_(_x_in_LSeg_(p3,p1)_&_ex_a1,_a2,_a3_being_Real_st_
(_0_<=_a1_&_0_<=_a2_&_0_<=_a3_&_(a1_+_a2)_+_a3_=_1_&_p0_=_((a1_*_p1)_+_(a2_*_p2))_+_(a3_*_p3)_)_)_)
percases ( x in LSeg (p1,p2) or x in LSeg (p2,p3) or x in LSeg (p3,p1) ) by A2, XBOOLE_0:def_3;
case x in LSeg (p1,p2) ; ::_thesis: ex a1, a2, a3 being Real st
( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )
then consider lambda being 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, EUCLID:27
.= (((1 - lambda) * p1) + (lambda * p2)) + (0 * p3) by EUCLID:29 ;
A7: ((1 - lambda) + lambda) + 0 = 1 ;
 1 - lambda >= 0 by A5, XREAL_1:48;
hence  ex a1, a2, a3 being Real st
( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) by A4, A7, A6; ::_thesis: verum
end;
case x in LSeg (p2,p3) ; ::_thesis: ex a1, a2, a3 being Real st
( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )
then consider lambda being 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, EUCLID:27
.= ((0 * p1) + ((1 - lambda) * p2)) + (lambda * p3) by EUCLID:29 ;
A12: (0 + (1 - lambda)) + lambda = 1 ;
 1 - lambda >= 0 by A10, XREAL_1:48;
hence  ex a1, a2, a3 being Real st
( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) by A9, A12, A11; ::_thesis: verum
end;
case x in LSeg (p3,p1) ; ::_thesis: ex a1, a2, a3 being Real st
( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )
then consider lambda being 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, EUCLID:27
.= ((lambda * p1) + (0 * p2)) + ((1 - lambda) * p3) by EUCLID:29 ;
A17: (lambda + 0) + (1 - lambda) = 1 ;
 1 - lambda >= 0 by A15, XREAL_1:48;
hence  ex a1, a2, a3 being Real st
( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) by A14, A17, A16; ::_thesis: verum
end;
end;
end;
hence  x in closed_inside_of_triangle (p1,p2,p3) ; ::_thesis: verum
end;
hence  Triangle (p1,p2,p3) c= closed_inside_of_triangle (p1,p2,p3) ; ::_thesis: verum
end;

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 & 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 & 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 & q1 <> 0. (TOP-REAL n) & q2 <> 0. (TOP-REAL n) )
proof
let n be Element of NAT ; ::_thesis: for q1, q2 being Point of (TOP-REAL n) st q1,q2 are_lindependent2 holds
( q1 <> q2 & q1 <> 0. (TOP-REAL n) & q2 <> 0. (TOP-REAL n) )
let q1, q2 be Point of (TOP-REAL n); ::_thesis: ( q1,q2 are_lindependent2 implies ( q1 <> q2 & q1 <> 0. (TOP-REAL n) & q2 <> 0. (TOP-REAL n) ) )
assume A1: q1,q2 are_lindependent2 ; ::_thesis: ( q1 <> q2 & q1 <> 0. (TOP-REAL n) & q2 <> 0. (TOP-REAL n) )
assume A2: ( q1 = q2 or q1 = 0. (TOP-REAL n) or q2 = 0. (TOP-REAL n) ) ; ::_thesis: contradiction
now__::_thesis:_(_(_q1_=_q2_&_contradiction_)_or_(_q1_=_0._(TOP-REAL_n)_&_contradiction_)_or_(_q2_=_0._(TOP-REAL_n)_&_contradiction_)_)
percases ( q1 = q2 or q1 = 0. (TOP-REAL n) or q2 = 0. (TOP-REAL n) ) by A2;
caseA3: q1 = q2 ; ::_thesis: contradiction
(1 * q1) + ((- 1) * q2) = (1 * q1) + (- q2) by EUCLID:39
.= q1 + (- q2) by EUCLID:29
.= 0. (TOP-REAL n) by A3, EUCLID:36 ;
hence  contradiction by A1, Def10; ::_thesis: verum
end;
case q1 = 0. (TOP-REAL n) ; ::_thesis: contradiction
then (1 * q1) + (0 * q2) = (0. (TOP-REAL n)) + (0 * q2) by EUCLID:28
.= (0. (TOP-REAL n)) + (0. (TOP-REAL n)) by EUCLID:29
.= 0. (TOP-REAL n) by EUCLID:27 ;
hence  contradiction by A1, Def10; ::_thesis: verum
end;
case q2 = 0. (TOP-REAL n) ; ::_thesis: contradiction
then (0 * q1) + (1 * q2) = (0 * q1) + (0. (TOP-REAL n)) by EUCLID:28
.= (0. (TOP-REAL n)) + (0. (TOP-REAL n)) by EUCLID:29
.= 0. (TOP-REAL n) by EUCLID:27 ;
hence  contradiction by A1, Def10; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;

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 & p0 in plane (p1,p2,p3) holds
ex a1, a2, a3 being Real st
( p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) & (a1 + a2) + a3 = 1 & ( for b1, b2, b3 being 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 ; ::_thesis: for p1, p2, p3, p0 being Point of (TOP-REAL n) st p2 - p1,p3 - p1 are_lindependent2 & p0 in plane (p1,p2,p3) holds
ex a1, a2, a3 being Real st
( p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) & (a1 + a2) + a3 = 1 & ( for b1, b2, b3 being Real st p0 = ((b1 * p1) + (b2 * p2)) + (b3 * p3) & (b1 + b2) + b3 = 1 holds
( b1 = a1 & b2 = a2 & b3 = a3 ) ) )
let p1, p2, p3, p0 be Point of (TOP-REAL n); ::_thesis: ( p2 - p1,p3 - p1 are_lindependent2 & p0 in plane (p1,p2,p3) implies ex a1, a2, a3 being Real st
( p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) & (a1 + a2) + a3 = 1 & ( for b1, b2, b3 being Real st p0 = ((b1 * p1) + (b2 * p2)) + (b3 * p3) & (b1 + b2) + b3 = 1 holds
( b1 = a1 & b2 = a2 & b3 = a3 ) ) ) )
assume that
A1: p2 - p1,p3 - p1 are_lindependent2 and
A2: p0 in plane (p1,p2,p3) ; ::_thesis: ex a1, a2, a3 being Real st
( p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) & (a1 + a2) + a3 = 1 & ( for b1, b2, b3 being Real st p0 = ((b1 * p1) + (b2 * p2)) + (b3 * p3) & (b1 + b2) + b3 = 1 holds
( b1 = a1 & b2 = a2 & b3 = a3 ) ) )
set q2 = p2 - p1;
set q3 = p3 - p1;
consider a01, a02, a03 being Real such that
A3: (a01 + a02) + a03 = 1 and
A4: p0 = ((a01 * p1) + (a02 * p2)) + (a03 * p3) by A2, Th48;
 for b1, b2, b3 being 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, EUCLID:29
.= (((a01 * p1) + (a02 * p2)) + (a03 * p3)) + (- (((a01 + a02) * p1) + (a03 * p1))) by EUCLID:33
.= (((a01 * p1) + (a02 * p2)) + (a03 * p3)) + (- (((a01 * p1) + (a02 * p1)) + (a03 * p1))) by EUCLID:33
.= (((a01 * p1) + (a02 * p2)) + (a03 * p3)) + ((- ((a01 * p1) + (a02 * p1))) - (a03 * p1)) by EUCLID:38
.= (((a01 * p1) + (a02 * p2)) + (a03 * p3)) + (((- (a01 * p1)) - (a02 * p1)) - (a03 * p1)) by EUCLID:38
.= ((a01 * p1) + ((a02 * p2) + (a03 * p3))) + (((- (a01 * p1)) + (- (a02 * p1))) + (- (a03 * p1))) by EUCLID:26
.= ((a01 * p1) + ((a02 * p2) + (a03 * p3))) + ((- (a01 * p1)) + ((- (a02 * p1)) + (- (a03 * p1)))) by EUCLID:26
.= ((((a02 * p2) + (a03 * p3)) + (a01 * p1)) - (a01 * p1)) + ((- (a02 * p1)) + (- (a03 * p1))) by EUCLID:26
.= ((a02 * p2) + (a03 * p3)) + ((- (a02 * p1)) + (- (a03 * p1))) by EUCLID:48
.= (((a02 * p2) + (a03 * p3)) + (- (a02 * p1))) + (- (a03 * p1)) by EUCLID:26
.= (((a02 * p2) + (- (a02 * p1))) + (a03 * p3)) + (- (a03 * p1)) by EUCLID:26
.= (((a02 * p2) + (a02 * (- p1))) + (a03 * p3)) + (- (a03 * p1)) by EUCLID:40
.= ((a02 * (p2 + (- p1))) + (a03 * p3)) + (- (a03 * p1)) by EUCLID:32
.= (a02 * (p2 + (- p1))) + ((a03 * p3) + (- (a03 * p1))) by EUCLID:26
.= (a02 * (p2 + (- p1))) + ((a03 * p3) + (a03 * (- p1))) by EUCLID:40
.= (a02 * (p2 - p1)) + (a03 * (p3 - p1)) by EUCLID:32 ;
let b1, b2, b3 be Real; ::_thesis: ( p0 = ((b1 * p1) + (b2 * p2)) + (b3 * p3) & (b1 + b2) + b3 = 1 implies ( b1 = a01 & b2 = a02 & b3 = a03 ) )
assume that
A6: p0 = ((b1 * p1) + (b2 * p2)) + (b3 * p3) and
A7: (b1 + b2) + b3 = 1 ; ::_thesis: ( b1 = a01 & b2 = a02 & b3 = a03 )
p0 + (- p1) = (((b1 * p1) + (b2 * p2)) + (b3 * p3)) + (- (((b1 + b2) + b3) * p1)) by A6, A7, EUCLID:29
.= (((b1 * p1) + (b2 * p2)) + (b3 * p3)) + (- (((b1 + b2) * p1) + (b3 * p1))) by EUCLID:33
.= (((b1 * p1) + (b2 * p2)) + (b3 * p3)) + (- (((b1 * p1) + (b2 * p1)) + (b3 * p1))) by EUCLID:33
.= (((b1 * p1) + (b2 * p2)) + (b3 * p3)) + ((- ((b1 * p1) + (b2 * p1))) - (b3 * p1)) by EUCLID:38
.= (((b1 * p1) + (b2 * p2)) + (b3 * p3)) + (((- (b1 * p1)) - (b2 * p1)) - (b3 * p1)) by EUCLID:38
.= ((b1 * p1) + ((b2 * p2) + (b3 * p3))) + (((- (b1 * p1)) + (- (b2 * p1))) + (- (b3 * p1))) by EUCLID:26
.= ((b1 * p1) + ((b2 * p2) + (b3 * p3))) + ((- (b1 * p1)) + ((- (b2 * p1)) + (- (b3 * p1)))) by EUCLID:26
.= ((((b2 * p2) + (b3 * p3)) + (b1 * p1)) - (b1 * p1)) + ((- (b2 * p1)) + (- (b3 * p1))) by EUCLID:26
.= ((b2 * p2) + (b3 * p3)) + ((- (b2 * p1)) + (- (b3 * p1))) by EUCLID:48
.= (((b2 * p2) + (b3 * p3)) + (- (b2 * p1))) + (- (b3 * p1)) by EUCLID:26
.= (((b2 * p2) + (- (b2 * p1))) + (b3 * p3)) + (- (b3 * p1)) by EUCLID:26
.= (((b2 * p2) + (b2 * (- p1))) + (b3 * p3)) + (- (b3 * p1)) by EUCLID:40
.= ((b2 * (p2 + (- p1))) + (b3 * p3)) + (- (b3 * p1)) by EUCLID:32
.= (b2 * (p2 + (- p1))) + ((b3 * p3) + (- (b3 * p1))) by EUCLID:26
.= (b2 * (p2 + (- p1))) + ((b3 * p3) + (b3 * (- p1))) by EUCLID:40
.= (b2 * (p2 - p1)) + (b3 * (p3 - p1)) by EUCLID:32 ;
then  ((b2 * (p2 - p1)) + (b3 * (p3 - p1))) + (- ((a02 * (p2 - p1)) + (a03 * (p3 - p1)))) = 0. (TOP-REAL n) by A5, EUCLID:36;
then  ((b2 * (p2 - p1)) + (b3 * (p3 - p1))) + ((- (a02 * (p2 - p1))) - (a03 * (p3 - p1))) = 0. (TOP-REAL n) by EUCLID:38;
then  (((b2 * (p2 - p1)) + (b3 * (p3 - p1))) + (- (a02 * (p2 - p1)))) + (- (a03 * (p3 - p1))) = 0. (TOP-REAL n) by EUCLID:26;
then  (((b2 * (p2 - p1)) + (- (a02 * (p2 - p1)))) + (b3 * (p3 - p1))) + (- (a03 * (p3 - p1))) = 0. (TOP-REAL n) by EUCLID:26;
then  (((b2 * (p2 - p1)) + ((- a02) * (p2 - p1))) + (b3 * (p3 - p1))) + (- (a03 * (p3 - p1))) = 0. (TOP-REAL n) by EUCLID:40;
then  (((b2 + (- a02)) * (p2 - p1)) + (b3 * (p3 - p1))) + (- (a03 * (p3 - p1))) = 0. (TOP-REAL n) by EUCLID:33;
then  ((b2 + (- a02)) * (p2 - p1)) + ((b3 * (p3 - p1)) + (- (a03 * (p3 - p1)))) = 0. (TOP-REAL n) by EUCLID:26;
then  ((b2 + (- a02)) * (p2 - p1)) + ((b3 * (p3 - p1)) + ((- a03) * (p3 - p1))) = 0. (TOP-REAL n) by EUCLID:40;
then  ((b2 + (- a02)) * (p2 - p1)) + ((b3 + (- a03)) * (p3 - p1)) = 0. (TOP-REAL n) by EUCLID:33;
then  ( (b2 - a02) + a02 = 0 + a02 & b3 + (- a03) = 0 ) by A1, Def10;
hence  ( b1 = a01 & b2 = a02 & b3 = a03 ) by A3, A7; ::_thesis: verum
end;
hence  ex a1, a2, a3 being Real st
( p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) & (a1 + a2) + a3 = 1 & ( for b1, b2, b3 being Real st p0 = ((b1 * p1) + (b2 * p2)) + (b3 * p3) & (b1 + b2) + b3 = 1 holds
( b1 = a1 & b2 = a2 & b3 = a3 ) ) ) by A3, A4; ::_thesis: verum
end;

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) & (a1 + a2) + a3 = 1 ) holds
p0 in plane (p1,p2,p3)
proof
let n be Element of NAT ; ::_thesis: 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) & (a1 + a2) + a3 = 1 ) holds
p0 in plane (p1,p2,p3)
let p1, p2, p3, p0 be Point of (TOP-REAL n); ::_thesis: ( ex a1, a2, a3 being Real st
( p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) & (a1 + a2) + a3 = 1 ) implies p0 in plane (p1,p2,p3) )
given a1, a2, a3 being Real such that A1: ( p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) & (a1 + a2) + a3 = 1 ) ; ::_thesis: p0 in plane (p1,p2,p3)
now__::_thesis:_(_(_(_0_>_a1_or_0_>_a2_or_0_>_a3_)_&_p0_in_plane_(p1,p2,p3)_)_or_(_0_<=_a1_&_0_<=_a2_&_0_<=_a3_&_p0_in_plane_(p1,p2,p3)_)_)
percases ( 0 > a1 or 0 > a2 or 0 > a3 or ( 0 <= a1 & 0 <= a2 & 0 <= a3 ) ) ;
case ( 0 > a1 or 0 > a2 or 0 > a3 ) ; ::_thesis: p0 in plane (p1,p2,p3)
then  p0 in outside_of_triangle (p1,p2,p3) by A1;
hence  p0 in plane (p1,p2,p3) by XBOOLE_0:def_3; ::_thesis: verum
end;
case ( 0 <= a1 & 0 <= a2 & 0 <= a3 ) ; ::_thesis: p0 in plane (p1,p2,p3)
then  p0 in closed_inside_of_triangle (p1,p2,p3) by A1;
hence  p0 in plane (p1,p2,p3) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
hence  p0 in plane (p1,p2,p3) ; ::_thesis: verum
end;

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 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )  }
proof
let n be Element of NAT ; ::_thesis: 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 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )  }
let p1, p2, p3 be Point of (TOP-REAL n); ::_thesis: plane (p1,p2,p3) =  {  p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )  }
thus  plane (p1,p2,p3) c=  {  p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )  }  c= plane (p1,p2,p3)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in plane (p1,p2,p3) or x in  {  p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )  }  )
assume A1: x in plane (p1,p2,p3) ; ::_thesis: x in  {  p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )  }
then reconsider p0 = x as Point of (TOP-REAL n) ;
 ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) by A1, Th48;
hence  x in  {  p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )  }  ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )  }  or x in plane (p1,p2,p3) )
assume  x in  {  p where p is Point of (TOP-REAL n) : ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )  }  ; ::_thesis: x in plane (p1,p2,p3)
then  ex p being Point of (TOP-REAL n) st
( p = x & ex a1, a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) ) ;
hence  x in plane (p1,p2,p3) by Th52; ::_thesis: verum
end;

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
proof
let p1, p2, p3 be Point of (TOP-REAL 2); ::_thesis: ( p2 - p1,p3 - p1 are_lindependent2 implies plane (p1,p2,p3) = REAL 2 )
assume A1: p2 - p1,p3 - p1 are_lindependent2 ; ::_thesis: plane (p1,p2,p3) = REAL 2
 the carrier of (TOP-REAL 2) = REAL 2 by EUCLID:22;
hence  plane (p1,p2,p3) c= REAL 2 ; :: according to XBOOLE_0:def_10 ::_thesis: REAL 2 c= plane (p1,p2,p3)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in REAL 2 or x in plane (p1,p2,p3) )
assume  x in REAL 2 ; ::_thesis: x in plane (p1,p2,p3)
then reconsider p0 = x as Point of (TOP-REAL 2) by EUCLID:22;
set q2 = p2 - p1;
set q3 = p3 - p1;
set p = p0 - p1;
A2: p3 - p1 <> 0. (TOP-REAL 2) by A1, Th50;
now__::_thesis:_(_(_(p3_-_p1)_`1_<>_0_&_x_in_plane_(p1,p2,p3)_)_or_(_(p3_-_p1)_`2_<>_0_&_x_in_plane_(p1,p2,p3)_)_)
percases ( (p3 - p1) `1 <> 0 or (p3 - p1) `2 <> 0 ) by A2, EUCLID:53, EUCLID:54;
caseA3: (p3 - p1) `1 <> 0 ; ::_thesis: x in plane (p1,p2,p3)
A4: now__::_thesis:_not_(((p2_-_p1)_`2)_*_((p3_-_p1)_`1))_-_(((p2_-_p1)_`1)_*_((p3_-_p1)_`2))_=_0
assume  (((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)) = 0 ; ::_thesis: contradiction
then  (p2 - p1) `2 = (((p2 - p1) `1) * ((p3 - p1) `2)) / ((p3 - p1) `1) by A3, XCMPLX_1:89;
then p2 - p1 = |[((p2 - p1) `1),((((p2 - p1) `1) * ((p3 - p1) `2)) / ((p3 - p1) `1))]| by EUCLID:53
.= |[(((p2 - p1) `1) * 1),((((p2 - p1) `1) * ((p3 - p1) `2)) * (((p3 - p1) `1) "))]| by XCMPLX_0:def_9
.= |[(((p2 - p1) `1) * 1),(((p2 - p1) `1) * (((p3 - p1) `2) * (((p3 - p1) `1) ")))]|
.= ((p2 - p1) `1) * |[1,(((p3 - p1) `2) * (((p3 - p1) `1) "))]| by EUCLID:58
.= ((p2 - p1) `1) * |[((((p3 - p1) `1) ") * ((p3 - p1) `1)),((((p3 - p1) `1) ") * ((p3 - p1) `2))]| by A3, XCMPLX_0:def_7
.= ((p2 - p1) `1) * ((((p3 - p1) `1) ") * |[((p3 - p1) `1),((p3 - p1) `2)]|) by EUCLID:58
.= ((p2 - p1) `1) * ((((p3 - p1) `1) ") * (p3 - p1)) by EUCLID:53
.= (((p2 - p1) `1) * (((p3 - p1) `1) ")) * (p3 - p1) by EUCLID:30 ;
then  (p2 - p1) + (- ((((p2 - p1) `1) * (((p3 - p1) `1) ")) * (p3 - p1))) = 0. (TOP-REAL 2) by EUCLID:36;
then  (1 * (p2 - p1)) + (- ((((p2 - p1) `1) * (((p3 - p1) `1) ")) * (p3 - p1))) = 0. (TOP-REAL 2) by EUCLID:29;
then  (1 * (p2 - p1)) + ((- (((p2 - p1) `1) * (((p3 - p1) `1) "))) * (p3 - p1)) = 0. (TOP-REAL 2) by EUCLID:40;
hence  contradiction by A1, Def10; ::_thesis: verum
end;
set a = ((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)));
set b = (((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1);
A5: ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1)) + (((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1)) * ((p3 - p1) `1)) = ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1)) + (((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) by A3, XCMPLX_1:87
.= (p0 - p1) `1 ;
A6: ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `2)) + (((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1)) * ((p3 - p1) `2)) = ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `2)) + (((((p0 - p1) `1) / ((p3 - p1) `1)) - (((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1)) / ((p3 - p1) `1))) * ((p3 - p1) `2)) by XCMPLX_1:120
.= (((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `2)) - ((((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1)) / ((p3 - p1) `1)) * ((p3 - p1) `2))) + ((((p0 - p1) `1) / ((p3 - p1) `1)) * ((p3 - p1) `2))
.= (((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `2)) - ((((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1)) * (((p3 - p1) `1) ")) * ((p3 - p1) `2))) + ((((p0 - p1) `1) / ((p3 - p1) `1)) * ((p3 - p1) `2)) by XCMPLX_0:def_9
.= ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * (((p2 - p1) `2) - ((((p2 - p1) `1) * (((p3 - p1) `1) ")) * ((p3 - p1) `2)))) + ((((p0 - p1) `1) / ((p3 - p1) `1)) * ((p3 - p1) `2))
.= ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * (((p2 - p1) `2) - ((((p2 - p1) `1) / ((p3 - p1) `1)) * ((p3 - p1) `2)))) + ((((p0 - p1) `1) / ((p3 - p1) `1)) * ((p3 - p1) `2)) by XCMPLX_0:def_9
.= ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * (((((p2 - p1) `2) / ((p3 - p1) `1)) * ((p3 - p1) `1)) - ((((p2 - p1) `1) / ((p3 - p1) `1)) * ((p3 - p1) `2)))) + ((((p0 - p1) `1) / ((p3 - p1) `1)) * ((p3 - p1) `2)) by A3, XCMPLX_1:87
.= ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * (((((p3 - p1) `1) / ((p3 - p1) `1)) * ((p2 - p1) `2)) - ((((p2 - p1) `1) / ((p3 - p1) `1)) * ((p3 - p1) `2)))) + ((((p0 - p1) `1) / ((p3 - p1) `1)) * ((p3 - p1) `2)) by XCMPLX_1:75
.= ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * (((((p3 - p1) `1) * (((p3 - p1) `1) ")) * ((p2 - p1) `2)) - ((((p2 - p1) `1) / ((p3 - p1) `1)) * ((p3 - p1) `2)))) + ((((p0 - p1) `1) / ((p3 - p1) `1)) * ((p3 - p1) `2)) by XCMPLX_0:def_9
.= ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((((p2 - p1) `2) * (((p3 - p1) `1) * (((p3 - p1) `1) "))) - (((((p3 - p1) `1) ") * ((p2 - p1) `1)) * ((p3 - p1) `2)))) + ((((p0 - p1) `1) / ((p3 - p1) `1)) * ((p3 - p1) `2)) by XCMPLX_0:def_9
.= (((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * (((p3 - p1) `1) ")) + ((((p0 - p1) `1) / ((p3 - p1) `1)) * ((p3 - p1) `2))
.= (((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) * (((p3 - p1) `1) ")) + ((((p0 - p1) `1) / ((p3 - p1) `1)) * ((p3 - p1) `2)) by A4, XCMPLX_1:87
.= (((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) * (((p3 - p1) `1) ")) + (((((p3 - p1) `1) ") * ((p0 - p1) `1)) * ((p3 - p1) `2)) by XCMPLX_0:def_9
.= (((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) + (((p3 - p1) `2) * ((p0 - p1) `1))) * (((p3 - p1) `1) ")
.= (((p0 - p1) `2) * ((p3 - p1) `1)) / ((p3 - p1) `1) by XCMPLX_0:def_9
.= (p0 - p1) `2 by A3, XCMPLX_1:89 ;
A7: ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * (p2 - p1)) + (((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1)) * (p3 - p1)) = (((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * p2) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * p1)) + (((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1)) * (p3 - p1)) by EUCLID:49
.= (((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * p2) + (- ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * p1))) + ((((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1)) * p3) - (((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1)) * p1)) by EUCLID:49
.= (((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * p2) + (- ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * p1))) + ((((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1)) * p3) + ((- ((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1))) * p1)) by EUCLID:40
.= (((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * p2) + ((- (((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2))))) * p1)) + (((- ((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1))) * p1) + (((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1)) * p3)) by EUCLID:40
.= ((((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * p2) + ((- (((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2))))) * p1)) + ((- ((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1))) * p1)) + (((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1)) * p3) by EUCLID:26
.= (((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * p2) + (((- (((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2))))) * p1) + ((- ((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1))) * p1))) + (((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1)) * p3) by EUCLID:26
.= ((((- (((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2))))) + (- ((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1)))) * p1) + ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * p2)) + (((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1)) * p3) by EUCLID:33 ;
((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * (p2 - p1)) + (((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1)) * (p3 - p1)) = ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * |[((p2 - p1) `1),((p2 - p1) `2)]|) + (((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1)) * (p3 - p1)) by EUCLID:53
.= ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * |[((p2 - p1) `1),((p2 - p1) `2)]|) + (((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1)) * |[((p3 - p1) `1),((p3 - p1) `2)]|) by EUCLID:53
.= |[((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1)),((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `2))]| + (((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1)) * |[((p3 - p1) `1),((p3 - p1) `2)]|) by EUCLID:58
.= |[((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1)),((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `2))]| + |[(((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1)) * ((p3 - p1) `1)),(((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1)) * ((p3 - p1) `2))]| by EUCLID:58
.= |[(((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1)) + (((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1)) * ((p3 - p1) `1))),(((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `2)) + (((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1)) * ((p3 - p1) `2)))]| by EUCLID:56
.= p0 - p1 by A5, A6, EUCLID:53 ;
then A8: p0 = p1 + (((((- (((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2))))) + (- ((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1)))) * p1) + ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * p2)) + (((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1)) * p3)) by A7, EUCLID:48
.= (p1 + ((((- (((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2))))) + (- ((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1)))) * p1) + ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * p2))) + (((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1)) * p3) by EUCLID:26
.= ((p1 + (((- (((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2))))) + (- ((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1)))) * p1)) + ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * p2)) + (((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1)) * p3) by EUCLID:26
.= (((1 * p1) + (((- (((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2))))) + (- ((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1)))) * p1)) + ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * p2)) + (((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1)) * p3) by EUCLID:29
.= (((1 + ((- (((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2))))) + (- ((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1))))) * p1) + ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * p2)) + (((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1)) * p3) by EUCLID:33 ;
 ((1 + ((- (((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2))))) + (- ((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1))))) + (((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2))))) + ((((p0 - p1) `1) - ((((((p0 - p1) `2) * ((p3 - p1) `1)) - (((p3 - p1) `2) * ((p0 - p1) `1))) / ((((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)))) * ((p2 - p1) `1))) / ((p3 - p1) `1)) = 1 ;
hence  x in plane (p1,p2,p3) by A8, Th52; ::_thesis: verum
end;
caseA9: (p3 - p1) `2 <> 0 ; ::_thesis: x in plane (p1,p2,p3)
now__::_thesis:_not_(((p2_-_p1)_`2)_*_((p3_-_p1)_`1))_-_(((p2_-_p1)_`1)_*_((p3_-_p1)_`2))_=_0
assume  (((p2 - p1) `2) * ((p3 - p1) `1)) - (((p2 - p1) `1) * ((p3 - p1) `2)) = 0 ; ::_thesis: contradiction
then  (p2 - p1) `1 = (((p2 - p1) `2) * ((p3 - p1) `1)) / ((p3 - p1) `2) by A9, XCMPLX_1:89;
then p2 - p1 = |[((((p2 - p1) `2) * ((p3 - p1) `1)) / ((p3 - p1) `2)),((p2 - p1) `2)]| by EUCLID:53
.= |[((((p2 - p1) `2) * ((p3 - p1) `1)) * (((p3 - p1) `2) ")),(((p2 - p1) `2) * 1)]| by XCMPLX_0:def_9
.= |[(((p2 - p1) `2) * (((p3 - p1) `1) * (((p3 - p1) `2) "))),(((p2 - p1) `2) * 1)]|
.= ((p2 - p1) `2) * |[(((p3 - p1) `1) * (((p3 - p1) `2) ")),1]| by EUCLID:58
.= ((p2 - p1) `2) * |[((((p3 - p1) `2) ") * ((p3 - p1) `1)),((((p3 - p1) `2) ") * ((p3 - p1) `2))]| by A9, XCMPLX_0:def_7
.= ((p2 - p1) `2) * ((((p3 - p1) `2) ") * |[((p3 - p1) `1),((p3 - p1) `2)]|) by EUCLID:58
.= ((p2 - p1) `2) * ((((p3 - p1) `2) ") * (p3 - p1)) by EUCLID:53
.= (((p2 - p1) `2) * (((p3 - p1) `2) ")) * (p3 - p1) by EUCLID:30 ;
then  (p2 - p1) + (- ((((p2 - p1) `2) * (((p3 - p1) `2) ")) * (p3 - p1))) = 0. (TOP-REAL 2) by EUCLID:36;
then  (1 * (p2 - p1)) + (- ((((p2 - p1) `2) * (((p3 - p1) `2) ")) * (p3 - p1))) = 0. (TOP-REAL 2) by EUCLID:29;
then  (1 * (p2 - p1)) + ((- (((p2 - p1) `2) * (((p3 - p1) `2) "))) * (p3 - p1)) = 0. (TOP-REAL 2) by EUCLID:40;
hence  contradiction by A1, Def10; ::_thesis: verum
end;
then A10: - ((((p2 - p1) `2) * ((p3 - p1) `1)) + (- (((p2 - p1) `1) * ((p3 - p1) `2)))) <> - 0 ;
set a = ((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)));
set b = (((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2);
A11: ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2)) + (((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2)) * ((p3 - p1) `2)) = ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2)) + (((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) by A9, XCMPLX_1:87
.= (p0 - p1) `2 ;
A12: ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `1)) + (((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2)) * ((p3 - p1) `1)) = ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `1)) + (((((p0 - p1) `2) / ((p3 - p1) `2)) - (((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2)) / ((p3 - p1) `2))) * ((p3 - p1) `1)) by XCMPLX_1:120
.= (((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `1)) - ((((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2)) / ((p3 - p1) `2)) * ((p3 - p1) `1))) + ((((p0 - p1) `2) / ((p3 - p1) `2)) * ((p3 - p1) `1))
.= (((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `1)) - ((((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2)) * (((p3 - p1) `2) ")) * ((p3 - p1) `1))) + ((((p0 - p1) `2) / ((p3 - p1) `2)) * ((p3 - p1) `1)) by XCMPLX_0:def_9
.= ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * (((p2 - p1) `1) - ((((p2 - p1) `2) * (((p3 - p1) `2) ")) * ((p3 - p1) `1)))) + ((((p0 - p1) `2) / ((p3 - p1) `2)) * ((p3 - p1) `1))
.= ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * (((p2 - p1) `1) - ((((p2 - p1) `2) / ((p3 - p1) `2)) * ((p3 - p1) `1)))) + ((((p0 - p1) `2) / ((p3 - p1) `2)) * ((p3 - p1) `1)) by XCMPLX_0:def_9
.= ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * (((((p2 - p1) `1) / ((p3 - p1) `2)) * ((p3 - p1) `2)) - ((((p2 - p1) `2) / ((p3 - p1) `2)) * ((p3 - p1) `1)))) + ((((p0 - p1) `2) / ((p3 - p1) `2)) * ((p3 - p1) `1)) by A9, XCMPLX_1:87
.= ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * (((((p3 - p1) `2) / ((p3 - p1) `2)) * ((p2 - p1) `1)) - ((((p2 - p1) `2) / ((p3 - p1) `2)) * ((p3 - p1) `1)))) + ((((p0 - p1) `2) / ((p3 - p1) `2)) * ((p3 - p1) `1)) by XCMPLX_1:75
.= ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * (((((p3 - p1) `2) * (((p3 - p1) `2) ")) * ((p2 - p1) `1)) - ((((p2 - p1) `2) / ((p3 - p1) `2)) * ((p3 - p1) `1)))) + ((((p0 - p1) `2) / ((p3 - p1) `2)) * ((p3 - p1) `1)) by XCMPLX_0:def_9
.= ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((((p2 - p1) `1) * (((p3 - p1) `2) * (((p3 - p1) `2) "))) - (((((p3 - p1) `2) ") * ((p2 - p1) `2)) * ((p3 - p1) `1)))) + ((((p0 - p1) `2) / ((p3 - p1) `2)) * ((p3 - p1) `1)) by XCMPLX_0:def_9
.= (((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * (((p3 - p1) `2) ")) + ((((p0 - p1) `2) / ((p3 - p1) `2)) * ((p3 - p1) `1))
.= (((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) * (((p3 - p1) `2) ")) + ((((p0 - p1) `2) / ((p3 - p1) `2)) * ((p3 - p1) `1)) by A10, XCMPLX_1:87
.= (((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) * (((p3 - p1) `2) ")) + (((((p3 - p1) `2) ") * ((p0 - p1) `2)) * ((p3 - p1) `1)) by XCMPLX_0:def_9
.= (((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) + (((p3 - p1) `1) * ((p0 - p1) `2))) * (((p3 - p1) `2) ")
.= (((p0 - p1) `1) * ((p3 - p1) `2)) / ((p3 - p1) `2) by XCMPLX_0:def_9
.= (p0 - p1) `1 by A9, XCMPLX_1:89 ;
A13: ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * (p2 - p1)) + (((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2)) * (p3 - p1)) = (((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * p2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * p1)) + (((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2)) * (p3 - p1)) by EUCLID:49
.= (((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * p2) + (- ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * p1))) + ((((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2)) * p3) - (((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2)) * p1)) by EUCLID:49
.= (((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * p2) + (- ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * p1))) + ((((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2)) * p3) + ((- ((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2))) * p1)) by EUCLID:40
.= (((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * p2) + ((- (((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1))))) * p1)) + (((- ((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2))) * p1) + (((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2)) * p3)) by EUCLID:40
.= ((((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * p2) + ((- (((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1))))) * p1)) + ((- ((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2))) * p1)) + (((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2)) * p3) by EUCLID:26
.= (((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * p2) + (((- (((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1))))) * p1) + ((- ((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2))) * p1))) + (((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2)) * p3) by EUCLID:26
.= ((((- (((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1))))) + (- ((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2)))) * p1) + ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * p2)) + (((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2)) * p3) by EUCLID:33 ;
((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * (p2 - p1)) + (((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2)) * (p3 - p1)) = ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * |[((p2 - p1) `1),((p2 - p1) `2)]|) + (((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2)) * (p3 - p1)) by EUCLID:53
.= ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * |[((p2 - p1) `1),((p2 - p1) `2)]|) + (((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2)) * |[((p3 - p1) `1),((p3 - p1) `2)]|) by EUCLID:53
.= |[((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `1)),((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))]| + (((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2)) * |[((p3 - p1) `1),((p3 - p1) `2)]|) by EUCLID:58
.= |[((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `1)),((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))]| + |[(((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2)) * ((p3 - p1) `1)),(((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2)) * ((p3 - p1) `2))]| by EUCLID:58
.= |[(((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `1)) + (((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2)) * ((p3 - p1) `1))),(((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2)) + (((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2)) * ((p3 - p1) `2)))]| by EUCLID:56
.= p0 - p1 by A11, A12, EUCLID:53 ;
then A14: p0 = p1 + (((((- (((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1))))) + (- ((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2)))) * p1) + ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * p2)) + (((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2)) * p3)) by A13, EUCLID:48
.= (p1 + ((((- (((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1))))) + (- ((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2)))) * p1) + ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * p2))) + (((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2)) * p3) by EUCLID:26
.= ((p1 + (((- (((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1))))) + (- ((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2)))) * p1)) + ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * p2)) + (((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2)) * p3) by EUCLID:26
.= (((1 * p1) + (((- (((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1))))) + (- ((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2)))) * p1)) + ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * p2)) + (((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2)) * p3) by EUCLID:29
.= (((1 + ((- (((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1))))) + (- ((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2))))) * p1) + ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * p2)) + (((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2)) * p3) by EUCLID:33 ;
 ((1 + ((- (((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1))))) + (- ((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2))))) + (((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1))))) + ((((p0 - p1) `2) - ((((((p0 - p1) `1) * ((p3 - p1) `2)) - (((p3 - p1) `1) * ((p0 - p1) `2))) / ((((p2 - p1) `1) * ((p3 - p1) `2)) - (((p2 - p1) `2) * ((p3 - p1) `1)))) * ((p2 - p1) `2))) / ((p3 - p1) `2)) = 1 ;
hence  x in plane (p1,p2,p3) by A14, Th52; ::_thesis: verum
end;
end;
end;
hence  x in plane (p1,p2,p3) ; ::_thesis: verum
end;

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 & 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 & p = ((it * p1) + (a2 * p2)) + (a3 * p3) );
existence
 ex b1, a2, a3 being Real st
( (b1 + a2) + a3 = 1 & p = ((b1 * p1) + (a2 * p2)) + (a3 * p3) )
proof
 ex a01, a02, a03 being Real st
( p = ((a01 * p1) + (a02 * p2)) + (a03 * p3) & (a01 + a02) + a03 = 1 & ( for b1, b2, b3 being Real st p = ((b1 * p1) + (b2 * p2)) + (b3 * p3) & (b1 + b2) + b3 = 1 holds
( b1 = a01 & b2 = a02 & b3 = a03 ) ) ) by A1, Th51;
hence  ex b1, a2, a3 being Real st
( (b1 + a2) + a3 = 1 & p = ((b1 * p1) + (a2 * p2)) + (a3 * p3) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Real st ex a2, a3 being Real st
( (b1 + a2) + a3 = 1 & p = ((b1 * p1) + (a2 * p2)) + (a3 * p3) ) & ex a2, a3 being Real st
( (b2 + a2) + a3 = 1 & p = ((b2 * p1) + (a2 * p2)) + (a3 * p3) ) holds
b1 = b2
proof
let a1, b1 be Real; ::_thesis: ( ex a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) & ex a2, a3 being Real st
( (b1 + a2) + a3 = 1 & p = ((b1 * p1) + (a2 * p2)) + (a3 * p3) ) implies a1 = b1 )
assume that
A2: ex a2, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) and
A3: ex a2, a3 being Real st
( (b1 + a2) + a3 = 1 & p = ((b1 * p1) + (a2 * p2)) + (a3 * p3) ) ; ::_thesis: a1 = b1
consider a001, a002, a003 being Real such that
 p = ((a001 * p1) + (a002 * p2)) + (a003 * p3) and
 (a001 + a002) + a003 = 1 and
A4: for b01, b02, b03 being 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  a1 = b1 by A3, A4; ::_thesis: verum
end;
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 & 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 & 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 & 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 & p = ((a1 * p1) + (it * p2)) + (a3 * p3) );
existence
 ex b1, a1, a3 being Real st
( (a1 + b1) + a3 = 1 & p = ((a1 * p1) + (b1 * p2)) + (a3 * p3) )
proof
 ex a01, a02, a03 being Real st
( p = ((a01 * p1) + (a02 * p2)) + (a03 * p3) & (a01 + a02) + a03 = 1 & ( for b1, b2, b3 being Real st p = ((b1 * p1) + (b2 * p2)) + (b3 * p3) & (b1 + b2) + b3 = 1 holds
( b1 = a01 & b2 = a02 & b3 = a03 ) ) ) by A1, Th51;
hence  ex b1, a1, a3 being Real st
( (a1 + b1) + a3 = 1 & p = ((a1 * p1) + (b1 * p2)) + (a3 * p3) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Real st ex a1, a3 being Real st
( (a1 + b1) + a3 = 1 & p = ((a1 * p1) + (b1 * p2)) + (a3 * p3) ) & ex a1, a3 being Real st
( (a1 + b2) + a3 = 1 & p = ((a1 * p1) + (b2 * p2)) + (a3 * p3) ) holds
b1 = b2
proof
let a2, b2 be Real; ::_thesis: ( ex a1, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) & ex a1, a3 being Real st
( (a1 + b2) + a3 = 1 & p = ((a1 * p1) + (b2 * p2)) + (a3 * p3) ) implies a2 = b2 )
assume that
A2: ex a1, a3 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) and
A3: ex a1, a3 being Real st
( (a1 + b2) + a3 = 1 & p = ((a1 * p1) + (b2 * p2)) + (a3 * p3) ) ; ::_thesis: a2 = b2
consider a001, a002, a003 being Real such that
 p = ((a001 * p1) + (a002 * p2)) + (a003 * p3) and
 (a001 + a002) + a003 = 1 and
A4: for b01, b02, b03 being 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  a2 = b2 by A3, A4; ::_thesis: verum
end;
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 & 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 & 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 & 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 & p = ((a1 * p1) + (a2 * p2)) + (it * p3) );
existence
 ex b1, a1, a2 being Real st
( (a1 + a2) + b1 = 1 & p = ((a1 * p1) + (a2 * p2)) + (b1 * p3) )
proof
 ex a01, a02, a03 being Real st
( p = ((a01 * p1) + (a02 * p2)) + (a03 * p3) & (a01 + a02) + a03 = 1 & ( for b1, b2, b3 being Real st p = ((b1 * p1) + (b2 * p2)) + (b3 * p3) & (b1 + b2) + b3 = 1 holds
( b1 = a01 & b2 = a02 & b3 = a03 ) ) ) by A1, Th51;
hence  ex b1, a1, a2 being Real st
( (a1 + a2) + b1 = 1 & p = ((a1 * p1) + (a2 * p2)) + (b1 * p3) ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Real st ex a1, a2 being Real st
( (a1 + a2) + b1 = 1 & p = ((a1 * p1) + (a2 * p2)) + (b1 * p3) ) & ex a1, a2 being Real st
( (a1 + a2) + b2 = 1 & p = ((a1 * p1) + (a2 * p2)) + (b2 * p3) ) holds
b1 = b2
proof
let a3, b3 be Real; ::_thesis: ( ex a1, a2 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) & ex a1, a2 being Real st
( (a1 + a2) + b3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (b3 * p3) ) implies a3 = b3 )
assume that
A2: ex a1, a2 being Real st
( (a1 + a2) + a3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) and
A3: ex a1, a2 being Real st
( (a1 + a2) + b3 = 1 & p = ((a1 * p1) + (a2 * p2)) + (b3 * p3) ) ; ::_thesis: a3 = b3
consider a001, a002, a003 being Real such that
 p = ((a001 * p1) + (a002 * p2)) + (a003 * p3) and
 (a001 + a002) + a003 = 1 and
A4: for b01, b02, b03 being 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  a3 = b3 by A3, A4; ::_thesis: verum
end;
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 & 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 & 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)
proof
defpred S1[ set , set ] means  for p being Point of (TOP-REAL 2) st p = $1 holds
$2 = tricord1 (p1,p2,p3,p);
set X = the carrier of (TOP-REAL 2);
set Y = the carrier of R^1;
A1: for x being set st x in the carrier of (TOP-REAL 2) holds
ex y being set st
( y in the carrier of R^1 & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in the carrier of (TOP-REAL 2) implies ex y being set st
( y in the carrier of R^1 & S1[x,y] ) )
assume  x in the carrier of (TOP-REAL 2) ; ::_thesis: ex y being set st
( y in the carrier of R^1 & S1[x,y] )
then reconsider p0 = x as Point of (TOP-REAL 2) ;
 S1[x, tricord1 (p1,p2,p3,p0)] ;
hence  ex y being set st
( y in the carrier of R^1 & S1[x,y] ) by TOPMETR:17; ::_thesis: verum
end;
 ex f being Function of the carrier of (TOP-REAL 2), the carrier of R^1 st
for x being set st x in the carrier of (TOP-REAL 2) holds
S1[x,f . x] from FUNCT_2:sch_1(A1);
then consider g being Function of the carrier of (TOP-REAL 2), the carrier of R^1 such that
A2: for x being set st x in the carrier of (TOP-REAL 2) holds
for p being Point of (TOP-REAL 2) st p = x holds
g . x = tricord1 (p1,p2,p3,p) ;
reconsider f0 = g as Function of (TOP-REAL 2),R^1 ;
 for p being Point of (TOP-REAL 2) holds f0 . p = tricord1 (p1,p2,p3,p) by A2;
hence  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) ; ::_thesis: verum
end;
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) ) & ( for p being Point of (TOP-REAL 2) holds b2 . p = tricord1 (p1,p2,p3,p) ) holds
b1 = b2
proof
let f1, f2 be Function of (TOP-REAL 2),R^1; ::_thesis: ( ( for p being Point of (TOP-REAL 2) holds f1 . p = tricord1 (p1,p2,p3,p) ) & ( for p being Point of (TOP-REAL 2) holds f2 . p = tricord1 (p1,p2,p3,p) ) implies f1 = f2 )
assume that
A3: for p being Point of (TOP-REAL 2) holds f1 . p = tricord1 (p1,p2,p3,p) and
A4: for p being Point of (TOP-REAL 2) holds f2 . p = tricord1 (p1,p2,p3,p) ; ::_thesis: f1 = f2
A5: for x being set st x in dom f1 holds
f1 . x = f2 . x
proof
let x be set ; ::_thesis: ( x in dom f1 implies f1 . x = f2 . x )
assume  x in dom f1 ; ::_thesis: f1 . x = f2 . x
then reconsider p0 = x as Point of (TOP-REAL 2) by FUNCT_2:def_1;
 f1 . p0 = tricord1 (p1,p2,p3,p0) by A3;
hence  f1 . x = f2 . x by A4; ::_thesis: verum
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; ::_thesis: verum
end;
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)
proof
defpred S1[ set , set ] means  for p being Point of (TOP-REAL 2) st p = $1 holds
$2 = tricord2 (p1,p2,p3,p);
set X = the carrier of (TOP-REAL 2);
set Y = the carrier of R^1;
A1: for x being set st x in the carrier of (TOP-REAL 2) holds
ex y being set st
( y in the carrier of R^1 & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in the carrier of (TOP-REAL 2) implies ex y being set st
( y in the carrier of R^1 & S1[x,y] ) )
assume  x in the carrier of (TOP-REAL 2) ; ::_thesis: ex y being set st
( y in the carrier of R^1 & S1[x,y] )
then reconsider p0 = x as Point of (TOP-REAL 2) ;
 S1[x, tricord2 (p1,p2,p3,p0)] ;
hence  ex y being set st
( y in the carrier of R^1 & S1[x,y] ) by TOPMETR:17; ::_thesis: verum
end;
 ex f being Function of the carrier of (TOP-REAL 2), the carrier of R^1 st
for x being set st x in the carrier of (TOP-REAL 2) holds
S1[x,f . x] from FUNCT_2:sch_1(A1);
then consider g being Function of the carrier of (TOP-REAL 2), the carrier of R^1 such that
A2: for x being set st x in the carrier of (TOP-REAL 2) holds
for p being Point of (TOP-REAL 2) st p = x holds
g . x = tricord2 (p1,p2,p3,p) ;
reconsider f0 = g as Function of (TOP-REAL 2),R^1 ;
 for p being Point of (TOP-REAL 2) holds f0 . p = tricord2 (p1,p2,p3,p) by A2;
hence  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) ; ::_thesis: verum
end;
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) ) & ( for p being Point of (TOP-REAL 2) holds b2 . p = tricord2 (p1,p2,p3,p) ) holds
b1 = b2
proof
let f1, f2 be Function of (TOP-REAL 2),R^1; ::_thesis: ( ( for p being Point of (TOP-REAL 2) holds f1 . p = tricord2 (p1,p2,p3,p) ) & ( for p being Point of (TOP-REAL 2) holds f2 . p = tricord2 (p1,p2,p3,p) ) implies f1 = f2 )
assume that
A3: for p being Point of (TOP-REAL 2) holds f1 . p = tricord2 (p1,p2,p3,p) and
A4: for p being Point of (TOP-REAL 2) holds f2 . p = tricord2 (p1,p2,p3,p) ; ::_thesis: f1 = f2
A5: for x being set st x in dom f1 holds
f1 . x = f2 . x
proof
let x be set ; ::_thesis: ( x in dom f1 implies f1 . x = f2 . x )
assume  x in dom f1 ; ::_thesis: f1 . x = f2 . x
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  f1 . x = f2 . x by A4; ::_thesis: verum
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; ::_thesis: verum
end;
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)
proof
defpred S1[ set , set ] means  for p being Point of (TOP-REAL 2) st p = $1 holds
$2 = tricord3 (p1,p2,p3,p);
set X = the carrier of (TOP-REAL 2);
set Y = the carrier of R^1;
A1: for x being set st x in the carrier of (TOP-REAL 2) holds
ex y being set st
( y in the carrier of R^1 & S1[x,y] )
proof
let x be set ; ::_thesis: ( x in the carrier of (TOP-REAL 2) implies ex y being set st
( y in the carrier of R^1 & S1[x,y] ) )
assume  x in the carrier of (TOP-REAL 2) ; ::_thesis: ex y being set st
( y in the carrier of R^1 & S1[x,y] )
then reconsider p0 = x as Point of (TOP-REAL 2) ;
 S1[x, tricord3 (p1,p2,p3,p0)] ;
hence  ex y being set st
( y in the carrier of R^1 & S1[x,y] ) by TOPMETR:17; ::_thesis: verum
end;
 ex f being Function of the carrier of (TOP-REAL 2), the carrier of R^1 st
for x being set st x in the carrier of (TOP-REAL 2) holds
S1[x,f . x] from FUNCT_2:sch_1(A1);
then consider g being Function of the carrier of (TOP-REAL 2), the carrier of R^1 such that
A2: for x being set st x in the carrier of (TOP-REAL 2) holds
for p being Point of (TOP-REAL 2) st p = x holds
g . x = tricord3 (p1,p2,p3,p) ;
reconsider f0 = g as Function of (TOP-REAL 2),R^1 ;
 for p being Point of (TOP-REAL 2) holds f0 . p = tricord3 (p1,p2,p3,p) by A2;
hence  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) ; ::_thesis: verum
end;
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) ) & ( for p being Point of (TOP-REAL 2) holds b2 . p = tricord3 (p1,p2,p3,p) ) holds
b1 = b2
proof
let f1, f2 be Function of (TOP-REAL 2),R^1; ::_thesis: ( ( for p being Point of (TOP-REAL 2) holds f1 . p = tricord3 (p1,p2,p3,p) ) & ( for p being Point of (TOP-REAL 2) holds f2 . p = tricord3 (p1,p2,p3,p) ) implies f1 = f2 )
assume that
A3: for p being Point of (TOP-REAL 2) holds f1 . p = tricord3 (p1,p2,p3,p) and
A4: for p being Point of (TOP-REAL 2) holds f2 . p = tricord3 (p1,p2,p3,p) ; ::_thesis: f1 = f2
A5: for x being set st x in dom f1 holds
f1 . x = f2 . x
proof
let x be set ; ::_thesis: ( x in dom f1 implies f1 . x = f2 . x )
assume  x in dom f1 ; ::_thesis: f1 . x = f2 . x
then reconsider p0 = x as Point of (TOP-REAL 2) by FUNCT_2:def_1;
 f1 . p0 = tricord3 (p1,p2,p3,p0) by A3;
hence  f1 . x = f2 . x by A4; ::_thesis: verum
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; ::_thesis: verum
end;
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 ) )
proof
let p1, p2, p3, p be Point of (TOP-REAL 2); ::_thesis: ( p2 - p1,p3 - p1 are_lindependent2 implies ( 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 ) ) )
set i1 = tricord1 (p1,p2,p3,p);
set i2 = tricord2 (p1,p2,p3,p);
set i3 = tricord3 (p1,p2,p3,p);
assume A1: p2 - p1,p3 - p1 are_lindependent2 ; ::_thesis: ( 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 ) )
thus  ( not p in outside_of_triangle (p1,p2,p3) or tricord1 (p1,p2,p3,p) < 0 or tricord2 (p1,p2,p3,p) < 0 or tricord3 (p1,p2,p3,p) < 0 ) ::_thesis: ( ( tricord1 (p1,p2,p3,p) < 0 or tricord2 (p1,p2,p3,p) < 0 or tricord3 (p1,p2,p3,p) < 0 ) implies p in outside_of_triangle (p1,p2,p3) )
proof
 p in the carrier of (TOP-REAL 2) ;
then  p in REAL 2 by EUCLID:22;
then A2: p in plane (p1,p2,p3) by A1, Th54;
assume  p in outside_of_triangle (p1,p2,p3) ; ::_thesis: ( tricord1 (p1,p2,p3,p) < 0 or tricord2 (p1,p2,p3,p) < 0 or tricord3 (p1,p2,p3,p) < 0 )
then  ex p0 being Point of (TOP-REAL 2) st
( p0 = p & ex a1, a2, a3 being Real st
( ( 0 > a1 or 0 > a2 or 0 > a3 ) & (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) ) ;
hence  ( tricord1 (p1,p2,p3,p) < 0 or tricord2 (p1,p2,p3,p) < 0 or tricord3 (p1,p2,p3,p) < 0 ) by A1, A2, Def11, Def12, Def13; ::_thesis: verum
end;
 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;
then consider a2, a3 being Real such that
A4: ( ((tricord1 (p1,p2,p3,p)) + a2) + a3 = 1 & p = (((tricord1 (p1,p2,p3,p)) * p1) + (a2 * p2)) + (a3 * p3) ) by A1, Def11;
assume A5: ( tricord1 (p1,p2,p3,p) < 0 or tricord2 (p1,p2,p3,p) < 0 or tricord3 (p1,p2,p3,p) < 0 ) ; ::_thesis: p in outside_of_triangle (p1,p2,p3)
 ( a2 = tricord2 (p1,p2,p3,p) & a3 = tricord3 (p1,p2,p3,p) ) by A1, A3, A4, Def12, Def13;
hence  p in outside_of_triangle (p1,p2,p3) by A5, A4; ::_thesis: verum
end;

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 & 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 be Point of (TOP-REAL 2); ::_thesis: ( p2 - p1,p3 - p1 are_lindependent2 implies ( 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 ) ) ) )
assume A1: p2 - p1,p3 - p1 are_lindependent2 ; ::_thesis: ( 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 ) ) )
A2: for p0 being Point of (TOP-REAL 2) 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 be Point of (TOP-REAL 2); ::_thesis: ( p0 in Triangle (p1,p2,p3) iff ( p0 in LSeg (p1,p2) or p0 in LSeg (p2,p3) or p0 in LSeg (p3,p1) ) )
 ( 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  ( p0 in Triangle (p1,p2,p3) iff ( p0 in LSeg (p1,p2) or p0 in LSeg (p2,p3) or p0 in LSeg (p3,p1) ) ) by XBOOLE_0:def_3; ::_thesis: verum
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 ) ) ) ::_thesis: ( 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 x = p;
assume A3: p in Triangle (p1,p2,p3) ; ::_thesis: ( 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 ) )
A4: now__::_thesis:_(_(_p_in_LSeg_(p1,p2)_&_ex_a1,_a2,_a3_being_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)_)_)_or_(_p_in_LSeg_(p2,p3)_&_ex_a1,_a2,_a3_being_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)_)_)_or_(_p_in_LSeg_(p3,p1)_&_ex_a1,_a2,_a3_being_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)_)_)_)
percases ( p in LSeg (p1,p2) or p in LSeg (p2,p3) or p in LSeg (p3,p1) ) by A2, A3;
case p in LSeg (p1,p2) ; ::_thesis: ex a1, a2, a3 being 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) )
then consider lambda being Real such that
A5: p = ((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, EUCLID:27
.= (((1 - lambda) * p1) + (lambda * p2)) + (0 * p3) by EUCLID:29 ;
A9: ((1 - lambda) + lambda) + 0 = 1 ;
 1 - lambda >= 0 by A7, XREAL_1:48;
hence  ex a1, a2, a3 being 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; ::_thesis: verum
end;
case p in LSeg (p2,p3) ; ::_thesis: ex a1, a2, a3 being 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) )
then consider lambda being Real such that
A10: p = ((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, EUCLID:27
.= ((0 * p1) + ((1 - lambda) * p2)) + (lambda * p3) by EUCLID:29 ;
A14: (0 + (1 - lambda)) + lambda = 1 ;
 1 - lambda >= 0 by A12, XREAL_1:48;
hence  ex a1, a2, a3 being 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; ::_thesis: verum
end;
case p in LSeg (p3,p1) ; ::_thesis: ex a1, a2, a3 being 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) )
then consider lambda being Real such that
A15: p = ((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, EUCLID:27
.= ((lambda * p1) + (0 * p2)) + ((1 - lambda) * p3) by EUCLID:29 ;
A19: (lambda + 0) + (1 - lambda) = 1 ;
 1 - lambda >= 0 by A17, XREAL_1:48;
hence  ex a1, a2, a3 being 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; ::_thesis: verum
end;
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  ( 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 ) ) by A1, A4, Def11, Def12, Def13; ::_thesis: verum
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) ) ::_thesis: verum
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 ) ; ::_thesis: p in Triangle (p1,p2,p3)
set i01 = tricord1 (p1,p2,p3,p);
set i02 = tricord2 (p1,p2,p3,p);
set i03 = tricord3 (p1,p2,p3,p);
 p in the carrier of (TOP-REAL 2) ;
then  p in REAL 2 by EUCLID:22;
then A24: p in plane (p1,p2,p3) by A1, Th54;
now__::_thesis:_(_(_tricord1_(p1,p2,p3,p)_=_0_&_(_p_in_LSeg_(p1,p2)_or_p_in_LSeg_(p2,p3)_or_p_in_LSeg_(p3,p1)_)_)_or_(_tricord2_(p1,p2,p3,p)_=_0_&_(_p_in_LSeg_(p1,p2)_or_p_in_LSeg_(p2,p3)_or_p_in_LSeg_(p3,p1)_)_)_or_(_tricord3_(p1,p2,p3,p)_=_0_&_(_p_in_LSeg_(p1,p2)_or_p_in_LSeg_(p2,p3)_or_p_in_LSeg_(p3,p1)_)_)_)
percases ( tricord1 (p1,p2,p3,p) = 0 or tricord2 (p1,p2,p3,p) = 0 or tricord3 (p1,p2,p3,p) = 0 ) by A23;
case tricord1 (p1,p2,p3,p) = 0 ; ::_thesis: ( p in LSeg (p1,p2) or p in LSeg (p2,p3) or p in LSeg (p3,p1) )
then consider a2, a3 being Real such that
A25: (0 + a2) + a3 = 1 and
A26: p = ((0 * p1) + (a2 * p2)) + (a3 * p3) by A1, A24, Def11;
 a2 = tricord2 (p1,p2,p3,p) 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, EUCLID:29
.= (a2 * p2) + (a3 * p3) by EUCLID:27 ;
 a3 = tricord3 (p1,p2,p3,p) 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; ::_thesis: verum
end;
case tricord2 (p1,p2,p3,p) = 0 ; ::_thesis: ( p in LSeg (p1,p2) or p in LSeg (p2,p3) or p in LSeg (p3,p1) )
then consider a1, a3 being Real such that
A29: (a1 + 0) + a3 = 1 and
A30: p = ((a1 * p1) + (0 * p2)) + (a3 * p3) by A1, A24, Def12;
 a1 = tricord1 (p1,p2,p3,p) 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, EUCLID:29
.= (a1 * p1) + (a3 * p3) by EUCLID:27 ;
 a3 = tricord3 (p1,p2,p3,p) by A1, A24, A29, A30, Def13;
then  p in  {  (((1 - lambda) * p1) + (lambda * p3)) where lambda is 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; ::_thesis: verum
end;
case tricord3 (p1,p2,p3,p) = 0 ; ::_thesis: ( p in LSeg (p1,p2) or p in LSeg (p2,p3) or p in LSeg (p3,p1) )
then consider a1, a2 being Real such that
A33: (a1 + a2) + 0 = 1 and
A34: p = ((a1 * p1) + (a2 * p2)) + (0 * p3) by A1, A24, Def13;
 a1 = tricord1 (p1,p2,p3,p) 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, EUCLID:29
.= (a1 * p1) + (a2 * p2) by EUCLID:27 ;
 a2 = tricord2 (p1,p2,p3,p) 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; ::_thesis: verum
end;
end;
end;
hence  p in Triangle (p1,p2,p3) by A2; ::_thesis: verum
end;
end;

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 & 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 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 & tricord2 (p1,p2,p3,p) > 0 & tricord3 (p1,p2,p3,p) > 0 ) )
proof
let p1, p2, p3, p be Point of (TOP-REAL 2); ::_thesis: ( p2 - p1,p3 - p1 are_lindependent2 implies ( 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 ) ) )
assume A1: p2 - p1,p3 - p1 are_lindependent2 ; ::_thesis: ( 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 ) )
A2: inside_of_triangle (p1,p2,p3) c=  {  p0 where p0 is Point of (TOP-REAL 2) : ex a1, a2, a3 being Real st
( 0 < a1 & 0 < a2 & 0 < a3 & (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )  }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in inside_of_triangle (p1,p2,p3) or x in  {  p0 where p0 is Point of (TOP-REAL 2) : ex a1, a2, a3 being Real st
( 0 < a1 & 0 < a2 & 0 < a3 & (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )  }  )
assume A3: x in inside_of_triangle (p1,p2,p3) ; ::_thesis: x in  {  p0 where p0 is Point of (TOP-REAL 2) : ex a1, a2, a3 being Real st
( 0 < a1 & 0 < a2 & 0 < a3 & (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * 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 being Point of (TOP-REAL 2) such that
A5: p0 = x and
A6: ex a1, a2, a3 being Real st
( 0 <= a1 & 0 <= a2 & 0 <= a3 & (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) ) ;
set i01 = tricord1 (p1,p2,p3,p0);
set i02 = tricord2 (p1,p2,p3,p0);
set i03 = tricord3 (p1,p2,p3,p0);
consider a1, a2, a3 being 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 = tricord1 (p1,p2,p3,p0) by A1, A10, Def11;
A13: a3 = tricord3 (p1,p2,p3,p0) by A1, A10, A11, Def13;
then A14: tricord2 (p1,p2,p3,p0) <> 0 by A1, A4, A5, A7, A9, A12, Th56;
A15: a2 = tricord2 (p1,p2,p3,p0) by A1, A10, A11, Def12;
then A16: tricord3 (p1,p2,p3,p0) <> 0 by A1, A4, A5, A7, A8, A12, Th56;
 tricord1 (p1,p2,p3,p0) <> 0 by A1, A4, A5, A8, A9, A15, A13, Th56;
hence  x in  {  p0 where p0 is Point of (TOP-REAL 2) : ex a1, a2, a3 being Real st
( 0 < a1 & 0 < a2 & 0 < a3 & (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )  }  by A5, A7, A8, A9, A10, A12, A15, A13, A14, A16; ::_thesis: verum
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 ) ) ::_thesis: ( 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
 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) ; ::_thesis: ( tricord1 (p1,p2,p3,p) > 0 & tricord2 (p1,p2,p3,p) > 0 & tricord3 (p1,p2,p3,p) > 0 )
then  p in closed_inside_of_triangle (p1,p2,p3) by XBOOLE_0:def_5;
then consider p0 being Point of (TOP-REAL 2) such that
A19: p0 = p and
A20: ex a1, a2, a3 being 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 or not tricord2 (p1,p2,p3,p0) >= 0 or not tricord3 (p1,p2,p3,p0) >= 0 or ( not tricord1 (p1,p2,p3,p0) = 0 & not tricord2 (p1,p2,p3,p0) = 0 & not tricord3 (p1,p2,p3,p0) = 0 ) ) by A1, A19, Th56;
hence  ( tricord1 (p1,p2,p3,p) > 0 & tricord2 (p1,p2,p3,p) > 0 & tricord3 (p1,p2,p3,p) > 0 ) by A1, A19, A20, A17, Def11, Def12, Def13; ::_thesis: verum
end;
  {  p0 where p0 is Point of (TOP-REAL 2) : ex a1, a2, a3 being 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  p0 where p0 is Point of (TOP-REAL 2) : ex a1, a2, a3 being Real st
( 0 < a1 & 0 < a2 & 0 < a3 & (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )  }  or x in inside_of_triangle (p1,p2,p3) )
assume  x in  {  p0 where p0 is Point of (TOP-REAL 2) : ex a1, a2, a3 being Real st
( 0 < a1 & 0 < a2 & 0 < a3 & (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )  }  ; ::_thesis: x in inside_of_triangle (p1,p2,p3)
then consider p0 being Point of (TOP-REAL 2) such that
A21: x = p0 and
A22: ex a1, a2, a3 being 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);
set i02 = tricord2 (p1,p2,p3,p0);
set i03 = tricord3 (p1,p2,p3,p0);
consider a01, a02, a03 being 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 = tricord3 (p1,p2,p3,p0) by A1, A25, Def13;
 ( a01 = tricord1 (p1,p2,p3,p0) & a02 = tricord2 (p1,p2,p3,p0) ) by A1, A25, A26, Def11, Def12;
then  not x in Triangle (p1,p2,p3) by A1, A21, A24, A27, Th56;
hence  x in inside_of_triangle (p1,p2,p3) by A23, XBOOLE_0:def_5; ::_thesis: verum
end;
then A28: inside_of_triangle (p1,p2,p3) =  {  p0 where p0 is Point of (TOP-REAL 2) : ex a1, a2, a3 being Real st
( 0 < a1 & 0 < a2 & 0 < a3 & (a1 + a2) + a3 = 1 & p0 = ((a1 * p1) + (a2 * p2)) + (a3 * p3) )  }  by A2, XBOOLE_0:def_10;
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) ) ::_thesis: verum
proof
set i1 = tricord1 (p1,p2,p3,p);
set i2 = tricord2 (p1,p2,p3,p);
set i3 = tricord3 (p1,p2,p3,p);
assume A29: ( tricord1 (p1,p2,p3,p) > 0 & tricord2 (p1,p2,p3,p) > 0 & tricord3 (p1,p2,p3,p) > 0 ) ; ::_thesis: p in inside_of_triangle (p1,p2,p3)
 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 being Real such that
A31: ( ((tricord1 (p1,p2,p3,p)) + a2) + a3 = 1 & p = (((tricord1 (p1,p2,p3,p)) * p1) + (a2 * p2)) + (a3 * p3) ) by A1, Def11;
 ( a2 = tricord2 (p1,p2,p3,p) & a3 = tricord3 (p1,p2,p3,p) ) by A1, A30, A31, Def12, Def13;
hence  p in inside_of_triangle (p1,p2,p3) by A28, A29, A31; ::_thesis: verum
end;
end;

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
proof
let p1, p2, p3 be Point of (TOP-REAL 2); ::_thesis: ( p2 - p1,p3 - p1 are_lindependent2 implies not inside_of_triangle (p1,p2,p3) is empty )
assume A1: p2 - p1,p3 - p1 are_lindependent2 ; ::_thesis: not inside_of_triangle (p1,p2,p3) is empty
set p0 = (((1 / 3) * p1) + ((1 / 3) * p2)) + ((1 / 3) * p3);
set i01 = tricord1 (p1,p2,p3,((((1 / 3) * p1) + ((1 / 3) * p2)) + ((1 / 3) * p3)));
set i02 = tricord2 (p1,p2,p3,((((1 / 3) * p1) + ((1 / 3) * p2)) + ((1 / 3) * p3)));
set i03 = tricord3 (p1,p2,p3,((((1 / 3) * p1) + ((1 / 3) * p2)) + ((1 / 3) * p3)));
 (((1 / 3) * p1) + ((1 / 3) * p2)) + ((1 / 3) * p3) in the carrier of (TOP-REAL 2) ;
then  (((1 / 3) * p1) + ((1 / 3) * p2)) + ((1 / 3) * p3) in REAL 2 by EUCLID:22;
then A2: ( ((1 / 3) + (1 / 3)) + (1 / 3) = 1 & (((1 / 3) * p1) + ((1 / 3) * p2)) + ((1 / 3) * p3) in plane (p1,p2,p3) ) by A1, Th54;
then A3: 1 / 3 = tricord3 (p1,p2,p3,((((1 / 3) * p1) + ((1 / 3) * p2)) + ((1 / 3) * p3))) by A1, Def13;
 ( 1 / 3 = tricord1 (p1,p2,p3,((((1 / 3) * p1) + ((1 / 3) * p2)) + ((1 / 3) * p3))) & 1 / 3 = tricord2 (p1,p2,p3,((((1 / 3) * p1) + ((1 / 3) * p2)) + ((1 / 3) * p3))) ) by A1, A2, Def11, Def12;
hence  not inside_of_triangle (p1,p2,p3) is empty by A1, A3, Th58; ::_thesis: verum
end;