:: EUCLID_3 semantic presentation

definition

let c₁ be Element of COMPLEX ;
func cpx2euc c₁ -> Point of (TOP-REAL 2) equals :: EUCLID_3:def 1
|[(Re a₁),(Im a₁)]|;
correctness ;

end;

:: deftheorem Def1 defines cpx2euc EUCLID_3:def 1 :

definition

let c₁ be Point of (TOP-REAL 2);
func euc2cpx c₁ -> Element of COMPLEX equals :: EUCLID_3:def 2
[*(a₁ `1 ),(a₁ `2 )*];
correctness ;

end;

:: deftheorem Def2 defines euc2cpx EUCLID_3:def 2 :

theorem Th1: :: EUCLID_3:1

for b₁ being Element of COMPLEX holds euc2cpx (cpx2euc b₁) = b₁

proof end;

theorem Th2: :: EUCLID_3:2

for b₁ being Point of (TOP-REAL 2) holds cpx2euc (euc2cpx b₁) = b₁

proof end;

theorem Th3: :: EUCLID_3:3

for b₁ being Point of (TOP-REAL 2) ex b₂ being Element of COMPLEX st b₁ = cpx2euc b₂

proof end;

theorem Th4: :: EUCLID_3:4

for b₁ being Element of COMPLEX ex b₂ being Point of (TOP-REAL 2) st b₁ = euc2cpx b₂

proof end;

theorem Th5: :: EUCLID_3:5

for b₁, b₂ being Element of COMPLEX st cpx2euc b₁ = cpx2euc b₂ holds
b₁ = b₂

proof end;

theorem Th6: :: EUCLID_3:6

for b₁, b₂ being Point of (TOP-REAL 2) st euc2cpx b₁ = euc2cpx b₂ holds
b₁ = b₂

proof end;

theorem Th7: :: EUCLID_3:7

for b₁ being Element of COMPLEX holds
( (cpx2euc b₁) `1 = Re b₁ & (cpx2euc b₁) `2 = Im b₁ ) by EUCLID:56;

theorem Th8: :: EUCLID_3:8

for b₁ being Point of (TOP-REAL 2) holds
( Re (euc2cpx b₁) = b₁ `1 & Im (euc2cpx b₁) = b₁ `2 )

proof end;

theorem Th9: :: EUCLID_3:9

for b₁, b₂ being Real holds cpx2euc [*b₁,b₂*] = |[b₁,b₂]|

proof end;

theorem Th10: :: EUCLID_3:10

for b₁, b₂ being Element of COMPLEX holds |[(Re (b₁ + b₂)),(Im (b₁ + b₂))]| = |[((Re b₁) + (Re b₂)),((Im b₁) + (Im b₂))]|

proof end;

theorem Th11: :: EUCLID_3:11

for b₁, b₂ being Element of COMPLEX holds cpx2euc (b₁ + b₂) = (cpx2euc b₁) + (cpx2euc b₂)

proof end;

theorem Th12: :: EUCLID_3:12

for b₁, b₂ being Point of (TOP-REAL 2) holds [*((b₁ + b₂) `1 ),((b₁ + b₂) `2 )*] = [*((b₁ `1 ) + (b₂ `1 )),((b₁ `2 ) + (b₂ `2 ))*]

proof end;

theorem Th13: :: EUCLID_3:13

for b₁, b₂ being Point of (TOP-REAL 2) holds euc2cpx (b₁ + b₂) = (euc2cpx b₁) + (euc2cpx b₂)

proof end;

theorem Th14: :: EUCLID_3:14

for b₁ being Element of COMPLEX holds |[(Re (- b₁)),(Im (- b₁))]| = |[(- (Re b₁)),(- (Im b₁))]|

proof end;

theorem Th15: :: EUCLID_3:15

for b₁ being Element of COMPLEX holds cpx2euc (- b₁) = - (cpx2euc b₁)

proof end;

theorem Th16: :: EUCLID_3:16

for b₁ being Point of (TOP-REAL 2) holds [*((- b₁) `1 ),((- b₁) `2 )*] = [*(- (b₁ `1 )),(- (b₁ `2 ))*]

proof end;

theorem Th17: :: EUCLID_3:17

for b₁ being Point of (TOP-REAL 2) holds euc2cpx (- b₁) = - (euc2cpx b₁)

proof end;

theorem Th18: :: EUCLID_3:18

for b₁, b₂ being Element of COMPLEX holds cpx2euc (b₁ - b₂) = (cpx2euc b₁) - (cpx2euc b₂)

proof end;

theorem Th19: :: EUCLID_3:19

for b₁, b₂ being Point of (TOP-REAL 2) holds euc2cpx (b₁ - b₂) = (euc2cpx b₁) - (euc2cpx b₂)

proof end;

theorem Th20: :: EUCLID_3:20

cpx2euc 0c = 0.REAL 2 by COMPLEX1:12, EUCLID:58;

theorem Th21: :: EUCLID_3:21

euc2cpx (0.REAL 2) = 0c by Th1, Th20;

theorem Th22: :: EUCLID_3:22

for b₁ being Point of (TOP-REAL 2) st euc2cpx b₁ = 0c holds
b₁ = 0.REAL 2 by Th2, Th20;

theorem Th23: :: EUCLID_3:23

for b₁ being Element of COMPLEX
for b₂ being Real holds cpx2euc ([*b₂,0*] * b₁) = b₂ * (cpx2euc b₁)

proof end;

theorem Th24: :: EUCLID_3:24

for b₁, b₂, b₃ being Real holds (b₁ + (0 * <i> )) * (b₂ + (b₃ * <i> )) = (b₁ * b₂) + ((b₁ * b₃) * <i> ) ;

theorem Th25: :: EUCLID_3:25

for b₁ being Real
for b₂ being Point of (TOP-REAL 2) holds euc2cpx (b₁ * b₂) = [*b₁,0*] * (euc2cpx b₂)

proof end;

theorem Th26: :: EUCLID_3:26

for b₁ being Point of (TOP-REAL 2) holds |.(euc2cpx b₁).| = sqrt (((b₁ `1 ) ^2 ) + ((b₁ `2 ) ^2 ))

proof end;

theorem Th27: :: EUCLID_3:27

for b₁ being FinSequence of REAL st len b₁ = 2 holds
|.b₁.| = sqrt (((b₁ . 1) ^2 ) + ((b₁ . 2) ^2 ))

proof end;

theorem Th28: :: EUCLID_3:28

for b₁ being FinSequence of REAL
for b₂ being Point of (TOP-REAL 2) st len b₁ = 2 & b₂ = b₁ holds
|.b₂.| = |.b₁.|

proof end;

theorem Th29: :: EUCLID_3:29

for b₁ being Element of COMPLEX holds |.(cpx2euc b₁).| = sqrt (((Re b₁) ^2 ) + ((Im b₁) ^2 ))

proof end;

theorem Th30: :: EUCLID_3:30

for b₁ being Element of COMPLEX holds |.(cpx2euc b₁).| = |.b₁.|

proof end;

theorem Th31: :: EUCLID_3:31

for b₁ being Point of (TOP-REAL 2) holds |.(euc2cpx b₁).| = |.b₁.|

proof end;

definition

let c₁ be Point of (TOP-REAL 2);
func Arg c₁ -> Real equals :: EUCLID_3:def 3
Arg (euc2cpx a₁);
correctness ;

end;

:: deftheorem Def3 defines Arg EUCLID_3:def 3 :

theorem Th32: :: EUCLID_3:32

for b₁ being Element of COMPLEX
for b₂ being Point of (TOP-REAL 2) st ( b₁ = euc2cpx b₂ or b₂ = cpx2euc b₁ ) holds
Arg b₁ = Arg b₂

proof end;

theorem Th33: :: EUCLID_3:33

for b₁ being Point of (TOP-REAL 2) holds
( 0 <= Arg b₁ & Arg b₁ < 2 * PI ) by COMPTRIG:52;

theorem Th34: :: EUCLID_3:34

for b₁, b₂ being Real
for b₃ being Point of (TOP-REAL 2) st b₁ = |.b₃.| * (cos (Arg b₃)) & b₂ = |.b₃.| * (sin (Arg b₃)) holds
b₃ = |[b₁,b₂]|

proof end;

theorem Th35: :: EUCLID_3:35

Arg (0.REAL 2) = 0 by Th21, COMPLEX2:20;

theorem Th36: :: EUCLID_3:36

for b₁ being Point of (TOP-REAL 2) st b₁ <> 0.REAL 2 holds
( ( Arg b₁ < PI implies Arg (- b₁) = (Arg b₁) + PI ) & ( Arg b₁ >= PI implies Arg (- b₁) = (Arg b₁) - PI ) )

proof end;

theorem Th37: :: EUCLID_3:37

for b₁ being Point of (TOP-REAL 2) st Arg b₁ = 0 holds
( b₁ = |[|.b₁.|,0]| & b₁ `2 = 0 )

proof end;

theorem Th38: :: EUCLID_3:38

for b₁ being Point of (TOP-REAL 2) st b₁ <> 0.REAL 2 holds
( Arg b₁ < PI iff Arg (- b₁) >= PI )

proof end;

theorem Th39: :: EUCLID_3:39

for b₁, b₂ being Point of (TOP-REAL 2) st ( b₁ <> b₂ or b₁ - b₂ <> 0.REAL 2 ) holds
( Arg (b₁ - b₂) < PI iff Arg (b₂ - b₁) >= PI )

proof end;

theorem Th40: :: EUCLID_3:40

for b₁ being Point of (TOP-REAL 2) holds
( Arg b₁ in ].0,PI .[ iff b₁ `2 > 0 )

proof end;

theorem Th41: :: EUCLID_3:41

for b₁ being Point of (TOP-REAL 2) st Arg b₁ <> 0 holds
( Arg b₁ < PI iff sin (Arg b₁) > 0 ) by COMPLEX2:28;

theorem Th42: :: EUCLID_3:42

for b₁, b₂ being Point of (TOP-REAL 2) st Arg b₁ < PI & Arg b₂ < PI holds
Arg (b₁ + b₂) < PI

proof end;

definition

let c₁, c₂, c₃ be Point of (TOP-REAL 2);
func angle c₁,c₂,c₃ -> Real equals :: EUCLID_3:def 4
angle (euc2cpx a₁),(euc2cpx a₂),(euc2cpx a₃);
correctness by XREAL_0:def 1;

end;

:: deftheorem Def4 defines angle EUCLID_3:def 4 :

theorem Th43: :: EUCLID_3:43

for b₁, b₂, b₃ being Point of (TOP-REAL 2) holds
( 0 <= angle b₁,b₂,b₃ & angle b₁,b₂,b₃ < 2 * PI ) by COMPLEX2:84;

theorem Th44: :: EUCLID_3:44

for b₁, b₂, b₃ being Point of (TOP-REAL 2) holds angle b₁,b₂,b₃ = angle (b₁ - b₂),(0.REAL 2),(b₃ - b₂)

proof end;

theorem Th45: :: EUCLID_3:45

for b₁, b₂, b₃ being Point of (TOP-REAL 2) st angle b₁,b₂,b₃ = 0 holds
( Arg (b₁ - b₂) = Arg (b₃ - b₂) & angle b₃,b₂,b₁ = 0 )

proof end;

theorem Th46: :: EUCLID_3:46

for b₁, b₂, b₃ being Point of (TOP-REAL 2) st angle b₁,b₂,b₃ <> 0 holds
angle b₃,b₂,b₁ = (2 * PI ) - (angle b₁,b₂,b₃)

proof end;

theorem Th47: :: EUCLID_3:47

for b₁, b₂, b₃ being Point of (TOP-REAL 2) st angle b₃,b₂,b₁ <> 0 holds
angle b₃,b₂,b₁ = (2 * PI ) - (angle b₁,b₂,b₃)

proof end;

theorem Th48: :: EUCLID_3:48

for b₁, b₂ being Element of COMPLEX holds Re (b₁ .|. b₂) = ((Re b₁) * (Re b₂)) + ((Im b₁) * (Im b₂))

proof end;

theorem Th49: :: EUCLID_3:49

for b₁, b₂ being Element of COMPLEX holds Im (b₁ .|. b₂) = (- ((Re b₁) * (Im b₂))) + ((Im b₁) * (Re b₂))

proof end;

theorem Th50: :: EUCLID_3:50

for b₁, b₂ being Point of (TOP-REAL 2) holds |(b₁,b₂)| = ((b₁ `1 ) * (b₂ `1 )) + ((b₁ `2 ) * (b₂ `2 ))

proof end;

theorem Th51: :: EUCLID_3:51

for b₁, b₂ being Point of (TOP-REAL 2) holds |(b₁,b₂)| = Re ((euc2cpx b₁) .|. (euc2cpx b₂))

proof end;

theorem Th52: :: EUCLID_3:52

for b₁, b₂, b₃ being Point of (TOP-REAL 2) st b₁ <> 0.REAL 2 & b₂ <> 0.REAL 2 holds
( |(b₁,b₂)| = 0 iff ( angle b₁,(0.REAL 2),b₂ = PI / 2 or angle b₁,(0.REAL 2),b₂ = (3 / 2) * PI ) )

proof end;

theorem Th53: :: EUCLID_3:53

for b₁, b₂ being Point of (TOP-REAL 2) st b₁ <> 0.REAL 2 & b₂ <> 0.REAL 2 holds
( ( ( not (- ((b₁ `1 ) * (b₂ `2 ))) + ((b₁ `2 ) * (b₂ `1 )) = |.b₁.| * |.b₂.| & not (- ((b₁ `1 ) * (b₂ `2 ))) + ((b₁ `2 ) * (b₂ `1 )) = - (|.b₁.| * |.b₂.|) ) or angle b₁,(0.REAL 2),b₂ = PI / 2 or angle b₁,(0.REAL 2),b₂ = (3 / 2) * PI ) & ( ( not angle b₁,(0.REAL 2),b₂ = PI / 2 & not angle b₁,(0.REAL 2),b₂ = (3 / 2) * PI ) or (- ((b₁ `1 ) * (b₂ `2 ))) + ((b₁ `2 ) * (b₂ `1 )) = |.b₁.| * |.b₂.| or (- ((b₁ `1 ) * (b₂ `2 ))) + ((b₁ `2 ) * (b₂ `1 )) = - (|.b₁.| * |.b₂.|) ) )

proof end;

theorem Th54: :: EUCLID_3:54

for b₁, b₂, b₃ being Point of (TOP-REAL 2) st b₁ <> b₂ & b₃ <> b₂ holds
( |((b₁ - b₂),(b₃ - b₂))| = 0 iff ( angle b₁,b₂,b₃ = PI / 2 or angle b₁,b₂,b₃ = (3 / 2) * PI ) )

proof end;

theorem Th55: :: EUCLID_3:55

for b₁, b₂, b₃ being Point of (TOP-REAL 2) st b₁ <> b₂ & b₃ <> b₂ & ( angle b₁,b₂,b₃ = PI / 2 or angle b₁,b₂,b₃ = (3 / 2) * PI ) holds
(|.(b₁ - b₂).| ^2 ) + (|.(b₃ - b₂).| ^2 ) = |.(b₁ - b₃).| ^2

proof end;

theorem Th56: :: EUCLID_3:56

for b₁, b₂, b₃ being Point of (TOP-REAL 2) st b₂ <> b₁ & b₁ <> b₃ & b₃ <> b₂ & angle b₂,b₁,b₃ < PI & angle b₁,b₃,b₂ < PI & angle b₃,b₂,b₁ < PI holds
((angle b₂,b₁,b₃) + (angle b₁,b₃,b₂)) + (angle b₃,b₂,b₁) = PI

proof end;

definition

let c₁ be Nat;
let c₂, c₃, c₄ be Point of (TOP-REAL c₁);
func Triangle c₂,c₃,c₄ -> Subset of (TOP-REAL a₁) equals :: EUCLID_3:def 5
((LSeg a₂,a₃) \/ (LSeg a₃,a₄)) \/ (LSeg a₄,a₂);
correctness ;

end;

:: deftheorem Def5 defines Triangle EUCLID_3:def 5 :

definition

let c₁ be Nat;
let c₂, c₃, c₄ be Point of (TOP-REAL c₁);
func closed_inside_of_triangle c₂,c₃,c₄ -> Subset of (TOP-REAL a₁) equals :: EUCLID_3:def 6
{ b₁ where B is Point of (TOP-REAL a₁) : ex b₁, b₂, b₃ being Real st
( 0 <= b₂ & 0 <= b₃ & 0 <= b₄ & (b₂ + b₃) + b₄ = 1 & b₁ = ((b₂ * a₂) + (b₃ * a₃)) + (b₄ * a₄) ) } ;
correctness

proof end;

end;

:: deftheorem Def6 defines closed_inside_of_triangle EUCLID_3:def 6 :

definition

let c₁ be Nat;
let c₂, c₃, c₄ be Point of (TOP-REAL c₁);
func inside_of_triangle c₂,c₃,c₄ -> Subset of (TOP-REAL a₁) equals :: EUCLID_3:def 7
(closed_inside_of_triangle a₂,a₃,a₄) \ (Triangle a₂,a₃,a₄);
correctness ;

end;

:: deftheorem Def7 defines inside_of_triangle EUCLID_3:def 7 :

definition

let c₁ be Nat;
let c₂, c₃, c₄ be Point of (TOP-REAL c₁);
func outside_of_triangle c₂,c₃,c₄ -> Subset of (TOP-REAL a₁) equals :: EUCLID_3:def 8
{ b₁ where B is Point of (TOP-REAL a₁) : ex b₁, b₂, b₃ being Real st
( ( 0 > b₂ or 0 > b₃ or 0 > b₄ ) & (b₂ + b₃) + b₄ = 1 & b₁ = ((b₂ * a₂) + (b₃ * a₃)) + (b₄ * a₄) ) } ;
correctness

proof end;

end;

:: deftheorem Def8 defines outside_of_triangle EUCLID_3:def 8 :

definition

let c₁ be Nat;
let c₂, c₃, c₄ be Point of (TOP-REAL c₁);
func plane c₂,c₃,c₄ -> Subset of (TOP-REAL a₁) equals :: EUCLID_3:def 9
(outside_of_triangle a₂,a₃,a₄) \/ (closed_inside_of_triangle a₂,a₃,a₄);
correctness ;

end;

:: deftheorem Def9 defines plane EUCLID_3:def 9 :

theorem Th57: :: EUCLID_3:57

for b₁ being Nat
for b₂, b₃, b₄, b₅ being Point of (TOP-REAL b₁) st b₅ in plane b₂,b₃,b₄ holds
ex b₆, b₇, b₈ being Real st
( (b₆ + b₇) + b₈ = 1 & b₅ = ((b₆ * b₂) + (b₇ * b₃)) + (b₈ * b₄) )

proof end;

theorem Th58: :: EUCLID_3:58

for b₁ being Nat
for b₂, b₃, b₄ being Point of (TOP-REAL b₁) holds Triangle b₂,b₃,b₄ c= closed_inside_of_triangle b₂,b₃,b₄

proof end;

definition

let c₁ be Nat;
let c₂, c₃ be Point of (TOP-REAL c₁);
pred c₂,c₃ are_lindependent2 means :Def10: :: EUCLID_3:def 10
for b₁, b₂ being Real st (b₁ * a₂) + (b₂ * a₃) = 0.REAL a₁ holds
( b₁ = 0 & b₂ = 0 );

end;

:: deftheorem Def10 defines are_lindependent2 EUCLID_3:def 10 :

notation

let c₁ be Nat;
let c₂, c₃ be Point of (TOP-REAL c₁);
antonym c₂,c₃ are_ldependent2 for c₂,c₃ are_lindependent2 ;

end;

theorem Th59: :: EUCLID_3:59

for b₁ being Nat
for b₂, b₃ being Point of (TOP-REAL b₁) st b₂,b₃ are_lindependent2 holds
( b₂ <> b₃ & b₂ <> 0.REAL b₁ & b₃ <> 0.REAL b₁ )

proof end;

theorem Th60: :: EUCLID_3:60

for b₁ being Nat
for b₂, b₃, b₄, b₅ being Point of (TOP-REAL b₁) st b₃ - b₂,b₄ - b₂ are_lindependent2 & b₅ in plane b₂,b₃,b₄ holds
ex b₆, b₇, b₈ being Real st
( b₅ = ((b₆ * b₂) + (b₇ * b₃)) + (b₈ * b₄) & (b₆ + b₇) + b₈ = 1 & ( for b₉, b₁₀, b₁₁ being Real st b₅ = ((b₉ * b₂) + (b₁₀ * b₃)) + (b₁₁ * b₄) & (b₉ + b₁₀) + b₁₁ = 1 holds
( b₉ = b₆ & b₁₀ = b₇ & b₁₁ = b₈ ) ) )

proof end;

theorem Th61: :: EUCLID_3:61

for b₁ being Nat
for b₂, b₃, b₄, b₅ being Point of (TOP-REAL b₁) st ex b₆, b₇, b₈ being Real st
( b₅ = ((b₆ * b₂) + (b₇ * b₃)) + (b₈ * b₄) & (b₆ + b₇) + b₈ = 1 ) holds
b₅ in plane b₂,b₃,b₄

proof end;

theorem Th62: :: EUCLID_3:62

for b₁ being Nat
for b₂, b₃, b₄ being Point of (TOP-REAL b₁) holds plane b₂,b₃,b₄ = { b₅ where B is Point of (TOP-REAL b₁) : ex b₁, b₂, b₃ being Real st
( (b₆ + b₇) + b₈ = 1 & b₅ = ((b₆ * b₂) + (b₇ * b₃)) + (b₈ * b₄) ) }

proof end;

theorem Th63: :: EUCLID_3:63

for b₁, b₂, b₃ being Point of (TOP-REAL 2) st b₂ - b₁,b₃ - b₁ are_lindependent2 holds
plane b₁,b₂,b₃ = REAL 2

proof end;

definition

let c₁ be Nat;
let c₂, c₃, c₄, c₅ be Point of (TOP-REAL c₁);
assume E33: ( c₃ - c₂,c₄ - c₂ are_lindependent2 & c₅ in plane c₂,c₃,c₄ ) ;
func tricord1 c₂,c₃,c₄,c₅ -> Real means :Def11: :: EUCLID_3:def 11
ex b₁, b₂ being Real st
( (a₆ + b₁) + b₂ = 1 & a₅ = ((a₆ * a₂) + (b₁ * a₃)) + (b₂ * a₄) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines tricord1 EUCLID_3:def 11 :

definition

let c₁ be Nat;
let c₂, c₃, c₄, c₅ be Point of (TOP-REAL c₁);
assume E34: ( c₃ - c₂,c₄ - c₂ are_lindependent2 & c₅ in plane c₂,c₃,c₄ ) ;
func tricord2 c₂,c₃,c₄,c₅ -> Real means :Def12: :: EUCLID_3:def 12
ex b₁, b₂ being Real st
( (b₁ + a₆) + b₂ = 1 & a₅ = ((b₁ * a₂) + (a₆ * a₃)) + (b₂ * a₄) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines tricord2 EUCLID_3:def 12 :

definition

let c₁ be Nat;
let c₂, c₃, c₄, c₅ be Point of (TOP-REAL c₁);
assume E35: ( c₃ - c₂,c₄ - c₂ are_lindependent2 & c₅ in plane c₂,c₃,c₄ ) ;
func tricord3 c₂,c₃,c₄,c₅ -> Real means :Def13: :: EUCLID_3:def 13
ex b₁, b₂ being Real st
( (b₁ + b₂) + a₆ = 1 & a₅ = ((b₁ * a₂) + (b₂ * a₃)) + (a₆ * a₄) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines tricord3 EUCLID_3:def 13 :

definition

let c₁, c₂, c₃ be Point of (TOP-REAL 2);
func trcmap1 c₁,c₂,c₃ -> Function of (TOP-REAL 2),R^1 means :: EUCLID_3:def 14
for b₁ being Point of (TOP-REAL 2) holds a₄ . b₁ = tricord1 a₁,a₂,a₃,b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines trcmap1 EUCLID_3:def 14 :

definition

let c₁, c₂, c₃ be Point of (TOP-REAL 2);
func trcmap2 c₁,c₂,c₃ -> Function of (TOP-REAL 2),R^1 means :: EUCLID_3:def 15
for b₁ being Point of (TOP-REAL 2) holds a₄ . b₁ = tricord2 a₁,a₂,a₃,b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines trcmap2 EUCLID_3:def 15 :

definition

let c₁, c₂, c₃ be Point of (TOP-REAL 2);
func trcmap3 c₁,c₂,c₃ -> Function of (TOP-REAL 2),R^1 means :: EUCLID_3:def 16
for b₁ being Point of (TOP-REAL 2) holds a₄ . b₁ = tricord3 a₁,a₂,a₃,b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16 defines trcmap3 EUCLID_3:def 16 :

theorem Th64: :: EUCLID_3:64

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2) st b₂ - b₁,b₃ - b₁ are_lindependent2 holds
( b₄ in outside_of_triangle b₁,b₂,b₃ iff ( tricord1 b₁,b₂,b₃,b₄ < 0 or tricord2 b₁,b₂,b₃,b₄ < 0 or tricord3 b₁,b₂,b₃,b₄ < 0 ) )

proof end;

theorem Th65: :: EUCLID_3:65

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2) st b₂ - b₁,b₃ - b₁ are_lindependent2 holds
( b₄ in Triangle b₁,b₂,b₃ iff ( tricord1 b₁,b₂,b₃,b₄ >= 0 & tricord2 b₁,b₂,b₃,b₄ >= 0 & tricord3 b₁,b₂,b₃,b₄ >= 0 & ( tricord1 b₁,b₂,b₃,b₄ = 0 or tricord2 b₁,b₂,b₃,b₄ = 0 or tricord3 b₁,b₂,b₃,b₄ = 0 ) ) )

proof end;

theorem Th66: :: EUCLID_3:66

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2) st b₂ - b₁,b₃ - b₁ are_lindependent2 holds
( b₄ in Triangle b₁,b₂,b₃ iff ( ( tricord1 b₁,b₂,b₃,b₄ = 0 & tricord2 b₁,b₂,b₃,b₄ >= 0 & tricord3 b₁,b₂,b₃,b₄ >= 0 ) or ( tricord1 b₁,b₂,b₃,b₄ >= 0 & tricord2 b₁,b₂,b₃,b₄ = 0 & tricord3 b₁,b₂,b₃,b₄ >= 0 ) or ( tricord1 b₁,b₂,b₃,b₄ >= 0 & tricord2 b₁,b₂,b₃,b₄ >= 0 & tricord3 b₁,b₂,b₃,b₄ = 0 ) ) ) by Th65;

theorem Th67: :: EUCLID_3:67

for b₁, b₂, b₃, b₄ being Point of (TOP-REAL 2) st b₂ - b₁,b₃ - b₁ are_lindependent2 holds
( b₄ in inside_of_triangle b₁,b₂,b₃ iff ( tricord1 b₁,b₂,b₃,b₄ > 0 & tricord2 b₁,b₂,b₃,b₄ > 0 & tricord3 b₁,b₂,b₃,b₄ > 0 ) )

proof end;

theorem Th68: :: EUCLID_3:68

for b₁, b₂, b₃ being Point of (TOP-REAL 2) st b₂ - b₁,b₃ - b₁ are_lindependent2 holds
not inside_of_triangle b₁,b₂,b₃ is empty

proof end;