let n be 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 & 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 & 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 & C is bounded holds
A is bounded
let C be Subset of ((Euclid n) | B); :: thesis: ( A = C & C is bounded implies A is bounded )
assume that
A1: A = C and
A2: C is bounded ; :: thesis: A is bounded
consider r0 being Real such that
A3: 0 < r0 and
A4: for x, y being Point of ((Euclid n) | B) st x in C & y in C holds
dist (x,y) <= r0 by A2;
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 A5: ( 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;
( the distance of ((Euclid n) | B) . (x0,y0) = the distance of (Euclid n) . (x,y) & the distance of ((Euclid n) | B) . (x0,y0) = dist (x0,y0) ) by TOPMETR:def 1;
hence dist (x,y) <= r0 by A1, A4, A5; :: thesis: verum

end;

hence A is bounded by A3; :: thesis: verum