thus for X being RealNormSpace
for x, y being Point of X holds
( ||.(x - y).|| > 0 iff x <> y ) :: thesis: ( ( for X being RealNormSpace
for x, y being Point of X holds ||.(x - y).|| = ||.(y - x).|| ) & ( for X being RealNormSpace
for x, y being Point of X holds
( ||.(x - y).|| = 0 iff x = y ) ) & ( for X being RealNormSpace
for x, y being Point of X holds
( ||.(x - y).|| <> 0 iff x <> y ) ) & ( for X being RealNormSpace
for x, y, z being Point of X
for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 holds
||.(x - y).|| < e ) & ( for X being RealNormSpace
for x, y, z being Point of X
for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 holds
||.(x - y).|| < e ) & ( for X being RealNormSpace
for x being Point of X st ( for e being Real st e > 0 holds
||.x.|| < e ) holds
x = 0. X ) & ( for X being RealNormSpace
for x, y being Point of X st ( for e being Real st e > 0 holds
||.(x - y).|| < e ) holds
x = y ) )

proof

let X be RealNormSpace; :: thesis: for x, y being Point of X holds
( ||.(x - y).|| > 0 iff x <> y )
let x, y be Point of X; :: thesis: ( ||.(x - y).|| > 0 iff x <> y )
( 0 < ||.(x - y).|| implies x - y <> 0. X ) by NORMSP_0:def 6;
hence ( 0 < ||.(x - y).|| implies x <> y ) by RLVECT_1:15; :: thesis: ( x <> y implies ||.(x - y).|| > 0 )

now :: thesis: ( x <> y implies 0 < ||.(x - y).|| )

assume x <> y ; :: thesis: 0 < ||.(x - y).||
then 0 <> ||.(x - y).|| by NORMSP_1:11;
hence 0 < ||.(x - y).|| by NORMSP_1:4; :: thesis: verum

end;

hence ( x <> y implies ||.(x - y).|| > 0 ) ; :: thesis: verum

end;

thus for X being RealNormSpace
for x, y being Point of X holds ||.(x - y).|| = ||.(y - x).|| :: thesis: ( ( for X being RealNormSpace
for x, y being Point of X holds
( ||.(x - y).|| = 0 iff x = y ) ) & ( for X being RealNormSpace
for x, y being Point of X holds
( ||.(x - y).|| <> 0 iff x <> y ) ) & ( for X being RealNormSpace
for x, y, z being Point of X
for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 holds
||.(x - y).|| < e ) & ( for X being RealNormSpace
for x, y, z being Point of X
for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 holds
||.(x - y).|| < e ) & ( for X being RealNormSpace
for x being Point of X st ( for e being Real st e > 0 holds
||.x.|| < e ) holds
x = 0. X ) & ( for X being RealNormSpace
for x, y being Point of X st ( for e being Real st e > 0 holds
||.(x - y).|| < e ) holds
x = y ) )

proof

let X be RealNormSpace; :: thesis: for x, y being Point of X holds ||.(x - y).|| = ||.(y - x).||
let x, y be Point of X; :: thesis: ||.(x - y).|| = ||.(y - x).||
thus ||.(x - y).|| = ||.(- (x - y)).|| by NORMSP_1:2
.= ||.(y - x).|| by RLVECT_1:33 ; :: thesis: verum

end;

A1: for X being RealNormSpace
for x, y, z being Point of X
for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 holds
||.(x - y).|| < e

proof

let X be RealNormSpace; :: thesis: for x, y, z being Point of X
for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 holds
||.(x - y).|| < e
let x, y, z be Point of X; :: thesis: for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 holds
||.(x - y).|| < e
let e be Real; :: thesis: ( e > 0 & ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 implies ||.(x - y).|| < e )
assume e > 0 ; :: thesis: ( not ||.(x - z).|| < e / 2 or not ||.(z - y).|| < e / 2 or ||.(x - y).|| < e )
assume ( ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 ) ; :: thesis: ||.(x - y).|| < e
then ||.(x - z).|| + ||.(z - y).|| < (e / 2) + (e / 2) by XREAL_1:8;
then ||.(x - y).|| + (||.(x - z).|| + ||.(z - y).||) < (||.(x - z).|| + ||.(z - y).||) + e by NORMSP_1:10, XREAL_1:8;
then (||.(x - y).|| + (||.(x - z).|| + ||.(z - y).||)) + (- (||.(x - z).|| + ||.(z - y).||)) < (e + (||.(x - z).|| + ||.(z - y).||)) + (- (||.(x - z).|| + ||.(z - y).||)) by XREAL_1:8;
hence ||.(x - y).|| < e ; :: thesis: verum

end;

A2: for X being RealNormSpace
for x, y, z being Point of X
for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 holds
||.(x - y).|| < e

proof

let X be RealNormSpace; :: thesis: for x, y, z being Point of X
for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 holds
||.(x - y).|| < e
let x, y, z be Point of X; :: thesis: for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 holds
||.(x - y).|| < e
let e be Real; :: thesis: ( e > 0 & ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 implies ||.(x - y).|| < e )
assume A3: e > 0 ; :: thesis: ( not ||.(x - z).|| < e / 2 or not ||.(y - z).|| < e / 2 or ||.(x - y).|| < e )
assume that
A4: ||.(x - z).|| < e / 2 and
A5: ||.(y - z).|| < e / 2 ; :: thesis: ||.(x - y).|| < e
||.(- (y - z)).|| < e / 2 by A5, NORMSP_1:2;
then ||.(z - y).|| < e / 2 by RLVECT_1:33;
hence ||.(x - y).|| < e by A1, A3, A4; :: thesis: verum

end;

A6: for X being RealNormSpace
for x being Point of X st ( for e being Real st e > 0 holds
||.x.|| < e ) holds
x = 0. X

proof

let X be RealNormSpace; :: thesis: for x being Point of X st ( for e being Real st e > 0 holds
||.x.|| < e ) holds
x = 0. X
let x be Point of X; :: thesis: ( ( for e being Real st e > 0 holds
||.x.|| < e ) implies x = 0. X )
assume A7: for e being Real st e > 0 holds
||.x.|| < e ; :: thesis: x = 0. X

now :: thesis: not x <> 0. X

assume x <> 0. X ; :: thesis: contradiction
then 0 <> ||.x.|| by NORMSP_0:def 5;
then 0 < ||.x.|| by NORMSP_1:4;
hence contradiction by A7; :: thesis: verum

end;

hence x = 0. X ; :: thesis: verum

end;

for X being RealNormSpace
for x, y being Point of X st ( for e being Real st e > 0 holds
||.(x - y).|| < e ) holds
x = y

proof

let X be RealNormSpace; :: thesis: for x, y being Point of X st ( for e being Real st e > 0 holds
||.(x - y).|| < e ) holds
x = y
let x, y be Point of X; :: thesis: ( ( for e being Real st e > 0 holds
||.(x - y).|| < e ) implies x = y )
assume for e being Real st e > 0 holds
||.(x - y).|| < e ; :: thesis: x = y
then x - y = 0. X by A6;
hence x = y by RLVECT_1:21; :: thesis: verum

end;

hence ( ( for X being RealNormSpace
for x, y being Point of X holds
( ||.(x - y).|| = 0 iff x = y ) ) & ( for X being RealNormSpace
for x, y being Point of X holds
( ||.(x - y).|| <> 0 iff x <> y ) ) & ( for X being RealNormSpace
for x, y, z being Point of X
for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(z - y).|| < e / 2 holds
||.(x - y).|| < e ) & ( for X being RealNormSpace
for x, y, z being Point of X
for e being Real st e > 0 & ||.(x - z).|| < e / 2 & ||.(y - z).|| < e / 2 holds
||.(x - y).|| < e ) & ( for X being RealNormSpace
for x being Point of X st ( for e being Real st e > 0 holds
||.x.|| < e ) holds
x = 0. X ) & ( for X being RealNormSpace
for x, y being Point of X st ( for e being Real st e > 0 holds
||.(x - y).|| < e ) holds
x = y ) ) by A1, A2, A6, NORMSP_1:6; :: thesis: verum