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 ) ) ) )

per cases ( x1 <> x2 or x1 = x2 ) ;

case A1: 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 ) ; :: thesis: verum

end;

case A3: 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 ) ; :: 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;
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:9, SQUARE_1:22;
hence |.(y1 - y2).| <= |.(y1 - x).| by EUCLID:9, 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