let n be 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

A1: for r being Real st r in dist_v (x,L) holds
0 <= r

proof

let r be Real; :: thesis: ( r in dist_v (x,L) implies 0 <= r )
assume r in dist_v (x,L) ; :: thesis: 0 <= r
then ex x0 being Element of REAL n st
( r = |.(x - x0).| & x0 in L ) ;
hence 0 <= r ; :: thesis: verum

end;

A2: dist_v (x,L) is bounded_below

proof

take 0 ; :: according to XXREAL_2:def 9 :: thesis: 0 is LowerBound of dist_v (x,L)
let r be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not r in dist_v (x,L) or 0 <= r )
assume r in dist_v (x,L) ; :: thesis: 0 <= r
then ex x0 being Element of REAL n st
( r = |.(x - x0).| & x0 in L ) ;
hence 0 <= r ; :: thesis: verum

end;

assume A3: x in L ; :: thesis: dist (x,L) = 0
|.(x - x).| = |.(0* n).| by Th9
.= sqrt |((0* n),(0* n))| by EUCLID_4:15
.= 0 by EUCLID_4:17, SQUARE_1:17 ;
then A4: 0 in dist_v (x,L) by A3;
then for s being Real st 0 < s holds
ex r being Real st
( r in dist_v (x,L) & r < 0 + s ) ;
hence dist (x,L) = 0 by A4, A1, A2, SEQ_4:def 2; :: thesis: verum

end;

now :: thesis: ( dist (x,L) = 0 implies x in L )

consider x0 being Element of REAL n such that
A5: x0 in L and
A6: |.(x - x0).| = dist (x,L) by Th57;
assume dist (x,L) = 0 ; :: thesis: x in L
then |((x - x0),(x - x0))| = 0 by A6, EUCLID_4:16;
then x - x0 = 0* n by EUCLID_4:17;
hence x in L by A5, Th9; :: thesis: verum

end;

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