:: EUCLID_4 semantic presentation

begin


theorem Th1: :: EUCLID_4:1
for n being Nat
for x being Element of REAL n holds
( (0 * x) + x = x & x + (0* n) = x )
proof
let n be Nat; ::_thesis: for x being Element of REAL n holds
( (0 * x) + x = x & x + (0* n) = x )
let x be Element of REAL n; ::_thesis: ( (0 * x) + x = x & x + (0* n) = x )
reconsider x9 = x as Element of n -tuples_on REAL ;
(0 * x) + x = (0 * x9) + (1 * x9) by RVSUM_1:52
.= (0 + 1) * x9 by RVSUM_1:50
.= x by RVSUM_1:52 ;
hence  ( (0 * x) + x = x & x + (0* n) = x ) by RVSUM_1:16; ::_thesis: verum
end;

theorem Th2: :: EUCLID_4:2
for a being Real
for n being Nat holds a * (0* n) = 0* n
proof
let a be Real; ::_thesis: for n being Nat holds a * (0* n) = 0* n
let n be Nat; ::_thesis: a * (0* n) = 0* n
|.(a * (0* n)).| = (abs a) * |.(0* n).| by EUCLID:11
.= (abs a) * 0 by EUCLID:7
.= 0 ;
hence  a * (0* n) = 0* n by EUCLID:8; ::_thesis: verum
end;

theorem Th3: :: EUCLID_4:3
for n being Nat
for x being Element of REAL n holds
( 1 * x = x & 0 * x = 0* n )
proof
let n be Nat; ::_thesis: for x being Element of REAL n holds
( 1 * x = x & 0 * x = 0* n )
let x be Element of REAL n; ::_thesis: ( 1 * x = x & 0 * x = 0* n )
reconsider x9 = x as Element of n -tuples_on REAL ;
0 * x = ((0 * x9) + x9) - x9 by RVSUM_1:42
.= x9 - x9 by Th1
.= 0* n by RVSUM_1:37 ;
hence  ( 1 * x = x & 0 * x = 0* n ) by RVSUM_1:52; ::_thesis: verum
end;

theorem :: EUCLID_4:4
for a, b being Real
for n being Nat
for x being Element of REAL n holds (a * b) * x = a * (b * x) by RVSUM_1:49;

theorem :: EUCLID_4:5
for a being Real
for n being Nat
for x being Element of REAL n holds
( not a * x = 0* n or a = 0 or x = 0* n )
proof
let a be Real; ::_thesis: for n being Nat
for x being Element of REAL n holds
( not a * x = 0* n or a = 0 or x = 0* n )
let n be Nat; ::_thesis: for x being Element of REAL n holds
( not a * x = 0* n or a = 0 or x = 0* n )
let x be Element of REAL n; ::_thesis: ( not a * x = 0* n or a = 0 or x = 0* n )
assume that
A1: a * x = 0* n and
A2: a <> 0 ; ::_thesis: x = 0* n
thus x = 1 * x by Th3
.= ((1 / a) * a) * x by A2, XCMPLX_1:106
.= (1 / a) * (a * x) by RVSUM_1:49
.= 0* n by A1, Th2 ; ::_thesis: verum
end;

theorem :: EUCLID_4:6
for a being Real
for n being Nat
for x1, x2 being Element of REAL n holds a * (x1 + x2) = (a * x1) + (a * x2) by RVSUM_1:51;

theorem :: EUCLID_4:7
for a, b being Real
for n being Nat
for x being Element of REAL n holds (a + b) * x = (a * x) + (b * x) by RVSUM_1:50;

theorem :: EUCLID_4:8
for a being Real
for n being Nat
for x1, x2 being Element of REAL n holds
( not a * x1 = a * x2 or a = 0 or x1 = x2 )
proof
let a be Real; ::_thesis: for n being Nat
for x1, x2 being Element of REAL n holds
( not a * x1 = a * x2 or a = 0 or x1 = x2 )
let n be Nat; ::_thesis: for x1, x2 being Element of REAL n holds
( not a * x1 = a * x2 or a = 0 or x1 = x2 )
let x1, x2 be Element of REAL n; ::_thesis: ( not a * x1 = a * x2 or a = 0 or x1 = x2 )
assume that
A1: a * x1 = a * x2 and
A2: a <> 0 ; ::_thesis: x1 = x2
 ((1 / a) * a) * x1 = (1 / a) * (a * x2) by A1, RVSUM_1:49;
then  ((1 / a) * a) * x1 = ((1 / a) * a) * x2 by RVSUM_1:49;
then  1 * x1 = ((1 / a) * a) * x2 by A2, XCMPLX_1:106;
then  1 * x1 = 1 * x2 by A2, XCMPLX_1:106;
hence x1 = 1 * x2 by Th3
.= x2 by Th3 ;
::_thesis: verum
end;

definition
let n be Nat;
let x1, x2 be Element of REAL n;
func Line (x1,x2) ->  Subset of (REAL n) equals :: EUCLID_4:def 1
 {  (((1 - lambda) * x1) + (lambda * x2)) where lambda is Real : verum  }  ;
coherence
  {  (((1 - lambda) * x1) + (lambda * x2)) where lambda is Real : verum  }  is Subset of (REAL n)
proof
set A =  {  (((1 - lambda) * x1) + (lambda * x2)) where lambda is Real : verum  }  ;
  {  (((1 - lambda) * x1) + (lambda * x2)) where lambda is Real : verum  }  c= REAL n
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (((1 - lambda) * x1) + (lambda * x2)) where lambda is Real : verum  }  or x in REAL n )
assume  x in  {  (((1 - lambda) * x1) + (lambda * x2)) where lambda is Real : verum  }  ; ::_thesis: x in REAL n
then  ex lambda being Real st x = ((1 - lambda) * x1) + (lambda * x2) ;
hence  x in REAL n ; ::_thesis: verum
end;
hence   {  (((1 - lambda) * x1) + (lambda * x2)) where lambda is Real : verum  }  is Subset of (REAL n) ; ::_thesis: verum
end;
end;

:: deftheorem  defines Line EUCLID_4:def_1_:_
 for n being Nat
for x1, x2 being Element of REAL n holds Line (x1,x2) =  {  (((1 - lambda) * x1) + (lambda * x2)) where lambda is Real : verum  }  ;

registration
let n be Nat;
let x1, x2 be Element of REAL n;
cluster Line (x1,x2) ->  non empty ;
coherence
 not Line (x1,x2) is empty
proof
A1: ( 1 - 0 = 1 & 1 * x1 = x1 ) by Th3;
 ( 0 * x2 = 0* n & x1 + (0* n) = x1 ) by Th1, Th3;
then  x1 in Line (x1,x2) by A1;
hence  not Line (x1,x2) is empty ; ::_thesis: verum
end;
end;

Lm1:  for n being Nat
for x1, x2 being Element of REAL n holds Line (x1,x2) c= Line (x2,x1)
proof
let n be Nat; ::_thesis: for x1, x2 being Element of REAL n holds Line (x1,x2) c= Line (x2,x1)
let x1, x2 be Element of REAL n; ::_thesis: Line (x1,x2) c= Line (x2,x1)
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Line (x1,x2) or z in Line (x2,x1) )
assume  z in Line (x1,x2) ; ::_thesis: z in Line (x2,x1)
then consider t being Real such that
A1: z = ((1 - t) * x1) + (t * x2) ;
 z = ((1 - (1 - t)) * x2) + ((1 - t) * x1) by A1;
hence  z in Line (x2,x1) ; ::_thesis: verum
end;

definition
let n be Nat;
let x1, x2 be Element of REAL n;
:: original: Line
redefine func Line (x1,x2) ->  Subset of (REAL n);
commutativity
 for x1, x2 being Element of REAL n holds Line (x1,x2) = Line (x2,x1)
proof
let x1, x2 be Element of REAL n; ::_thesis: Line (x1,x2) = Line (x2,x1)
 ( Line (x1,x2) c= Line (x2,x1) & Line (x2,x1) c= Line (x1,x2) ) by Lm1;
hence  Line (x1,x2) = Line (x2,x1) by XBOOLE_0:def_10; ::_thesis: verum
end;
end;

theorem Th9: :: EUCLID_4:9
for n being Nat
for x1, x2 being Element of REAL n holds
( x1 in Line (x1,x2) & x2 in Line (x1,x2) )
proof
let n be Nat; ::_thesis: for x1, x2 being Element of REAL n holds
( x1 in Line (x1,x2) & x2 in Line (x1,x2) )
let x1, x2 be Element of REAL n; ::_thesis: ( x1 in Line (x1,x2) & x2 in Line (x1,x2) )
A1: ( 1 - 0 = 1 & 1 * x1 = x1 ) by Th3;
A2: ( 1 - 1 = 0 & 0 * x1 = 0* n ) by Th3;
A3: ( 1 * x2 = x2 & (0* n) + x2 = x2 ) by Th1, Th3;
 ( 0 * x2 = 0* n & x1 + (0* n) = x1 ) by Th1, Th3;
hence  ( x1 in Line (x1,x2) & x2 in Line (x1,x2) ) by A1, A2, A3; ::_thesis: verum
end;

Lm2:  for n being Nat
for x1, x2, x3 being Element of REAL n holds x1 + (x2 + x3) = (x1 + x2) + x3
by FINSEQOP:28;

theorem Th10: :: EUCLID_4:10
for n being Nat
for y1, x1, x2, y2 being Element of REAL n st y1 in Line (x1,x2) & y2 in Line (x1,x2) holds
Line (y1,y2) c= Line (x1,x2)
proof
let n be Nat; ::_thesis: for y1, x1, x2, y2 being Element of REAL n st y1 in Line (x1,x2) & y2 in Line (x1,x2) holds
Line (y1,y2) c= Line (x1,x2)
let y1, x1, x2, y2 be Element of REAL n; ::_thesis: ( y1 in Line (x1,x2) & y2 in Line (x1,x2) implies Line (y1,y2) c= Line (x1,x2) )
assume  y1 in Line (x1,x2) ; ::_thesis: ( not y2 in Line (x1,x2) or Line (y1,y2) c= Line (x1,x2) )
then consider t being Real such that
A1: y1 = ((1 - t) * x1) + (t * x2) ;
assume  y2 in Line (x1,x2) ; ::_thesis: Line (y1,y2) c= Line (x1,x2)
then consider s being Real such that
A2: y2 = ((1 - s) * x1) + (s * x2) ;
now__::_thesis:_for_z_being_set_st_z_in_Line_(y1,y2)_holds_
z_in_Line_(x1,x2)
let z be set ; ::_thesis: ( z in Line (y1,y2) implies z in Line (x1,x2) )
assume  z in Line (y1,y2) ; ::_thesis: z in Line (x1,x2)
then consider u being Real such that
A3: z = ((1 - u) * y1) + (u * y2) ;
z = (((1 - u) * ((1 - t) * x1)) + ((1 - u) * (t * x2))) + (u * (((1 - s) * x1) + (s * x2))) by A1, A2, A3, RVSUM_1:51
.= (((1 - u) * ((1 - t) * x1)) + ((1 - u) * (t * x2))) + ((u * ((1 - s) * x1)) + (u * (s * x2))) by RVSUM_1:51
.= ((((1 - u) * (1 - t)) * x1) + ((1 - u) * (t * x2))) + ((u * ((1 - s) * x1)) + (u * (s * x2))) by RVSUM_1:49
.= ((((1 - u) * (1 - t)) * x1) + (((1 - u) * t) * x2)) + ((u * ((1 - s) * x1)) + (u * (s * x2))) by RVSUM_1:49
.= ((((1 - u) * (1 - t)) * x1) + (((1 - u) * t) * x2)) + (((u * (1 - s)) * x1) + (u * (s * x2))) by RVSUM_1:49
.= ((((1 - u) * (1 - t)) * x1) + (((1 - u) * t) * x2)) + (((u * (1 - s)) * x1) + ((u * s) * x2)) by RVSUM_1:49
.= (((1 - u) * (1 - t)) * x1) + ((((1 - u) * t) * x2) + (((u * (1 - s)) * x1) + ((u * s) * x2))) by FINSEQOP:28
.= (((1 - u) * (1 - t)) * x1) + (((u * (1 - s)) * x1) + ((((1 - u) * t) * x2) + ((u * s) * x2))) by Lm2
.= ((((1 - u) * (1 - t)) * x1) + ((u * (1 - s)) * x1)) + ((((1 - u) * t) * x2) + ((u * s) * x2)) by FINSEQOP:28
.= ((((1 - u) * (1 - t)) + (u * (1 - s))) * x1) + ((((1 - u) * t) * x2) + ((u * s) * x2)) by RVSUM_1:50
.= ((1 - (((1 * t) - (u * t)) + (u * s))) * x1) + ((((1 * t) - (u * t)) + (u * s)) * x2) by RVSUM_1:50 ;
hence  z in Line (x1,x2) ; ::_thesis: verum
end;
hence  Line (y1,y2) c= Line (x1,x2) by TARSKI:def_3; ::_thesis: verum
end;

theorem Th11: :: EUCLID_4:11
for n being Nat
for y1, x1, x2, y2 being Element of REAL n st y1 in Line (x1,x2) & y2 in Line (x1,x2) & y1 <> y2 holds
Line (x1,x2) c= Line (y1,y2)
proof
let n be Nat; ::_thesis: for y1, x1, x2, y2 being Element of REAL n st y1 in Line (x1,x2) & y2 in Line (x1,x2) & y1 <> y2 holds
Line (x1,x2) c= Line (y1,y2)
let y1, x1, x2, y2 be Element of REAL n; ::_thesis: ( y1 in Line (x1,x2) & y2 in Line (x1,x2) & y1 <> y2 implies Line (x1,x2) c= Line (y1,y2) )
assume  y1 in Line (x1,x2) ; ::_thesis: ( not y2 in Line (x1,x2) or not y1 <> y2 or Line (x1,x2) c= Line (y1,y2) )
then consider t being Real such that
A1: y1 = ((1 - t) * x1) + (t * x2) ;
assume  y2 in Line (x1,x2) ; ::_thesis: ( not y1 <> y2 or Line (x1,x2) c= Line (y1,y2) )
then consider s being Real such that
A2: y2 = ((1 - s) * x1) + (s * x2) ;
assume  y1 <> y2 ; ::_thesis: Line (x1,x2) c= Line (y1,y2)
then A3: t - s <> 0 by A1, A2;
then ((1 - ((t - 1) / (t - s))) * y1) + (((t - 1) / (t - s)) * y2) = ((((1 * (t - s)) - (t - 1)) / (t - s)) * y1) + (((t - 1) / (t - s)) * y2) by XCMPLX_1:127
.= (((((- s) + 1) / (t - s)) * ((1 - t) * x1)) + ((((- s) + 1) / (t - s)) * (t * x2))) + (((t - 1) / (t - s)) * (((1 - s) * x1) + (s * x2))) by A1, A2, RVSUM_1:51
.= (((((- s) + 1) / (t - s)) * ((1 - t) * x1)) + ((((- s) + 1) / (t - s)) * (t * x2))) + ((((t - 1) / (t - s)) * ((1 - s) * x1)) + (((t - 1) / (t - s)) * (s * x2))) by RVSUM_1:51
.= ((((((- s) + 1) / (t - s)) * (1 - t)) * x1) + ((((- s) + 1) / (t - s)) * (t * x2))) + ((((t - 1) / (t - s)) * ((1 - s) * x1)) + (((t - 1) / (t - s)) * (s * x2))) by RVSUM_1:49
.= ((((((- s) + 1) / (t - s)) * (1 - t)) * x1) + (((((- s) + 1) / (t - s)) * t) * x2)) + ((((t - 1) / (t - s)) * ((1 - s) * x1)) + (((t - 1) / (t - s)) * (s * x2))) by RVSUM_1:49
.= ((((((- s) + 1) / (t - s)) * (1 - t)) * x1) + (((((- s) + 1) / (t - s)) * t) * x2)) + (((((t - 1) / (t - s)) * (1 - s)) * x1) + (((t - 1) / (t - s)) * (s * x2))) by RVSUM_1:49
.= ((((((- s) + 1) / (t - s)) * (1 - t)) * x1) + (((((- s) + 1) / (t - s)) * t) * x2)) + (((((t - 1) / (t - s)) * (1 - s)) * x1) + ((((t - 1) / (t - s)) * s) * x2)) by RVSUM_1:49
.= ((((((- s) + 1) * (1 / (t - s))) * (1 - t)) * x1) + (((((- s) + 1) / (t - s)) * t) * x2)) + (((((t - 1) / (t - s)) * (1 - s)) * x1) + ((((t - 1) / (t - s)) * s) * x2)) by XCMPLX_1:99
.= ((((((- s) + 1) * (1 - t)) * (1 / (t - s))) * x1) + (((((- s) + 1) / (t - s)) * t) * x2)) + (((((t - 1) / (t - s)) * (1 - s)) * x1) + ((((t - 1) / (t - s)) * s) * x2))
.= ((((((- s) + 1) * (1 - t)) / (t - s)) * x1) + (((((- s) + 1) / (t - s)) * t) * x2)) + (((((t - 1) / (t - s)) * (1 - s)) * x1) + ((((t - 1) / (t - s)) * s) * x2)) by XCMPLX_1:99
.= ((((((- s) + 1) * (1 - t)) / (t - s)) * x1) + (((((- s) + 1) * (1 / (t - s))) * t) * x2)) + (((((t - 1) / (t - s)) * (1 - s)) * x1) + ((((t - 1) / (t - s)) * s) * x2)) by XCMPLX_1:99
.= ((((((- s) + 1) * (1 - t)) / (t - s)) * x1) + (((((- s) + 1) * t) * (1 / (t - s))) * x2)) + (((((t - 1) / (t - s)) * (1 - s)) * x1) + ((((t - 1) / (t - s)) * s) * x2))
.= ((((((- s) + 1) * (1 - t)) / (t - s)) * x1) + (((((- s) + 1) * t) / (t - s)) * x2)) + (((((t - 1) / (t - s)) * (1 - s)) * x1) + ((((t - 1) / (t - s)) * s) * x2)) by XCMPLX_1:99
.= ((((((- s) + 1) * (1 - t)) / (t - s)) * x1) + (((((- s) + 1) * t) / (t - s)) * x2)) + (((((t - 1) * (1 / (t - s))) * (1 - s)) * x1) + ((((t - 1) / (t - s)) * s) * x2)) by XCMPLX_1:99
.= ((((((- s) + 1) * (1 - t)) / (t - s)) * x1) + (((((- s) + 1) * t) / (t - s)) * x2)) + (((((t - 1) * (1 - s)) * (1 / (t - s))) * x1) + ((((t - 1) / (t - s)) * s) * x2))
.= ((((((- s) + 1) * (1 - t)) / (t - s)) * x1) + (((((- s) + 1) * t) / (t - s)) * x2)) + (((((t - 1) * (1 - s)) / (t - s)) * x1) + ((((t - 1) / (t - s)) * s) * x2)) by XCMPLX_1:99
.= ((((((- s) + 1) * (1 - t)) / (t - s)) * x1) + (((((- s) + 1) * t) / (t - s)) * x2)) + (((((t - 1) * (1 - s)) / (t - s)) * x1) + ((((t - 1) * (1 / (t - s))) * s) * x2)) by XCMPLX_1:99
.= ((((((- s) + 1) * (1 - t)) / (t - s)) * x1) + (((((- s) + 1) * t) / (t - s)) * x2)) + (((((t - 1) * (1 - s)) / (t - s)) * x1) + ((((t - 1) * s) * (1 / (t - s))) * x2))
.= ((((((- s) + 1) * (1 - t)) / (t - s)) * x1) + (((((- s) + 1) * t) / (t - s)) * x2)) + (((((t - 1) * (1 - s)) / (t - s)) * x1) + ((((t - 1) * s) / (t - s)) * x2)) by XCMPLX_1:99
.= (((((- s) + 1) * (1 - t)) / (t - s)) * x1) + ((((((- s) + 1) * t) / (t - s)) * x2) + (((((t - 1) * (1 - s)) / (t - s)) * x1) + ((((t - 1) * s) / (t - s)) * x2))) by FINSEQOP:28
.= (((((- s) + 1) * (1 - t)) / (t - s)) * x1) + (((((t - 1) * (1 - s)) / (t - s)) * x1) + ((((((- s) + 1) * t) / (t - s)) * x2) + ((((t - 1) * s) / (t - s)) * x2))) by Lm2
.= ((((((- s) + 1) * (1 - t)) / (t - s)) * x1) + ((((t - 1) * (1 - s)) / (t - s)) * x1)) + ((((((- s) + 1) * t) / (t - s)) * x2) + ((((t - 1) * s) / (t - s)) * x2)) by FINSEQOP:28
.= ((((((- s) + 1) * (1 - t)) / (t - s)) + (((t - 1) * (1 - s)) / (t - s))) * x1) + ((((((- s) + 1) * t) / (t - s)) * x2) + ((((t - 1) * s) / (t - s)) * x2)) by RVSUM_1:50
.= ((((((- s) + 1) * (1 - t)) / (t - s)) + (((t - 1) * (1 - s)) / (t - s))) * x1) + ((((((- s) + 1) * t) / (t - s)) + (((t - 1) * s) / (t - s))) * x2) by RVSUM_1:50
.= ((((((- s) + 1) * (1 - t)) + ((t - 1) * (1 - s))) / (t - s)) * x1) + ((((((- s) + 1) * t) / (t - s)) + (((t - 1) * s) / (t - s))) * x2) by XCMPLX_1:62
.= (((((1 - t) * (1 - s)) + (- ((1 - t) * (1 - s)))) / (t - s)) * x1) + ((((((- s) + 1) * t) + ((t - 1) * s)) / (t - s)) * x2) by XCMPLX_1:62
.= (0* n) + ((((((- s) + 1) * t) + ((t - 1) * s)) / (t - s)) * x2) by Th3
.= ((1 * (t - s)) / (t - s)) * x2 by Th1
.= 1 * x2 by A3, XCMPLX_1:89
.= x2 by Th3 ;
then A4: x2 in Line (y1,y2) ;
((1 - (t / (t - s))) * y1) + ((t / (t - s)) * y2) = ((((1 * (t - s)) - t) / (t - s)) * y1) + ((t / (t - s)) * y2) by A3, XCMPLX_1:127
.= ((((- s) / (t - s)) * ((1 - t) * x1)) + (((- s) / (t - s)) * (t * x2))) + ((t / (t - s)) * (((1 - s) * x1) + (s * x2))) by A1, A2, RVSUM_1:51
.= ((((- s) / (t - s)) * ((1 - t) * x1)) + (((- s) / (t - s)) * (t * x2))) + (((t / (t - s)) * ((1 - s) * x1)) + ((t / (t - s)) * (s * x2))) by RVSUM_1:51
.= (((((- s) / (t - s)) * (1 - t)) * x1) + (((- s) / (t - s)) * (t * x2))) + (((t / (t - s)) * ((1 - s) * x1)) + ((t / (t - s)) * (s * x2))) by RVSUM_1:49
.= (((((- s) / (t - s)) * (1 - t)) * x1) + ((((- s) / (t - s)) * t) * x2)) + (((t / (t - s)) * ((1 - s) * x1)) + ((t / (t - s)) * (s * x2))) by RVSUM_1:49
.= (((((- s) / (t - s)) * (1 - t)) * x1) + ((((- s) / (t - s)) * t) * x2)) + ((((t / (t - s)) * (1 - s)) * x1) + ((t / (t - s)) * (s * x2))) by RVSUM_1:49
.= (((((- s) / (t - s)) * (1 - t)) * x1) + ((((- s) / (t - s)) * t) * x2)) + ((((t / (t - s)) * (1 - s)) * x1) + (((t / (t - s)) * s) * x2)) by RVSUM_1:49
.= (((((- s) * (1 / (t - s))) * (1 - t)) * x1) + ((((- s) / (t - s)) * t) * x2)) + ((((t / (t - s)) * (1 - s)) * x1) + (((t / (t - s)) * s) * x2)) by XCMPLX_1:99
.= (((((- s) * (1 - t)) * (1 / (t - s))) * x1) + ((((- s) / (t - s)) * t) * x2)) + ((((t / (t - s)) * (1 - s)) * x1) + (((t / (t - s)) * s) * x2))
.= (((((- s) * (1 - t)) / (t - s)) * x1) + ((((- s) / (t - s)) * t) * x2)) + ((((t / (t - s)) * (1 - s)) * x1) + (((t / (t - s)) * s) * x2)) by XCMPLX_1:99
.= (((((- s) * (1 - t)) / (t - s)) * x1) + ((((- s) * (1 / (t - s))) * t) * x2)) + ((((t / (t - s)) * (1 - s)) * x1) + (((t / (t - s)) * s) * x2)) by XCMPLX_1:99
.= (((((- s) * (1 - t)) / (t - s)) * x1) + ((((- s) * t) * (1 / (t - s))) * x2)) + ((((t / (t - s)) * (1 - s)) * x1) + (((t / (t - s)) * s) * x2))
.= (((((- s) * (1 - t)) / (t - s)) * x1) + ((((- s) * t) / (t - s)) * x2)) + ((((t / (t - s)) * (1 - s)) * x1) + (((t / (t - s)) * s) * x2)) by XCMPLX_1:99
.= (((((- s) * (1 - t)) / (t - s)) * x1) + ((((- s) * t) / (t - s)) * x2)) + ((((t * (1 / (t - s))) * (1 - s)) * x1) + (((t / (t - s)) * s) * x2)) by XCMPLX_1:99
.= (((((- s) * (1 - t)) / (t - s)) * x1) + ((((- s) * t) / (t - s)) * x2)) + ((((t * (1 - s)) * (1 / (t - s))) * x1) + (((t / (t - s)) * s) * x2))
.= (((((- s) * (1 - t)) / (t - s)) * x1) + ((((- s) * t) / (t - s)) * x2)) + ((((t * (1 - s)) / (t - s)) * x1) + (((t / (t - s)) * s) * x2)) by XCMPLX_1:99
.= (((((- s) * (1 - t)) / (t - s)) * x1) + ((((- s) * t) / (t - s)) * x2)) + ((((t * (1 - s)) / (t - s)) * x1) + (((t * (1 / (t - s))) * s) * x2)) by XCMPLX_1:99
.= (((((- s) * (1 - t)) / (t - s)) * x1) + ((((- s) * t) / (t - s)) * x2)) + ((((t * (1 - s)) / (t - s)) * x1) + (((t * s) * (1 / (t - s))) * x2))
.= (((((- s) * (1 - t)) / (t - s)) * x1) + ((((- s) * t) / (t - s)) * x2)) + ((((t * (1 - s)) / (t - s)) * x1) + (((t * s) / (t - s)) * x2)) by XCMPLX_1:99
.= ((((- s) * (1 - t)) / (t - s)) * x1) + (((((- s) * t) / (t - s)) * x2) + ((((t * (1 - s)) / (t - s)) * x1) + (((t * s) / (t - s)) * x2))) by FINSEQOP:28
.= ((((- s) * (1 - t)) / (t - s)) * x1) + ((((t * (1 - s)) / (t - s)) * x1) + (((((- s) * t) / (t - s)) * x2) + (((t * s) / (t - s)) * x2))) by Lm2
.= (((((- s) * (1 - t)) / (t - s)) * x1) + (((t * (1 - s)) / (t - s)) * x1)) + (((((- s) * t) / (t - s)) * x2) + (((t * s) / (t - s)) * x2)) by FINSEQOP:28
.= (((((- s) * (1 - t)) / (t - s)) + ((t * (1 - s)) / (t - s))) * x1) + (((((- s) * t) / (t - s)) * x2) + (((t * s) / (t - s)) * x2)) by RVSUM_1:50
.= (((((- s) * (1 - t)) / (t - s)) + ((t * (1 - s)) / (t - s))) * x1) + (((((- s) * t) / (t - s)) + ((t * s) / (t - s))) * x2) by RVSUM_1:50
.= (((((- s) * (1 - t)) + (t * (1 - s))) / (t - s)) * x1) + (((((- s) * t) / (t - s)) + ((t * s) / (t - s))) * x2) by XCMPLX_1:62
.= (((((- s) * (1 - t)) + (t * (1 - s))) / (t - s)) * x1) + (((((- s) * t) + (t * s)) / (t - s)) * x2) by XCMPLX_1:62
.= (((((- s) * (1 - t)) + (t * (1 - s))) / (t - s)) * x1) + (0* n) by Th3
.= ((1 * (t - s)) / (t - s)) * x1 by Th1
.= 1 * x1 by A3, XCMPLX_1:89
.= x1 by Th3 ;
then  x1 in Line (y1,y2) ;
hence  Line (x1,x2) c= Line (y1,y2) by A4, Th10; ::_thesis: verum
end;

definition
let n be Nat;
let A be Subset of (REAL n);
attrA is being_line  means :Def2: :: EUCLID_4:def 2
 ex x1, x2 being Element of REAL n st
( x1 <> x2 & A = Line (x1,x2) );
end;

:: deftheorem Def2 defines being_line EUCLID_4:def_2_:_
 for n being Nat
for A being Subset of (REAL n) holds
( A is being_line iff ex x1, x2 being Element of REAL n st
( x1 <> x2 & A = Line (x1,x2) ) );

Lm3:  for n being Nat
for A being Subset of (REAL n)
for x1, x2 being Element of REAL n st A is being_line & x1 in A & x2 in A & x1 <> x2 holds
A = Line (x1,x2)
proof
let n be Nat; ::_thesis: for A being Subset of (REAL n)
for x1, x2 being Element of REAL n st A is being_line & x1 in A & x2 in A & x1 <> x2 holds
A = Line (x1,x2)
let A be Subset of (REAL n); ::_thesis: for x1, x2 being Element of REAL n st A is being_line & x1 in A & x2 in A & x1 <> x2 holds
A = Line (x1,x2)
let x1, x2 be Element of REAL n; ::_thesis: ( A is being_line & x1 in A & x2 in A & x1 <> x2 implies A = Line (x1,x2) )
assume that
A1: A is being_line and
A2: ( x1 in A & x2 in A & x1 <> x2 ) ; ::_thesis: A = Line (x1,x2)
 ex y1, y2 being Element of REAL n st
( y1 <> y2 & A = Line (y1,y2) ) by A1, Def2;
then  ( Line (x1,x2) c= A & A c= Line (x1,x2) ) by A2, Th10, Th11;
hence  A = Line (x1,x2) by XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: EUCLID_4:12
for n being Nat
for A, C being Subset of (REAL n)
for x1, x2 being Element of REAL n st A is being_line & C is being_line & x1 in A & x2 in A & x1 in C & x2 in C & not x1 = x2 holds
A = C
proof
let n be Nat; ::_thesis: for A, C being Subset of (REAL n)
for x1, x2 being Element of REAL n st A is being_line & C is being_line & x1 in A & x2 in A & x1 in C & x2 in C & not x1 = x2 holds
A = C
let A, C be Subset of (REAL n); ::_thesis: for x1, x2 being Element of REAL n st A is being_line & C is being_line & x1 in A & x2 in A & x1 in C & x2 in C & not x1 = x2 holds
A = C
let x1, x2 be Element of REAL n; ::_thesis: ( A is being_line & C is being_line & x1 in A & x2 in A & x1 in C & x2 in C & not x1 = x2 implies A = C )
assume that
A1: A is being_line and
A2: C is being_line and
A3: ( x1 in A & x2 in A ) and
A4: ( x1 in C & x2 in C ) ; ::_thesis: ( x1 = x2 or A = C )
assume A5: x1 <> x2 ; ::_thesis: A = C
then  A = Line (x1,x2) by A1, A3, Lm3;
hence  A = C by A2, A4, A5, Lm3; ::_thesis: verum
end;

theorem Th13: :: EUCLID_4:13
for n being Nat
for A being Subset of (REAL n) st A is being_line holds
ex x1, x2 being Element of REAL n st
( x1 in A & x2 in A & x1 <> x2 )
proof
let n be Nat; ::_thesis: for A being Subset of (REAL n) st A is being_line holds
ex x1, x2 being Element of REAL n st
( x1 in A & x2 in A & x1 <> x2 )
let A be Subset of (REAL n); ::_thesis: ( A is being_line implies ex x1, x2 being Element of REAL n st
( x1 in A & x2 in A & x1 <> x2 ) )
assume  A is being_line ; ::_thesis: ex x1, x2 being Element of REAL n st
( x1 in A & x2 in A & x1 <> x2 )
then consider x1, x2 being Element of REAL n such that
A1: x1 <> x2 and
A2: A = Line (x1,x2) by Def2;
 ( x1 in A & x2 in A ) by A2, Th9;
hence  ex x1, x2 being Element of REAL n st
( x1 in A & x2 in A & x1 <> x2 ) by A1; ::_thesis: verum
end;

theorem :: EUCLID_4:14
for n being Nat
for x1 being Element of REAL n
for A being Subset of (REAL n) st A is being_line holds
ex x2 being Element of REAL n st
( x1 <> x2 & x2 in A )
proof
let n be Nat; ::_thesis: for x1 being Element of REAL n
for A being Subset of (REAL n) st A is being_line holds
ex x2 being Element of REAL n st
( x1 <> x2 & x2 in A )
let x1 be Element of REAL n; ::_thesis: for A being Subset of (REAL n) st A is being_line holds
ex x2 being Element of REAL n st
( x1 <> x2 & x2 in A )
let A be Subset of (REAL n); ::_thesis: ( A is being_line implies ex x2 being Element of REAL n st
( x1 <> x2 & x2 in A ) )
assume  A is being_line ; ::_thesis: ex x2 being Element of REAL n st
( x1 <> x2 & x2 in A )
then consider y1, y2 being Element of REAL n such that
A1: y1 in A and
A2: ( y2 in A & y1 <> y2 ) by Th13;
 ( x1 = y1 implies ( x1 <> y2 & y2 in A ) ) by A2;
hence  ex x2 being Element of REAL n st
( x1 <> x2 & x2 in A ) by A1; ::_thesis: verum
end;

theorem :: EUCLID_4:15
for n being Nat
for x being Element of REAL n holds |.x.| = sqrt |(x,x)| ;

theorem Th16: :: EUCLID_4:16
for n being Nat
for x being Element of REAL n holds
( |(x,x)| = 0 iff |.x.| = 0 )
proof
let n be Nat; ::_thesis: for x being Element of REAL n holds
( |(x,x)| = 0 iff |.x.| = 0 )
let x be Element of REAL n; ::_thesis: ( |(x,x)| = 0 iff |.x.| = 0 )
thus  ( |(x,x)| = 0 implies |.x.| = 0 ) ::_thesis: ( |.x.| = 0 implies |(x,x)| = 0 )
proof
assume  |(x,x)| = 0 ; ::_thesis: |.x.| = 0
then  |.x.| ^2 = 0 by EUCLID_2:4;
hence  |.x.| = 0 by XCMPLX_1:6; ::_thesis: verum
end;
 ( |.x.| = 0 implies |(x,x)| = 0 ^2 ) by EUCLID_2:4;
hence  ( |.x.| = 0 implies |(x,x)| = 0 ) ; ::_thesis: verum
end;

theorem Th17: :: EUCLID_4:17
for n being Nat
for x being Element of REAL n holds
( |(x,x)| = 0 iff x = 0* n )
proof
let n be Nat; ::_thesis: for x being Element of REAL n holds
( |(x,x)| = 0 iff x = 0* n )
let x be Element of REAL n; ::_thesis: ( |(x,x)| = 0 iff x = 0* n )
thus  ( |(x,x)| = 0 implies x = 0* n ) ::_thesis: ( x = 0* n implies |(x,x)| = 0 )
proof
assume  |(x,x)| = 0 ; ::_thesis: x = 0* n
then  |.x.| = 0 by Th16;
hence  x = 0* n by EUCLID:8; ::_thesis: verum
end;
thus  ( x = 0* n implies |(x,x)| = 0 ) ::_thesis: verum
proof
assume  x = 0* n ; ::_thesis: |(x,x)| = 0
then |(x,x)| = (1 / 4) * ((|.((0* n) + (0* n)).| ^2) - (|.((0* n) - (0* n)).| ^2)) by EUCLID_2:3
.= (1 / 4) * ((|.(0* n).| ^2) - (|.((0* n) - (0* n)).| ^2)) by Th1
.= (1 / 4) * 0 by RVSUM_1:32 ;
hence  |(x,x)| = 0 ; ::_thesis: verum
end;
end;

theorem Th18: :: EUCLID_4:18
for n being Nat
for x being Element of REAL n holds |(x,(0* n))| = 0
proof
let n be Nat; ::_thesis: for x being Element of REAL n holds |(x,(0* n))| = 0
let x be Element of REAL n; ::_thesis: |(x,(0* n))| = 0
|(x,(0* n))| = (1 / 4) * ((|.(x + (0* n)).| ^2) - (|.(x - (0* n)).| ^2)) by EUCLID_2:3
.= (1 / 4) * ((|.x.| ^2) - (|.(x - (0* n)).| ^2)) by Th1
.= (1 / 4) * ((|.x.| ^2) - (|.x.| ^2)) by RVSUM_1:32
.= (1 / 4) * 0 ;
hence  |(x,(0* n))| = 0 ; ::_thesis: verum
end;

theorem :: EUCLID_4:19
for n being Nat
for x being Element of REAL n holds |((0* n),x)| = 0 by Th18;

theorem Th20: :: EUCLID_4:20
for n being Nat
for x1, x2, x3 being Element of REAL n holds |((x1 + x2),x3)| = |(x1,x3)| + |(x2,x3)|
proof
let n be Nat; ::_thesis: for x1, x2, x3 being Element of REAL n holds |((x1 + x2),x3)| = |(x1,x3)| + |(x2,x3)|
let x1, x2, x3 be Element of REAL n; ::_thesis: |((x1 + x2),x3)| = |(x1,x3)| + |(x2,x3)|
A1: len x3 = n by CARD_1:def_7;
 ( len x1 = n & len x2 = n ) by CARD_1:def_7;
hence  |((x1 + x2),x3)| = |(x1,x3)| + |(x2,x3)| by A1, RVSUM_1:120; ::_thesis: verum
end;

theorem Th21: :: EUCLID_4:21
for n being Nat
for x1, x2 being Element of REAL n
for a being real number holds |((a * x1),x2)| = a * |(x1,x2)|
proof
let n be Nat; ::_thesis: for x1, x2 being Element of REAL n
for a being real number holds |((a * x1),x2)| = a * |(x1,x2)|
let x1, x2 be Element of REAL n; ::_thesis: for a being real number holds |((a * x1),x2)| = a * |(x1,x2)|
let a be real number ; ::_thesis: |((a * x1),x2)| = a * |(x1,x2)|
 ( len x1 = n & len x2 = n ) by CARD_1:def_7;
hence  |((a * x1),x2)| = a * |(x1,x2)| by RVSUM_1:121; ::_thesis: verum
end;

theorem :: EUCLID_4:22
for n being Nat
for x1, x2 being Element of REAL n
for a being real number holds |(x1,(a * x2))| = a * |(x1,x2)| by Th21;

theorem Th23: :: EUCLID_4:23
for n being Nat
for x1, x2 being Element of REAL n holds |((- x1),x2)| = - |(x1,x2)|
proof
let n be Nat; ::_thesis: for x1, x2 being Element of REAL n holds |((- x1),x2)| = - |(x1,x2)|
let x1, x2 be Element of REAL n; ::_thesis: |((- x1),x2)| = - |(x1,x2)|
 ( len x1 = n & len x2 = n ) by CARD_1:def_7;
hence  |((- x1),x2)| = - |(x1,x2)| by RVSUM_1:122; ::_thesis: verum
end;

theorem :: EUCLID_4:24
for n being Nat
for x1, x2 being Element of REAL n holds |(x1,(- x2))| = - |(x1,x2)| by Th23;

theorem :: EUCLID_4:25
for n being Nat
for x1, x2 being Element of REAL n holds |((- x1),(- x2))| = |(x1,x2)|
proof
let n be Nat; ::_thesis: for x1, x2 being Element of REAL n holds |((- x1),(- x2))| = |(x1,x2)|
let x1, x2 be Element of REAL n; ::_thesis: |((- x1),(- x2))| = |(x1,x2)|
thus |((- x1),(- x2))| = - |(x1,(- x2))| by Th23
.= (- 1) * |(x1,(- x2))|
.= (- 1) * (- |(x1,x2)|) by Th23
.= |(x1,x2)| ; ::_thesis: verum
end;

theorem Th26: :: EUCLID_4:26
for n being Nat
for x1, x2, x3 being Element of REAL n holds |((x1 - x2),x3)| = |(x1,x3)| - |(x2,x3)|
proof
let n be Nat; ::_thesis: for x1, x2, x3 being Element of REAL n holds |((x1 - x2),x3)| = |(x1,x3)| - |(x2,x3)|
let x1, x2, x3 be Element of REAL n; ::_thesis: |((x1 - x2),x3)| = |(x1,x3)| - |(x2,x3)|
A1: len x3 = n by CARD_1:def_7;
 ( len x1 = n & len x2 = n ) by CARD_1:def_7;
hence  |((x1 - x2),x3)| = |(x1,x3)| - |(x2,x3)| by A1, RVSUM_1:124; ::_thesis: verum
end;

theorem :: EUCLID_4:27
for n being Nat
for a, b being real number
for x1, x2, x3 being Element of REAL n holds |(((a * x1) + (b * x2)),x3)| = (a * |(x1,x3)|) + (b * |(x2,x3)|)
proof
let n be Nat; ::_thesis: for a, b being real number
for x1, x2, x3 being Element of REAL n holds |(((a * x1) + (b * x2)),x3)| = (a * |(x1,x3)|) + (b * |(x2,x3)|)
let a, b be real number ; ::_thesis: for x1, x2, x3 being Element of REAL n holds |(((a * x1) + (b * x2)),x3)| = (a * |(x1,x3)|) + (b * |(x2,x3)|)
let x1, x2, x3 be Element of REAL n; ::_thesis: |(((a * x1) + (b * x2)),x3)| = (a * |(x1,x3)|) + (b * |(x2,x3)|)
thus |(((a * x1) + (b * x2)),x3)| = |((a * x1),x3)| + |((b * x2),x3)| by Th20
.= (a * |(x1,x3)|) + |((b * x2),x3)| by Th21
.= (a * |(x1,x3)|) + (b * |(x2,x3)|) by Th21 ; ::_thesis: verum
end;

theorem :: EUCLID_4:28
for n being Nat
for x1, y1, y2 being Element of REAL n holds |(x1,(y1 + y2))| = |(x1,y1)| + |(x1,y2)| by Th20;

theorem :: EUCLID_4:29
for n being Nat
for x1, y1, y2 being Element of REAL n holds |(x1,(y1 - y2))| = |(x1,y1)| - |(x1,y2)| by Th26;

theorem Th30: :: EUCLID_4:30
for n being Nat
for x1, x2, y1, y2 being Element of REAL n holds |((x1 + x2),(y1 + y2))| = ((|(x1,y1)| + |(x1,y2)|) + |(x2,y1)|) + |(x2,y2)|
proof
let n be Nat; ::_thesis: for x1, x2, y1, y2 being Element of REAL n holds |((x1 + x2),(y1 + y2))| = ((|(x1,y1)| + |(x1,y2)|) + |(x2,y1)|) + |(x2,y2)|
let x1, x2, y1, y2 be Element of REAL n; ::_thesis: |((x1 + x2),(y1 + y2))| = ((|(x1,y1)| + |(x1,y2)|) + |(x2,y1)|) + |(x2,y2)|
thus |((x1 + x2),(y1 + y2))| = |(x1,(y1 + y2))| + |(x2,(y1 + y2))| by Th20
.= (|(x1,y1)| + |(x1,y2)|) + |(x2,(y1 + y2))| by Th20
.= (|(x1,y1)| + |(x1,y2)|) + (|(x2,y1)| + |(x2,y2)|) by Th20
.= ((|(x1,y1)| + |(x1,y2)|) + |(x2,y1)|) + |(x2,y2)| ; ::_thesis: verum
end;

theorem Th31: :: EUCLID_4:31
for n being Nat
for x1, x2, y1, y2 being Element of REAL n holds |((x1 - x2),(y1 - y2))| = ((|(x1,y1)| - |(x1,y2)|) - |(x2,y1)|) + |(x2,y2)|
proof
let n be Nat; ::_thesis: for x1, x2, y1, y2 being Element of REAL n holds |((x1 - x2),(y1 - y2))| = ((|(x1,y1)| - |(x1,y2)|) - |(x2,y1)|) + |(x2,y2)|
let x1, x2, y1, y2 be Element of REAL n; ::_thesis: |((x1 - x2),(y1 - y2))| = ((|(x1,y1)| - |(x1,y2)|) - |(x2,y1)|) + |(x2,y2)|
thus |((x1 - x2),(y1 - y2))| = |(x1,(y1 - y2))| - |(x2,(y1 - y2))| by Th26
.= (|(x1,y1)| - |(x1,y2)|) - |(x2,(y1 - y2))| by Th26
.= (|(x1,y1)| - |(x1,y2)|) - (|(x2,y1)| - |(x2,y2)|) by Th26
.= ((|(x1,y1)| - |(x1,y2)|) - |(x2,y1)|) + |(x2,y2)| ; ::_thesis: verum
end;

theorem Th32: :: EUCLID_4:32
for n being Nat
for x, y being Element of REAL n holds |((x + y),(x + y))| = (|(x,x)| + (2 * |(x,y)|)) + |(y,y)|
proof
let n be Nat; ::_thesis: for x, y being Element of REAL n holds |((x + y),(x + y))| = (|(x,x)| + (2 * |(x,y)|)) + |(y,y)|
let x, y be Element of REAL n; ::_thesis: |((x + y),(x + y))| = (|(x,x)| + (2 * |(x,y)|)) + |(y,y)|
thus |((x + y),(x + y))| = ((|(x,x)| + |(x,y)|) + |(y,x)|) + |(y,y)| by Th30
.= (|(x,x)| + (2 * |(x,y)|)) + |(y,y)| ; ::_thesis: verum
end;

theorem Th33: :: EUCLID_4:33
for n being Nat
for x, y being Element of REAL n holds |((x - y),(x - y))| = (|(x,x)| - (2 * |(x,y)|)) + |(y,y)|
proof
let n be Nat; ::_thesis: for x, y being Element of REAL n holds |((x - y),(x - y))| = (|(x,x)| - (2 * |(x,y)|)) + |(y,y)|
let x, y be Element of REAL n; ::_thesis: |((x - y),(x - y))| = (|(x,x)| - (2 * |(x,y)|)) + |(y,y)|
thus |((x - y),(x - y))| = ((|(x,x)| - |(x,y)|) - |(y,x)|) + |(y,y)| by Th31
.= (|(x,x)| - (2 * |(x,y)|)) + |(y,y)| ; ::_thesis: verum
end;

theorem :: EUCLID_4:34
for n being Nat
for x, y being Element of REAL n holds |.(x + y).| ^2 = ((|.x.| ^2) + (2 * |(x,y)|)) + (|.y.| ^2)
proof
let n be Nat; ::_thesis: for x, y being Element of REAL n holds |.(x + y).| ^2 = ((|.x.| ^2) + (2 * |(x,y)|)) + (|.y.| ^2)
let x, y be Element of REAL n; ::_thesis: |.(x + y).| ^2 = ((|.x.| ^2) + (2 * |(x,y)|)) + (|.y.| ^2)
thus |.(x + y).| ^2 = |((x + y),(x + y))| by EUCLID_2:4
.= (|(x,x)| + (2 * |(x,y)|)) + |(y,y)| by Th32
.= ((|.x.| ^2) + (2 * |(x,y)|)) + |(y,y)| by EUCLID_2:4
.= ((|.x.| ^2) + (2 * |(x,y)|)) + (|.y.| ^2) by EUCLID_2:4 ; ::_thesis: verum
end;

theorem :: EUCLID_4:35
for n being Nat
for x, y being Element of REAL n holds |.(x - y).| ^2 = ((|.x.| ^2) - (2 * |(x,y)|)) + (|.y.| ^2)
proof
let n be Nat; ::_thesis: for x, y being Element of REAL n holds |.(x - y).| ^2 = ((|.x.| ^2) - (2 * |(x,y)|)) + (|.y.| ^2)
let x, y be Element of REAL n; ::_thesis: |.(x - y).| ^2 = ((|.x.| ^2) - (2 * |(x,y)|)) + (|.y.| ^2)
thus |.(x - y).| ^2 = |((x - y),(x - y))| by EUCLID_2:4
.= (|(x,x)| - (2 * |(x,y)|)) + |(y,y)| by Th33
.= ((|.x.| ^2) - (2 * |(x,y)|)) + |(y,y)| by EUCLID_2:4
.= ((|.x.| ^2) - (2 * |(x,y)|)) + (|.y.| ^2) by EUCLID_2:4 ; ::_thesis: verum
end;

theorem :: EUCLID_4:36
for n being Nat
for x, y being Element of REAL n holds (|.(x + y).| ^2) + (|.(x - y).| ^2) = 2 * ((|.x.| ^2) + (|.y.| ^2))
proof
let n be Nat; ::_thesis: for x, y being Element of REAL n holds (|.(x + y).| ^2) + (|.(x - y).| ^2) = 2 * ((|.x.| ^2) + (|.y.| ^2))
let x, y be Element of REAL n; ::_thesis: (|.(x + y).| ^2) + (|.(x - y).| ^2) = 2 * ((|.x.| ^2) + (|.y.| ^2))
 ( len x = n & len y = n ) by CARD_1:def_7;
hence  (|.(x + y).| ^2) + (|.(x - y).| ^2) = 2 * ((|.x.| ^2) + (|.y.| ^2)) by EUCLID_2:13; ::_thesis: verum
end;

theorem :: EUCLID_4:37
for n being Nat
for x, y being Element of REAL n holds (|.(x + y).| ^2) - (|.(x - y).| ^2) = 4 * |(x,y)|
proof
let n be Nat; ::_thesis: for x, y being Element of REAL n holds (|.(x + y).| ^2) - (|.(x - y).| ^2) = 4 * |(x,y)|
let x, y be Element of REAL n; ::_thesis: (|.(x + y).| ^2) - (|.(x - y).| ^2) = 4 * |(x,y)|
 ( len x = n & len y = n ) by CARD_1:def_7;
hence  (|.(x + y).| ^2) - (|.(x - y).| ^2) = 4 * |(x,y)| by EUCLID_2:14; ::_thesis: verum
end;

theorem :: EUCLID_4:38
for n being Nat
for x, y being Element of REAL n holds abs |(x,y)| <= |.x.| * |.y.|
proof
let n be Nat; ::_thesis: for x, y being Element of REAL n holds abs |(x,y)| <= |.x.| * |.y.|
let x, y be Element of REAL n; ::_thesis: abs |(x,y)| <= |.x.| * |.y.|
 ( len x = n & len y = n ) by CARD_1:def_7;
hence  abs |(x,y)| <= |.x.| * |.y.| by EUCLID_2:15; ::_thesis: verum
end;

theorem :: EUCLID_4:39
for n being Nat
for x, y being Element of REAL n holds |.(x + y).| <= |.x.| + |.y.|
proof
let n be Nat; ::_thesis: for x, y being Element of REAL n holds |.(x + y).| <= |.x.| + |.y.|
let x, y be Element of REAL n; ::_thesis: |.(x + y).| <= |.x.| + |.y.|
 ( len x = n & len y = n ) by CARD_1:def_7;
hence  |.(x + y).| <= |.x.| + |.y.| by EUCLID_2:16; ::_thesis: verum
end;

Lm4:  for a being Real
for n being Nat
for x being Element of REAL n holds
( - (a * x) = (- a) * x & - (a * x) = a * (- x) )
proof
let a be Real; ::_thesis: for n being Nat
for x being Element of REAL n holds
( - (a * x) = (- a) * x & - (a * x) = a * (- x) )
let n be Nat; ::_thesis: for x being Element of REAL n holds
( - (a * x) = (- a) * x & - (a * x) = a * (- x) )
let x be Element of REAL n; ::_thesis: ( - (a * x) = (- a) * x & - (a * x) = a * (- x) )
reconsider p = x as Point of (TOP-REAL n) by EUCLID:22;
reconsider x9 = p as Element of n -tuples_on REAL ;
thus  - (a * x) = ((- 1) * a) * x9 by RVSUM_1:49
.= (- a) * x ; ::_thesis: - (a * x) = a * (- x)
hence  - (a * x) = (a * (- 1)) * x
.= a * (- x) by RVSUM_1:49 ;
::_thesis: verum
end;

Lm5:  for n being Nat
for x1, x2 being Element of REAL n st x1 <> x2 holds
|.(x1 - x2).| <> 0
proof
let n be Nat; ::_thesis: for x1, x2 being Element of REAL n st x1 <> x2 holds
|.(x1 - x2).| <> 0
let x1, x2 be Element of REAL n; ::_thesis: ( x1 <> x2 implies |.(x1 - x2).| <> 0 )
now__::_thesis:_(_x1_<>_x2_implies_|.(x1_-_x2).|_<>_0_)
assume that
A1: x1 <> x2 and
A2: not |.(x1 - x2).| <> 0 ; ::_thesis: contradiction
 |((x1 - x2),(x1 - x2))| = 0 ^2 by A2, EUCLID_2:4;
then  x1 - x2 = 0* n by Th17;
then x1 = x1 - (x1 + (- x2)) by RVSUM_1:32
.= (x1 - x1) - (- x2) by RVSUM_1:39
.= (0* n) - (- x2) by RVSUM_1:37
.= x2 by RVSUM_1:33 ;
hence  contradiction by A1; ::_thesis: verum
end;
hence  ( x1 <> x2 implies |.(x1 - x2).| <> 0 ) ; ::_thesis: verum
end;

Lm6:  for n being Nat
for y1, y2, x1, x2 being Element of REAL n st y1 in Line (x1,x2) & y2 in Line (x1,x2) holds
ex a being Real st y1 - y2 = a * (x1 - x2)
proof
let n be Nat; ::_thesis: for y1, y2, x1, x2 being Element of REAL n st y1 in Line (x1,x2) & y2 in Line (x1,x2) holds
ex a being Real st y1 - y2 = a * (x1 - x2)
let y1, y2 be Element of REAL n; ::_thesis: for x1, x2 being Element of REAL n st y1 in Line (x1,x2) & y2 in Line (x1,x2) holds
ex a being Real st y1 - y2 = a * (x1 - x2)
let x1, x2 be Element of REAL n; ::_thesis: ( y1 in Line (x1,x2) & y2 in Line (x1,x2) implies ex a being Real st y1 - y2 = a * (x1 - x2) )
assume  y1 in Line (x1,x2) ; ::_thesis: ( not y2 in Line (x1,x2) or ex a being Real st y1 - y2 = a * (x1 - x2) )
then consider t being Real such that
A1: y1 = ((1 - t) * x1) + (t * x2) ;
assume  y2 in Line (x1,x2) ; ::_thesis: ex a being Real st y1 - y2 = a * (x1 - x2)
then consider s being Real such that
A2: y2 = ((1 - s) * x1) + (s * x2) ;
take  s - t ; ::_thesis: y1 - y2 = (s - t) * (x1 - x2)
y1 - y2 = ((((1 - t) * x1) + (t * x2)) - ((1 - s) * x1)) - (s * x2) by A1, A2, RVSUM_1:39
.= ((((1 - t) * x1) + (- ((1 - s) * x1))) + (t * x2)) + (- (s * x2)) by Lm2
.= (((1 - t) * x1) + (- ((1 - s) * x1))) + ((t * x2) + (- (s * x2))) by FINSEQOP:28
.= (((1 - t) * x1) + ((- (1 - s)) * x1)) + ((t * x2) + (- (s * x2))) by Lm4
.= (((1 - t) * x1) + ((- (1 - s)) * x1)) + ((t * x2) + ((- s) * x2)) by Lm4
.= (((1 - t) + (- (1 - s))) * x1) + ((t * x2) + ((- s) * x2)) by RVSUM_1:50
.= (((1 - t) - (1 - s)) * x1) + ((t + (- s)) * x2) by RVSUM_1:50
.= ((s - t) * x1) + ((- (s + (- t))) * x2)
.= ((s - t) * x1) + (- ((s - t) * x2)) by Lm4
.= ((s - t) * x1) + ((s - t) * (- x2)) by Lm4
.= (s - t) * (x1 - x2) by RVSUM_1:51 ;
hence  y1 - y2 = (s - t) * (x1 - x2) ; ::_thesis: verum
end;

Lm7:  for n being Nat
for x1, x2, y1 being Element of REAL n ex y2 being Element of REAL n st
( y2 in Line (x1,x2) & x1 - x2,y1 - y2 are_orthogonal & ( for x being Element of REAL n st x in Line (x1,x2) holds
|.(y1 - y2).| <= |.(y1 - x).| ) )
proof
let n be Nat; ::_thesis: for x1, x2, y1 being Element of REAL n ex y2 being Element of REAL n st
( y2 in Line (x1,x2) & x1 - x2,y1 - y2 are_orthogonal & ( for x being Element of REAL n st x in Line (x1,x2) holds
|.(y1 - y2).| <= |.(y1 - x).| ) )
let x1, x2, y1 be Element of REAL n; ::_thesis: ex y2 being Element of REAL n st
( y2 in Line (x1,x2) & x1 - x2,y1 - y2 are_orthogonal & ( for x being Element of REAL n st x in Line (x1,x2) holds
|.(y1 - y2).| <= |.(y1 - x).| ) )
now__::_thesis:_(_(_x1_<>_x2_&_((1_-_(-_(|((x1_-_x2),(y1_-_x1))|_/_(|.(x1_-_x2).|_^2))))_*_x1)_+_((-_(|((x1_-_x2),(y1_-_x1))|_/_(|.(x1_-_x2).|_^2)))_*_x2)_in_Line_(x1,x2)_&_x1_-_x2,y1_-_(((1_-_(-_(|((x1_-_x2),(y1_-_x1))|_/_(|.(x1_-_x2).|_^2))))_*_x1)_+_((-_(|((x1_-_x2),(y1_-_x1))|_/_(|.(x1_-_x2).|_^2)))_*_x2))_are_orthogonal_)_or_(_x1_=_x2_&_(_for_mu_being_Real_ex_y2_being_Element_of_REAL_n_st_
(_y2_in_Line_(x1,x2)_&_x1_-_x2,y1_-_y2_are_orthogonal_)_)_)_)
percases ( x1 <> x2 or x1 = x2 ) ;
caseA1: x1 <> x2 ; ::_thesis: ( ((1 - (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * x1) + ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2))) * x2) in Line (x1,x2) & x1 - x2,y1 - (((1 - (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * x1) + ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2))) * x2)) are_orthogonal )
set mu = - (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2));
set y2 = ((1 - (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * x1) + ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2))) * x2);
 |.(x1 - x2).| <> 0 by A1, Lm5;
then A2: |.(x1 - x2).| ^2 <> 0 by SQUARE_1:12;
|((x1 - x2),(y1 - (((1 - (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * x1) + ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2))) * x2))))| = |((x1 - x2),((y1 - ((1 + (- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2))))) * x1)) - ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2))) * x2)))| by RVSUM_1:39
.= |((x1 - x2),((y1 - ((1 * x1) + ((- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * x1))) - ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2))) * x2)))| by RVSUM_1:50
.= |((x1 - x2),(((y1 - (1 * x1)) - ((- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * x1)) - ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2))) * x2)))| by RVSUM_1:39
.= |((x1 - x2),(((y1 - x1) - ((- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * x1)) - ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2))) * x2)))| by Th3
.= |((x1 - x2),((y1 - x1) - (((- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * x1) + ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2))) * x2))))| by RVSUM_1:39
.= |((x1 - x2),((y1 - x1) - (((- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * x1) + (- ((- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * x2)))))| by Lm4
.= |((x1 - x2),((y1 - x1) - (((- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * x1) + ((- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * (- x2)))))| by Lm4
.= |((x1 - x2),((y1 - x1) - ((- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * (x1 - x2))))| by RVSUM_1:51
.= |((x1 - x2),(y1 - x1))| - |((x1 - x2),((- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * (x1 - x2)))| by Th26
.= |((x1 - x2),(y1 - x1))| - ((- (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * |((x1 - x2),(x1 - x2))|) by Th21
.= |((x1 - x2),(y1 - x1))| + ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2))) * |((x1 - x2),(x1 - x2))|)
.= |((x1 - x2),(y1 - x1))| + ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2))) * (|.(x1 - x2).| ^2)) by EUCLID_2:4
.= |((x1 - x2),(y1 - x1))| + (((- |((x1 - x2),(y1 - x1))|) / (|.(x1 - x2).| ^2)) * (|.(x1 - x2).| ^2)) by XCMPLX_1:187
.= |((x1 - x2),(y1 - x1))| + (- |((x1 - x2),(y1 - x1))|) by A2, XCMPLX_1:87
.= 0 ;
hence  ( ((1 - (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * x1) + ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2))) * x2) in Line (x1,x2) & x1 - x2,y1 - (((1 - (- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2)))) * x1) + ((- (|((x1 - x2),(y1 - x1))| / (|.(x1 - x2).| ^2))) * x2)) are_orthogonal ) by RVSUM_1:def_17; ::_thesis: verum
end;
caseA3: x1 = x2 ; ::_thesis: for mu being Real ex y2 being Element of REAL n st
( y2 in Line (x1,x2) & x1 - x2,y1 - y2 are_orthogonal )
let mu be Real; ::_thesis: ex y2 being Element of REAL n st
( y2 in Line (x1,x2) & x1 - x2,y1 - y2 are_orthogonal )
set y2 = ((1 - mu) * x1) + (mu * x2);
take y2 = ((1 - mu) * x1) + (mu * x2); ::_thesis: ( y2 in Line (x1,x2) & x1 - x2,y1 - y2 are_orthogonal )
 x1 - x2 = 0* n by A3, RVSUM_1:37;
then  |((x1 - x2),(y1 - y2))| = 0 by Th18;
hence  ( y2 in Line (x1,x2) & x1 - x2,y1 - y2 are_orthogonal ) by RVSUM_1:def_17; ::_thesis: verum
end;
end;
end;
then consider y2 being Element of REAL n such that
A4: y2 in Line (x1,x2) and
A5: x1 - x2,y1 - y2 are_orthogonal ;
A6: |((x1 - x2),(y1 - y2))| = 0 by A5, RVSUM_1:def_17;
 for x being Element of REAL n st x in Line (x1,x2) holds
|.(y1 - y2).| <= |.(y1 - x).|
proof
let x be Element of REAL n; ::_thesis: ( x in Line (x1,x2) implies |.(y1 - y2).| <= |.(y1 - x).| )
assume  x in Line (x1,x2) ; ::_thesis: |.(y1 - y2).| <= |.(y1 - x).|
then consider a being Real such that
A7: y2 - x = a * (x1 - x2) by A4, Lm6;
(y2 - x) + (y1 - y2) = (((- x) + y2) + (- y2)) + y1 by Lm2
.= ((- x) + (y2 - y2)) + y1 by FINSEQOP:28
.= ((- x) + (0* n)) + y1 by RVSUM_1:37
.= y1 - x by Th1 ;
then |.(y1 - x).| ^2 = |(((a * (x1 - x2)) + (y1 - y2)),((a * (x1 - x2)) + (y1 - y2)))| by A7, EUCLID_2:4
.= (|((a * (x1 - x2)),(a * (x1 - x2)))| + (2 * |((a * (x1 - x2)),(y1 - y2))|)) + |((y1 - y2),(y1 - y2))| by Th32
.= ((a * |((x1 - x2),(a * (x1 - x2)))|) + (2 * |((a * (x1 - x2)),(y1 - y2))|)) + |((y1 - y2),(y1 - y2))| by Th21
.= ((a * (a * |((x1 - x2),(x1 - x2))|)) + (2 * |((a * (x1 - x2)),(y1 - y2))|)) + |((y1 - y2),(y1 - y2))| by Th21
.= (((a ^2) * |((x1 - x2),(x1 - x2))|) + (2 * |((a * (x1 - x2)),(y1 - y2))|)) + |((y1 - y2),(y1 - y2))|
.= (((a ^2) * (|.(x1 - x2).| ^2)) + (2 * |((a * (x1 - x2)),(y1 - y2))|)) + |((y1 - y2),(y1 - y2))| by EUCLID_2:4
.= (((a ^2) * (|.(x1 - x2).| ^2)) + (2 * (a * |((x1 - x2),(y1 - y2))|))) + |((y1 - y2),(y1 - y2))| by Th21
.= ((a * |.(x1 - x2).|) ^2) + (|.(y1 - y2).| ^2) by A6, EUCLID_2:4 ;
then  0 <= (|.(y1 - x).| ^2) - (|.(y1 - y2).| ^2) by XREAL_1:63;
then A8: |.(y1 - y2).| ^2 <= |.(y1 - x).| ^2 by XREAL_1:49;
 0 <= |.(y1 - y2).| ^2 by XREAL_1:63;
then  sqrt (|.(y1 - y2).| ^2) <= sqrt (|.(y1 - x).| ^2) by A8, SQUARE_1:26;
then  |.(y1 - y2).| <= sqrt (|.(y1 - x).| ^2) by EUCLID_2:6, SQUARE_1:22;
hence  |.(y1 - y2).| <= |.(y1 - x).| by EUCLID_2:6, SQUARE_1:22; ::_thesis: verum
end;
hence  ex y2 being Element of REAL n st
( y2 in Line (x1,x2) & x1 - x2,y1 - y2 are_orthogonal & ( for x being Element of REAL n st x in Line (x1,x2) holds
|.(y1 - y2).| <= |.(y1 - x).| ) ) by A4, A5; ::_thesis: verum
end;

theorem :: EUCLID_4:40
for n being Nat
for R being Subset of REAL
for x1, x2, y1 being Element of REAL n st R =  {  |.(y1 - x).| where x is Element of REAL n : x in Line (x1,x2)  }  holds
ex y2 being Element of REAL n st
( y2 in Line (x1,x2) & |.(y1 - y2).| = lower_bound R & x1 - x2,y1 - y2 are_orthogonal )
proof
let n be Nat; ::_thesis: for R being Subset of REAL
for x1, x2, y1 being Element of REAL n st R =  {  |.(y1 - x).| where x is Element of REAL n : x in Line (x1,x2)  }  holds
ex y2 being Element of REAL n st
( y2 in Line (x1,x2) & |.(y1 - y2).| = lower_bound R & x1 - x2,y1 - y2 are_orthogonal )
let R be Subset of REAL; ::_thesis: for x1, x2, y1 being Element of REAL n st R =  {  |.(y1 - x).| where x is Element of REAL n : x in Line (x1,x2)  }  holds
ex y2 being Element of REAL n st
( y2 in Line (x1,x2) & |.(y1 - y2).| = lower_bound R & x1 - x2,y1 - y2 are_orthogonal )
let x1, x2, y1 be Element of REAL n; ::_thesis: ( R =  {  |.(y1 - x).| where x is Element of REAL n : x in Line (x1,x2)  }  implies ex y2 being Element of REAL n st
( y2 in Line (x1,x2) & |.(y1 - y2).| = lower_bound R & x1 - x2,y1 - y2 are_orthogonal ) )
consider y2 being Element of REAL n such that
A1: y2 in Line (x1,x2) and
A2: x1 - x2,y1 - y2 are_orthogonal and
A3: for x being Element of REAL n st x in Line (x1,x2) holds
|.(y1 - y2).| <= |.(y1 - x).| by Lm7;
assume A4: R =  {  |.(y1 - x).| where x is Element of REAL n : x in Line (x1,x2)  }  ; ::_thesis: ex y2 being Element of REAL n st
( y2 in Line (x1,x2) & |.(y1 - y2).| = lower_bound R & x1 - x2,y1 - y2 are_orthogonal )
A5: for s being real number st 0 < s holds
ex r being real number st
( r in R & r < |.(y1 - y2).| + s )
proof
let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st
( r in R & r < |.(y1 - y2).| + s ) )
assume A6: 0 < s ; ::_thesis: ex r being real number st
( r in R & r < |.(y1 - y2).| + s )
take  |.(y1 - y2).| ; ::_thesis: ( |.(y1 - y2).| in R & |.(y1 - y2).| < |.(y1 - y2).| + s )
thus  ( |.(y1 - y2).| in R & |.(y1 - y2).| < |.(y1 - y2).| + s ) by A4, A1, A6, XREAL_1:29; ::_thesis: verum
end;
 x1 in Line (x1,x2) by Th9;
then A7: |.(y1 - x1).| in R by A4;
A8: for r being real number st r in R holds
|.(y1 - y2).| <= r
proof
let r be real number ; ::_thesis: ( r in R implies |.(y1 - y2).| <= r )
assume  r in R ; ::_thesis: |.(y1 - y2).| <= r
then  ex x0 being Element of REAL n st
( r = |.(y1 - x0).| & x0 in Line (x1,x2) ) by A4;
hence  |.(y1 - y2).| <= r by A3; ::_thesis: verum
end;
 R is bounded_below
proof
take  |.(y1 - y2).| ; :: according to XXREAL_2:def_9 ::_thesis: |.(y1 - y2).| is LowerBound of R
let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in R or |.(y1 - y2).| <= r )
assume  r in R ; ::_thesis: |.(y1 - y2).| <= r
then  ex x0 being Element of REAL n st
( r = |.(y1 - x0).| & x0 in Line (x1,x2) ) by A4;
hence  |.(y1 - y2).| <= r by A3; ::_thesis: verum
end;
then  |.(y1 - y2).| = lower_bound R by A7, A5, A8, SEQ_4:def_2;
hence  ex y2 being Element of REAL n st
( y2 in Line (x1,x2) & |.(y1 - y2).| = lower_bound R & x1 - x2,y1 - y2 are_orthogonal ) by A1, A2; ::_thesis: verum
end;

definition
let n be Nat;
let p1, p2 be Point of (TOP-REAL n);
func Line (p1,p2) ->  Subset of (TOP-REAL n) equals :: EUCLID_4:def 3
 {  (((1 - lambda) * p1) + (lambda * p2)) where lambda is Real : verum  }  ;
coherence
  {  (((1 - lambda) * p1) + (lambda * p2)) where lambda is Real : verum  }  is Subset of (TOP-REAL n)
proof
set A =  {  (((1 - lambda) * p1) + (lambda * p2)) where lambda is Real : verum  }  ;
  {  (((1 - lambda) * p1) + (lambda * p2)) where lambda is Real : verum  }  c= the carrier of (TOP-REAL n)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (((1 - lambda) * p1) + (lambda * p2)) where lambda is Real : verum  }  or x in the carrier of (TOP-REAL n) )
assume  x in  {  (((1 - lambda) * p1) + (lambda * p2)) where lambda is Real : verum  }  ; ::_thesis: x in the carrier of (TOP-REAL n)
then  ex lambda being Real st x = ((1 - lambda) * p1) + (lambda * p2) ;
hence  x in the carrier of (TOP-REAL n) ; ::_thesis: verum
end;
hence   {  (((1 - lambda) * p1) + (lambda * p2)) where lambda is Real : verum  }  is Subset of (TOP-REAL n) ; ::_thesis: verum
end;
end;

:: deftheorem  defines Line EUCLID_4:def_3_:_
 for n being Nat
for p1, p2 being Point of (TOP-REAL n) holds Line (p1,p2) =  {  (((1 - lambda) * p1) + (lambda * p2)) where lambda is Real : verum  }  ;

registration
let n be Nat;
let p1, p2 be Point of (TOP-REAL n);
cluster Line (p1,p2) ->  non empty ;
coherence
 not Line (p1,p2) is empty
proof
A1: ( 0 * p2 = 0. (TOP-REAL n) & p1 + (0. (TOP-REAL n)) = p1 ) by EUCLID:27, EUCLID:29;
 ( 1 - 0 = 1 & 1 * p1 = p1 ) by EUCLID:29;
then  p1 in Line (p1,p2) by A1;
hence  not Line (p1,p2) is empty ; ::_thesis: verum
end;
end;

    Lm8:  for n being Nat
for p1, p2 being Point of (TOP-REAL n) ex x1, x2 being Element of REAL n st
( p1 = x1 & p2 = x2 & Line (x1,x2) = Line (p1,p2) )
proof
let n be Nat; ::_thesis: for p1, p2 being Point of (TOP-REAL n) ex x1, x2 being Element of REAL n st
( p1 = x1 & p2 = x2 & Line (x1,x2) = Line (p1,p2) )
let p1, p2 be Point of (TOP-REAL n); ::_thesis: ex x1, x2 being Element of REAL n st
( p1 = x1 & p2 = x2 & Line (x1,x2) = Line (p1,p2) )
reconsider x1 = p1, x2 = p2 as Element of REAL n by EUCLID:22;
take  x1 ; ::_thesis: ex x2 being Element of REAL n st
( p1 = x1 & p2 = x2 & Line (x1,x2) = Line (p1,p2) )
take  x2 ; ::_thesis: ( p1 = x1 & p2 = x2 & Line (x1,x2) = Line (p1,p2) )
thus  ( p1 = x1 & p2 = x2 ) ; ::_thesis: Line (x1,x2) = Line (p1,p2)
thus  Line (x1,x2) c= Line (p1,p2) :: according to XBOOLE_0:def_10 ::_thesis: Line (p1,p2) c= Line (x1,x2)
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in Line (x1,x2) or e in Line (p1,p2) )
assume  e in Line (x1,x2) ; ::_thesis: e in Line (p1,p2)
then consider lambda being Real such that
A1: e = ((1 - lambda) * x1) + (lambda * x2) ;
 e = ((1 - lambda) * p1) + (lambda * p2) by A1;
hence  e in Line (p1,p2) ; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in Line (p1,p2) or e in Line (x1,x2) )
assume  e in Line (p1,p2) ; ::_thesis: e in Line (x1,x2)
then consider lambda being Real such that
A2: e = ((1 - lambda) * p1) + (lambda * p2) ;
 e = ((1 - lambda) * x1) + (lambda * x2) by A2;
hence  e in Line (x1,x2) ; ::_thesis: verum
end;

definition
let n be Nat;
let p1, p2 be Point of (TOP-REAL n);
:: original: Line
redefine func Line (p1,p2) ->  Subset of (TOP-REAL n);
commutativity
 for p1, p2 being Point of (TOP-REAL n) holds Line (p1,p2) = Line (p2,p1)
proof
let p1, p2 be Point of (TOP-REAL n); ::_thesis: Line (p1,p2) = Line (p2,p1)
 ( ex x1, x2 being Element of REAL n st
( x1 = p1 & x2 = p2 & Line (x1,x2) = Line (p1,p2) ) & ex x29, x19 being Element of REAL n st
( x29 = p2 & x19 = p1 & Line (x29,x19) = Line (p2,p1) ) ) by Lm8;
hence  Line (p1,p2) = Line (p2,p1) ; ::_thesis: verum
end;
end;

theorem Th41: :: EUCLID_4:41
for n being Nat
for p1, p2 being Point of (TOP-REAL n) holds
( p1 in Line (p1,p2) & p2 in Line (p1,p2) )
proof
let n be Nat; ::_thesis: for p1, p2 being Point of (TOP-REAL n) holds
( p1 in Line (p1,p2) & p2 in Line (p1,p2) )
let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( p1 in Line (p1,p2) & p2 in Line (p1,p2) )
 ex x1, x2 being Element of REAL n st
( x1 = p1 & x2 = p2 & Line (x1,x2) = Line (p1,p2) ) by Lm8;
hence  ( p1 in Line (p1,p2) & p2 in Line (p1,p2) ) by Th9; ::_thesis: verum
end;

theorem Th42: :: EUCLID_4:42
for n being Nat
for q1, p1, p2, q2 being Point of (TOP-REAL n) st q1 in Line (p1,p2) & q2 in Line (p1,p2) holds
Line (q1,q2) c= Line (p1,p2)
proof
let n be Nat; ::_thesis: for q1, p1, p2, q2 being Point of (TOP-REAL n) st q1 in Line (p1,p2) & q2 in Line (p1,p2) holds
Line (q1,q2) c= Line (p1,p2)
let q1, p1, p2, q2 be Point of (TOP-REAL n); ::_thesis: ( q1 in Line (p1,p2) & q2 in Line (p1,p2) implies Line (q1,q2) c= Line (p1,p2) )
assume A1: ( q1 in Line (p1,p2) & q2 in Line (p1,p2) ) ; ::_thesis: Line (q1,q2) c= Line (p1,p2)
 ( ex x1, x2 being Element of REAL n st
( x1 = p1 & x2 = p2 & Line (x1,x2) = Line (p1,p2) ) & ex y1, y2 being Element of REAL n st
( y1 = q1 & y2 = q2 & Line (y1,y2) = Line (q1,q2) ) ) by Lm8;
hence  Line (q1,q2) c= Line (p1,p2) by A1, Th10; ::_thesis: verum
end;

theorem Th43: :: EUCLID_4:43
for n being Nat
for q1, p1, p2, q2 being Point of (TOP-REAL n) st q1 in Line (p1,p2) & q2 in Line (p1,p2) & q1 <> q2 holds
Line (p1,p2) c= Line (q1,q2)
proof
let n be Nat; ::_thesis: for q1, p1, p2, q2 being Point of (TOP-REAL n) st q1 in Line (p1,p2) & q2 in Line (p1,p2) & q1 <> q2 holds
Line (p1,p2) c= Line (q1,q2)
let q1, p1, p2, q2 be Point of (TOP-REAL n); ::_thesis: ( q1 in Line (p1,p2) & q2 in Line (p1,p2) & q1 <> q2 implies Line (p1,p2) c= Line (q1,q2) )
assume A1: ( q1 in Line (p1,p2) & q2 in Line (p1,p2) & q1 <> q2 ) ; ::_thesis: Line (p1,p2) c= Line (q1,q2)
 ( ex x1, x2 being Element of REAL n st
( x1 = p1 & x2 = p2 & Line (x1,x2) = Line (p1,p2) ) & ex y1, y2 being Element of REAL n st
( y1 = q1 & y2 = q2 & Line (y1,y2) = Line (q1,q2) ) ) by Lm8;
hence  Line (p1,p2) c= Line (q1,q2) by A1, Th11; ::_thesis: verum
end;

definition
let n be Nat;
let A be Subset of (TOP-REAL n);
attrA is being_line  means :Def4: :: EUCLID_4:def 4
 ex p1, p2 being Point of (TOP-REAL n) st
( p1 <> p2 & A = Line (p1,p2) );
end;

:: deftheorem Def4 defines being_line EUCLID_4:def_4_:_
 for n being Nat
for A being Subset of (TOP-REAL n) holds
( A is being_line iff ex p1, p2 being Point of (TOP-REAL n) st
( p1 <> p2 & A = Line (p1,p2) ) );

Lm9:  for n being Nat
for A being Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st A is being_line & p1 in A & p2 in A & p1 <> p2 holds
A = Line (p1,p2)
proof
let n be Nat; ::_thesis: for A being Subset of (TOP-REAL n)
for p1, p2 being Point of (TOP-REAL n) st A is being_line & p1 in A & p2 in A & p1 <> p2 holds
A = Line (p1,p2)
let A be Subset of (TOP-REAL n); ::_thesis: for p1, p2 being Point of (TOP-REAL n) st A is being_line & p1 in A & p2 in A & p1 <> p2 holds
A = Line (p1,p2)
let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( A is being_line & p1 in A & p2 in A & p1 <> p2 implies A = Line (p1,p2) )
assume that
A1: A is being_line and
A2: ( p1 in A & p2 in A & p1 <> p2 ) ; ::_thesis: A = Line (p1,p2)
 ex q1, q2 being Point of (TOP-REAL n) st
( q1 <> q2 & A = Line (q1,q2) ) by A1, Def4;
then  ( Line (p1,p2) c= A & A c= Line (p1,p2) ) by A2, Th42, Th43;
hence  A = Line (p1,p2) by XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: EUCLID_4:44
for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for A, C being Subset of (TOP-REAL n) st A is being_line & C is being_line & p1 in A & p2 in A & p1 in C & p2 in C & not p1 = p2 holds
A = C
proof
let n be Nat; ::_thesis: for p1, p2 being Point of (TOP-REAL n)
for A, C being Subset of (TOP-REAL n) st A is being_line & C is being_line & p1 in A & p2 in A & p1 in C & p2 in C & not p1 = p2 holds
A = C
let p1, p2 be Point of (TOP-REAL n); ::_thesis: for A, C being Subset of (TOP-REAL n) st A is being_line & C is being_line & p1 in A & p2 in A & p1 in C & p2 in C & not p1 = p2 holds
A = C
let A, C be Subset of (TOP-REAL n); ::_thesis: ( A is being_line & C is being_line & p1 in A & p2 in A & p1 in C & p2 in C & not p1 = p2 implies A = C )
assume that
A1: A is being_line and
A2: C is being_line and
A3: ( p1 in A & p2 in A ) and
A4: ( p1 in C & p2 in C ) ; ::_thesis: ( p1 = p2 or A = C )
assume A5: p1 <> p2 ; ::_thesis: A = C
then  A = Line (p1,p2) by A1, A3, Lm9;
hence  A = C by A2, A4, A5, Lm9; ::_thesis: verum
end;

theorem Th45: :: EUCLID_4:45
for n being Nat
for A being Subset of (TOP-REAL n) st A is being_line holds
ex p1, p2 being Point of (TOP-REAL n) st
( p1 in A & p2 in A & p1 <> p2 )
proof
let n be Nat; ::_thesis: for A being Subset of (TOP-REAL n) st A is being_line holds
ex p1, p2 being Point of (TOP-REAL n) st
( p1 in A & p2 in A & p1 <> p2 )
let A be Subset of (TOP-REAL n); ::_thesis: ( A is being_line implies ex p1, p2 being Point of (TOP-REAL n) st
( p1 in A & p2 in A & p1 <> p2 ) )
assume  A is being_line ; ::_thesis: ex p1, p2 being Point of (TOP-REAL n) st
( p1 in A & p2 in A & p1 <> p2 )
then consider p1, p2 being Point of (TOP-REAL n) such that
A1: p1 <> p2 and
A2: A = Line (p1,p2) by Def4;
 ( p1 in A & p2 in A ) by A2, Th41;
hence  ex p1, p2 being Point of (TOP-REAL n) st
( p1 in A & p2 in A & p1 <> p2 ) by A1; ::_thesis: verum
end;

theorem :: EUCLID_4:46
for n being Nat
for p1 being Point of (TOP-REAL n)
for A being Subset of (TOP-REAL n) st A is being_line holds
ex p2 being Point of (TOP-REAL n) st
( p1 <> p2 & p2 in A )
proof
let n be Nat; ::_thesis: for p1 being Point of (TOP-REAL n)
for A being Subset of (TOP-REAL n) st A is being_line holds
ex p2 being Point of (TOP-REAL n) st
( p1 <> p2 & p2 in A )
let p1 be Point of (TOP-REAL n); ::_thesis: for A being Subset of (TOP-REAL n) st A is being_line holds
ex p2 being Point of (TOP-REAL n) st
( p1 <> p2 & p2 in A )
let A be Subset of (TOP-REAL n); ::_thesis: ( A is being_line implies ex p2 being Point of (TOP-REAL n) st
( p1 <> p2 & p2 in A ) )
assume  A is being_line ; ::_thesis: ex p2 being Point of (TOP-REAL n) st
( p1 <> p2 & p2 in A )
then consider q1, q2 being Point of (TOP-REAL n) such that
A1: q1 in A and
A2: ( q2 in A & q1 <> q2 ) by Th45;
 ( p1 = q1 implies ( p1 <> q2 & q2 in A ) ) by A2;
hence  ex p2 being Point of (TOP-REAL n) st
( p1 <> p2 & p2 in A ) by A1; ::_thesis: verum
end;

theorem :: EUCLID_4:47
for n being Nat
for R being Subset of REAL
for p1, p2, q1 being Point of (TOP-REAL n) st R =  {  |.(q1 - p).| where p is Point of (TOP-REAL n) : p in Line (p1,p2)  }  holds
ex q2 being Point of (TOP-REAL n) st
( q2 in Line (p1,p2) & |.(q1 - q2).| = lower_bound R & p1 - p2,q1 - q2 are_orthogonal )
proof
let n be Nat; ::_thesis: for R being Subset of REAL
for p1, p2, q1 being Point of (TOP-REAL n) st R =  {  |.(q1 - p).| where p is Point of (TOP-REAL n) : p in Line (p1,p2)  }  holds
ex q2 being Point of (TOP-REAL n) st
( q2 in Line (p1,p2) & |.(q1 - q2).| = lower_bound R & p1 - p2,q1 - q2 are_orthogonal )
let R be Subset of REAL; ::_thesis: for p1, p2, q1 being Point of (TOP-REAL n) st R =  {  |.(q1 - p).| where p is Point of (TOP-REAL n) : p in Line (p1,p2)  }  holds
ex q2 being Point of (TOP-REAL n) st
( q2 in Line (p1,p2) & |.(q1 - q2).| = lower_bound R & p1 - p2,q1 - q2 are_orthogonal )
let p1, p2, q1 be Point of (TOP-REAL n); ::_thesis: ( R =  {  |.(q1 - p).| where p is Point of (TOP-REAL n) : p in Line (p1,p2)  }  implies ex q2 being Point of (TOP-REAL n) st
( q2 in Line (p1,p2) & |.(q1 - q2).| = lower_bound R & p1 - p2,q1 - q2 are_orthogonal ) )
reconsider y1 = q1 as Element of REAL n by EUCLID:22;
consider x1, x2 being Element of REAL n such that
A1: ( p1 = x1 & p2 = x2 ) and
A2: Line (x1,x2) = Line (p1,p2) by Lm8;
A3: x1 - x2 = p1 - p2 by A1;
consider y2 being Element of REAL n such that
A4: y2 in Line (x1,x2) and
A5: x1 - x2,y1 - y2 are_orthogonal and
A6: for x being Element of REAL n st x in Line (x1,x2) holds
|.(y1 - y2).| <= |.(y1 - x).| by Lm7;
reconsider q2 = y2 as Point of (TOP-REAL n) by EUCLID:22;
assume A7: R =  {  |.(q1 - p).| where p is Point of (TOP-REAL n) : p in Line (p1,p2)  }  ; ::_thesis: ex q2 being Point of (TOP-REAL n) st
( q2 in Line (p1,p2) & |.(q1 - q2).| = lower_bound R & p1 - p2,q1 - q2 are_orthogonal )
A8: for s being real number st 0 < s holds
ex r being real number st
( r in R & r < |.(q1 - q2).| + s )
proof
let s be real number ; ::_thesis: ( 0 < s implies ex r being real number st
( r in R & r < |.(q1 - q2).| + s ) )
assume A9: 0 < s ; ::_thesis: ex r being real number st
( r in R & r < |.(q1 - q2).| + s )
take  |.(q1 - q2).| ; ::_thesis: ( |.(q1 - q2).| in R & |.(q1 - q2).| < |.(q1 - q2).| + s )
thus  ( |.(q1 - q2).| in R & |.(q1 - q2).| < |.(q1 - q2).| + s ) by A7, A2, A4, A9, XREAL_1:29; ::_thesis: verum
end;
 p1 in Line (p1,p2) by Th41;
then A10: |.(q1 - p1).| in R by A7;
A11: for r being real number st r in R holds
|.(q1 - q2).| <= r
proof
let r be real number ; ::_thesis: ( r in R implies |.(q1 - q2).| <= r )
assume  r in R ; ::_thesis: |.(q1 - q2).| <= r
then consider p0 being Point of (TOP-REAL n) such that
A12: ( r = |.(q1 - p0).| & p0 in Line (p1,p2) ) by A7;
 the carrier of (Euclid n) = the carrier of (TOP-REAL n) by EUCLID:67;
then reconsider x = p0 as Element of REAL n ;
thus  |.(q1 - q2).| <= r by A2, A6, A12; ::_thesis: verum
end;
 R is bounded_below
proof
take  |.(q1 - q2).| ; :: according to XXREAL_2:def_9 ::_thesis: |.(q1 - q2).| is LowerBound of R
let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in R or |.(q1 - q2).| <= r )
assume  r in R ; ::_thesis: |.(q1 - q2).| <= r
then consider p0 being Point of (TOP-REAL n) such that
A13: ( r = |.(q1 - p0).| & p0 in Line (p1,p2) ) by A7;
 the carrier of (Euclid n) = the carrier of (TOP-REAL n) by EUCLID:67;
then reconsider x = p0 as Element of REAL n ;
thus  |.(q1 - q2).| <= r by A2, A6, A13; ::_thesis: verum
end;
then  ( y1 - y2 = q1 - q2 & |.(q1 - q2).| = lower_bound R ) by A10, A8, A11, SEQ_4:def_2;
hence  ex q2 being Point of (TOP-REAL n) st
( q2 in Line (p1,p2) & |.(q1 - q2).| = lower_bound R & p1 - p2,q1 - q2 are_orthogonal ) by A2, A4, A5, A3; ::_thesis: verum
end;