let T be non empty Reflexive symmetric triangle MetrStruct ; :: thesis: for P being Subset of T st P is finite holds

P is bounded

let P be Subset of T; :: thesis: ( P is finite implies P is bounded )

defpred S_{1}[ set ] means ex X being Subset of T st

( X = $1 & X is bounded );

{} T is bounded ;

then A1: S_{1}[ {} ]
;

A2: for x, B being set st x in P & B c= P & S_{1}[B] holds

S_{1}[B \/ {x}]

S_{1}[P]
from FINSET_1:sch 2(A7, A1, A2);

hence P is bounded ; :: thesis: verum

P is bounded

let P be Subset of T; :: thesis: ( P is finite implies P is bounded )

defpred S

( X = $1 & X is bounded );

{} T is bounded ;

then A1: S

A2: for x, B being set st x in P & B c= P & S

S

proof

assume A7:
P is finite
; :: thesis: P is bounded
let x, B be set ; :: thesis: ( x in P & B c= P & S_{1}[B] implies S_{1}[B \/ {x}] )

assume that

A3: x in P and

B c= P and

A4: S_{1}[B]
; :: thesis: S_{1}[B \/ {x}]

reconsider x = x as Element of T by A3;

reconsider W = {x} as Subset of T ;

consider X being Subset of T such that

A5: ( X = B & X is bounded ) by A4;

A6: W is bounded by Th15;

ex Y being Subset of T st

( Y = B \/ {x} & Y is bounded )_{1}[B \/ {x}]
; :: thesis: verum

end;assume that

A3: x in P and

B c= P and

A4: S

reconsider x = x as Element of T by A3;

reconsider W = {x} as Subset of T ;

consider X being Subset of T such that

A5: ( X = B & X is bounded ) by A4;

A6: W is bounded by Th15;

ex Y being Subset of T st

( Y = B \/ {x} & Y is bounded )

proof

hence
S
take
X \/ W
; :: thesis: ( X \/ W = B \/ {x} & X \/ W is bounded )

thus ( X \/ W = B \/ {x} & X \/ W is bounded ) by A5, A6, Th13; :: thesis: verum

end;thus ( X \/ W = B \/ {x} & X \/ W is bounded ) by A5, A6, Th13; :: thesis: verum

S

hence P is bounded ; :: thesis: verum