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₁[ set ] means ex X being Subset of T st
( 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₁[B] holds
S₁[B \/ {x}]

proof

let x, B be set ; :: thesis: ( x in P & B c= P & S₁[B] implies S₁[B \/ {x}] )
assume that
A3: x in P and
B c= P and
A4: S₁[B] ; :: thesis: S₁[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 Th22;
ex Y being Subset of T st
( Y = B \/ {x} & Y is bounded )

proof

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

end;

hence S₁[B \/ {x}] ; :: thesis: verum

end;

assume A7: P is finite ; :: thesis: P is bounded
S₁[P] from FINSET_1:sch 2(A7, A1, A2);
hence P is bounded ; :: thesis: verum