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

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, y being Point of X holds

( ||.(x - y).|| > 0 iff x <> y )

for x, y being Point of X holds ||.(x - y).|| = ||.(y - x).||

for x being Point of X st ( for e being Real st e > 0 holds

||.x.|| < e ) holds

x = 0. X

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 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).|| = ||.(y - x).|| ) & ( 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 A6, A7, A1, A2, A8; :: thesis: verum

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

A2:
for X being RealNormSpace
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;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

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

A6:
for X being RealNormSpace
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;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

for x, y being Point of X holds

( ||.(x - y).|| > 0 iff x <> y )

proof

A7:
for X being RealNormSpace
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 )

end;( ||.(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).|| )

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

then 0 <> ||.(x - y).|| by NORMSP_1:11;

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

end;then 0 <> ||.(x - y).|| by NORMSP_1:11;

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

for x, y being Point of X holds ||.(x - y).|| = ||.(y - x).||

proof

A8:
for X being RealNormSpace
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;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

for x being Point of X st ( for e being Real st e > 0 holds

||.x.|| < e ) holds

x = 0. X

proof

thus
( ( for X being RealNormSpace
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 A9: for e being Real st e > 0 holds

||.x.|| < e ; :: thesis: x = 0. X

end;||.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 A9: for e being Real st e > 0 holds

||.x.|| < e ; :: thesis: x = 0. X

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

hence
x = 0. X
; :: thesis: verumassume
x <> 0. X
; :: thesis: contradiction

then 0 <> ||.x.|| by NORMSP_0:def 5;

then 0 < ||.x.|| ;

hence contradiction by A9; :: thesis: verum

end;then 0 <> ||.x.|| by NORMSP_0:def 5;

then 0 < ||.x.|| ;

hence contradiction by A9; :: thesis: verum

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 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).|| = ||.(y - x).|| ) & ( 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 A6, A7, A1, A2, A8; :: thesis: verum