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_{1}[ 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_{1}[B] holds

S_{1}[B \/ {x}]
_{1}[ {} ]
S_{1}[Y]
from FINSET_1:sch 2(A1, A9, A3);

hence union Y is bounded ; :: thesis: verum

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

( X = union $1 & X is bounded );

A3: for x, B being set st x in Y & B c= Y & S

S

proof

A9:
S
let x, B be set ; :: thesis: ( x in Y & B c= Y & S_{1}[B] implies S_{1}[B \/ {x}] )

assume that

A4: x in Y and

B c= Y and

A5: S_{1}[B]
; :: thesis: S_{1}[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 )_{1}[B \/ {x}]
; :: thesis: verum

end;assume that

A4: x in Y and

B c= Y and

A5: S

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

hence
S
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;thus ( X \/ x = union (B \/ {x}) & X \/ x is bounded ) by A6, A7, A8, Th13; :: thesis: verum

hence union Y is bounded ; :: thesis: verum