begin
Lm1:
for N being non empty MetrStruct
for f being Function holds
( f is sequence of N iff ( dom f = NAT & ( for x being set st x in NAT holds
f . x is Element of N ) ) )
Lm2:
for T being non empty Reflexive symmetric triangle MetrStruct
for t1 being Element of T
for r being real number st 0 < r holds
Ball (t1,r) is bounded
definition
let N be non
empty Reflexive MetrStruct ;
let C be
Subset of
N;
assume A1:
C is
bounded
;
consistency
for b1 being Real holds verum
;
existence
( ( C <> {} implies ex b1 being Real st
( ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= b1 ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= s ) holds
b1 <= s ) ) ) & ( not C <> {} implies ex b1 being Real st b1 = 0 ) )
uniqueness
for b1, b2 being Real holds
( ( C <> {} & ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= b1 ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= s ) holds
b1 <= s ) & ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= b2 ) & ( for s being Real st ( for x, y being Point of N st x in C & y in C holds
dist (x,y) <= s ) holds
b2 <= s ) implies b1 = b2 ) & ( not C <> {} & b1 = 0 & b2 = 0 implies b1 = b2 ) )
end;