let n be Element of NAT ; :: thesis: for A being Subset of (Euclid n)
for B being non empty Subset of (Euclid n)
for C being Subset of ((Euclid n) | B) st A c= B & A = C & C is bounded holds
A is bounded
let A be Subset of (Euclid n); :: thesis: for B being non empty Subset of (Euclid n)
for C being Subset of ((Euclid n) | B) st A c= B & A = C & C is bounded holds
A is bounded
let B be non empty Subset of (Euclid n); :: thesis: for C being Subset of ((Euclid n) | B) st A c= B & A = C & C is bounded holds
A is bounded
let C be Subset of ((Euclid n) | B); :: thesis: ( A c= B & A = C & C is bounded implies A is bounded )
assume A1:
( A c= B & A = C & C is bounded )
; :: thesis: A is bounded
then consider r0 being Real such that
A2:
( 0 < r0 & ( for x, y being Point of ((Euclid n) | B) st x in C & y in C holds
dist x,y <= r0 ) )
by TBSP_1:def 9;
for x, y being Point of (Euclid n) st x in A & y in A holds
dist x,y <= r0
proof
let x,
y be
Point of
(Euclid n);
:: thesis: ( x in A & y in A implies dist x,y <= r0 )
assume A3:
(
x in A &
y in A )
;
:: thesis: dist x,y <= r0
then reconsider x0 =
x,
y0 =
y as
Point of
((Euclid n) | B) by A1;
A4:
dist x0,
y0 <= r0
by A1, A2, A3;
A5:
the
distance of
((Euclid n) | B) . x0,
y0 = the
distance of
(Euclid n) . x,
y
by TOPMETR:def 1;
the
distance of
((Euclid n) | B) . x0,
y0 = dist x0,
y0
by METRIC_1:def 1;
hence
dist x,
y <= r0
by A4, A5, METRIC_1:def 1;
:: thesis: verum
end;
hence
A is bounded
by A2, TBSP_1:def 9; :: thesis: verum