let n be Element of NAT ; :: thesis: for x being Element of REAL n
for L being Element of line_of_REAL n holds
( x in L iff dist x,L = 0 )
let x be Element of REAL n; :: thesis: for L being Element of line_of_REAL n holds
( x in L iff dist x,L = 0 )
let L be Element of line_of_REAL n; :: thesis: ( x in L iff dist x,L = 0 )
thus ( x in L implies dist x,L = 0 ) :: thesis: ( dist x,L = 0 implies x in L )

proof

assume A1: x in L ; :: thesis: dist x,L = 0
|.(x - x).| = |.(0* n).| by Th14
.= sqrt |((0* n),(0* n))| by EUCLID_4:20
.= 0 by EUCLID_4:22, SQUARE_1:82 ;
then A2: 0 in dist_v x,L by A1;
then A3: for s being real number st 0 < s holds
ex r being real number st
( r in dist_v x,L & r < 0 + s ) ;
A4: for r being real number st r in dist_v x,L holds
0 <= r

proof

let r be real number ; :: thesis: ( r in dist_v x,L implies 0 <= r )
assume r in dist_v x,L ; :: thesis: 0 <= r
then consider x0 being Element of REAL n such that
A5: ( r = |.(x - x0).| & x0 in L ) ;
thus 0 <= r by A5; :: thesis: verum

end;

then dist_v x,L is bounded_below by SEQ_4:def 2;
hence dist x,L = 0 by A2, A3, A4, SEQ_4:def 5; :: thesis: verum

end;

now

assume A6: dist x,L = 0 ; :: thesis: x in L
consider x0 being Element of REAL n such that
A7: ( x0 in L & |.(x - x0).| = dist x,L ) by Th62;
|((x - x0),(x - x0))| = 0 by A6, A7, EUCLID_4:21;
then x - x0 = 0* n by EUCLID_4:22;
hence x in L by A7, Th14; :: thesis: verum

end;

hence ( dist x,L = 0 implies x in L ) ; :: thesis: verum