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
defpred S₁[ set ] means ex A being Subset of X st
( A = union $1 & A 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;

A4: 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
A5: x in F and
B c= F and
A6: S₁[B] ; :: thesis: S₁[B \/ {x}]
consider A being Subset of X such that
A7: ( A = union B & A is bounded ) by A6;
reconsider x = x as Subset of X by A5;
A8: union (B \/ {x}) = (union B) \/ (union {x}) by ZFMISC_1:78
.= (union B) \/ x by ZFMISC_1:25 ;
A9: x is bounded by A3, A5;
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 A7, A8, A9, Th42; :: thesis: verum

end;

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

end;

{} X = union {} by ZFMISC_1:2;
then A10: S₁[ {} ] ;
S₁[F] from FINSET_1:sch 2(A1, A10, A4);
hence union F is bounded ; :: thesis: verum