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 S₁[ 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 & S₁[B] holds
S₁[B \/ {x}]

proof

let x, B be set ; :: thesis: ( x in Y & B c= Y & S₁[B] implies S₁[B \/ {x}] )
assume that
A4: x in Y and
B c= Y and
A5: S₁[B] ; :: thesis: S₁[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}) = (union B) \/ (union {x}) by ZFMISC_1:78
.= (union B) \/ 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 S₁[B \/ {x}] ; :: thesis: verum

end;

A9: S₁[ {} ]

proof

set m = {} T;
{} T = union {} by ZFMISC_1:2;
hence S₁[ {} ] ; :: thesis: verum

end;

S₁[Y] from FINSET_1:sch 2(A1, A9, A3);
hence union Y is bounded ; :: thesis: verum