let X be LinearTopSpace; :: thesis: for F being Subset-Family of X st F is finite & F = { P where P is bounded Subset of X : verum } holds
union F is bounded
let F be Subset-Family of X; :: thesis: ( F is finite & F = { P where P is bounded Subset of X : verum } implies union F is bounded )
assume that
A1: F is finite and
A2: F = { P where P is bounded Subset of X : verum } ; :: thesis: union F is bounded

A3: now

let P be Subset of X; :: thesis: ( P in F implies P is bounded )
assume P in F ; :: thesis: P is bounded
then ex A being bounded Subset of X st P = A by A2;
hence P is bounded ; :: thesis: verum

end;

defpred S₁[ set ] means ex A being Subset of X st
( A = union $1 & A is bounded );
( {} X = union {} & {} X is bounded ) by ZFMISC_1:2;
then A4: S₁[ {} ] ;
A5: for x, B being set st x in F & B c= F & S₁[B] holds
S₁[B \/ {x}]

proof

let x, B be set ; :: thesis: ( x in F & B c= F & S₁[B] implies S₁[B \/ {x}] )
assume that
A6: x in F and
B c= F and
A7: S₁[B] ; :: thesis: S₁[B \/ {x}]
consider A being Subset of X such that
A8: A = union B and
A9: A is bounded by A7;
reconsider x = x as Subset of X by A6;
A10: union (B \/ {x}) = (union B) \/ (union {x}) by ZFMISC_1:96
.= (union B) \/ x by ZFMISC_1:31 ;
A11: x is bounded by A3, A6;
ex Y being Subset of X st
( Y = union (B \/ {x}) & Y is bounded )

proof

take A \/ x ; :: thesis: ( A \/ x = union (B \/ {x}) & A \/ x is bounded )
thus ( A \/ x = union (B \/ {x}) & A \/ x is bounded ) by A8, A9, A10, A11, Th42; :: thesis: verum

end;

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

end;

S₁[F] from FINSET_1:sch 2(A1, A4, A5);
hence union F is bounded ; :: thesis: verum