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 & 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, 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 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;
A6: ( 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 METRIC_1:def 1, TOPMETR:def 1;
dist x0,y0 <= r0 by A1, A4, A5;
hence dist x,y <= r0 by A6, METRIC_1:def 1; :: thesis: verum

end;

hence A is bounded by A3, TBSP_1:def 9; :: thesis: verum