let T be non empty Reflexive symmetric triangle MetrStruct ; :: thesis: for Y being Subset-Family of T st Y is finite & ( for P being Subset of T st P in Y holds
P is bounded ) holds
union Y is bounded

let Y be Subset-Family of T; :: thesis: ( Y is finite & ( for P being Subset of T st P in Y holds
P is bounded ) implies union Y is bounded )

assume that
A1: Y is finite and
A2: for P being Subset of T st P in Y holds
P is bounded ; :: thesis: union Y is bounded
defpred S1[ set ] means ex X being Subset of T st
( X = union \$1 & X is bounded );
A3: for x, B being set st x in Y & B c= Y & S1[B] holds
S1[B \/ {x}]
proof
let x, B be set ; :: thesis: ( x in Y & B c= Y & S1[B] implies S1[B \/ {x}] )
assume that
A4: x in Y and
B c= Y and
A5: S1[B] ; :: thesis: S1[B \/ {x}]
consider X being Subset of T such that
A6: ( X = union B & X is bounded ) by A5;
reconsider x = x as Subset of T by A4;
A7: union (B \/ {x}) = () \/ () by ZFMISC_1:78
.= () \/ x by ZFMISC_1:25 ;
A8: x is bounded by A2, A4;
ex Y being Subset of T st
( Y = union (B \/ {x}) & Y is bounded )
proof
take X \/ x ; :: thesis: ( X \/ x = union (B \/ {x}) & X \/ x is bounded )
thus ( X \/ x = union (B \/ {x}) & X \/ x is bounded ) by A6, A7, A8, Th13; :: thesis: verum
end;
hence S1[B \/ {x}] ; :: thesis: verum
end;
A9: S1[ {} ]
proof
set m = {} T;
{} T = union {} by ZFMISC_1:2;
hence S1[ {} ] ; :: thesis: verum
end;
S1[Y] from FINSET_1:sch 2(A1, A9, A3);
hence union Y is bounded ; :: thesis: verum