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 S1[ set ] means ex X being Subset of T st
( X = \$1 & X is bounded );
{} T is bounded ;
then A1: S1[ {} ] ;
A2: for x, B being set st x in P & B c= P & S1[B] holds
S1[B \/ {x}]
proof
let x, B be set ; :: thesis: ( x in P & B c= P & S1[B] implies S1[B \/ {x}] )
assume that
A3: x in P and
B c= P and
A4: S1[B] ; :: thesis: S1[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 )
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, Th13; :: thesis: verum
end;
hence S1[B \/ {x}] ; :: thesis: verum
end;
assume A7: P is finite ; :: thesis: P is bounded
S1[P] from FINSET_1:sch 2(A7, A1, A2);
hence P is bounded ; :: thesis: verum