let GX be non empty TopSpace; :: thesis: for Fu being Subset-Family of GX st ( for A being Subset of GX st A in Fu holds

A is a_union_of_components of GX ) holds

union Fu is a_union_of_components of GX

let Fu be Subset-Family of GX; :: thesis: ( ( for A being Subset of GX st A in Fu holds

A is a_union_of_components of GX ) implies union Fu is a_union_of_components of GX )

{ B where B is Subset of GX : ex B2 being Subset of GX st

( B2 in Fu & B c= B2 & B is a_component ) } c= bool the carrier of GX

( B2 in Fu & B c= B2 & B is a_component ) } as Subset-Family of GX ;

A1: for B being Subset of GX st B in F2 holds

B is a_component

A is a_union_of_components of GX ; :: thesis: union Fu is a_union_of_components of GX

A3: union Fu c= union F2

hence union Fu is a_union_of_components of GX by A1, Def2; :: thesis: verum

A is a_union_of_components of GX ) holds

union Fu is a_union_of_components of GX

let Fu be Subset-Family of GX; :: thesis: ( ( for A being Subset of GX st A in Fu holds

A is a_union_of_components of GX ) implies union Fu is a_union_of_components of GX )

{ B where B is Subset of GX : ex B2 being Subset of GX st

( B2 in Fu & B c= B2 & B is a_component ) } c= bool the carrier of GX

proof

then reconsider F2 = { B where B is Subset of GX : ex B2 being Subset of GX st
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { B where B is Subset of GX : ex B2 being Subset of GX st

( B2 in Fu & B c= B2 & B is a_component ) } or x in bool the carrier of GX )

assume x in { B where B is Subset of GX : ex B2 being Subset of GX st

( B2 in Fu & B c= B2 & B is a_component ) } ; :: thesis: x in bool the carrier of GX

then ex B being Subset of GX st

( x = B & ex B2 being Subset of GX st

( B2 in Fu & B c= B2 & B is a_component ) ) ;

hence x in bool the carrier of GX ; :: thesis: verum

end;( B2 in Fu & B c= B2 & B is a_component ) } or x in bool the carrier of GX )

assume x in { B where B is Subset of GX : ex B2 being Subset of GX st

( B2 in Fu & B c= B2 & B is a_component ) } ; :: thesis: x in bool the carrier of GX

then ex B being Subset of GX st

( x = B & ex B2 being Subset of GX st

( B2 in Fu & B c= B2 & B is a_component ) ) ;

hence x in bool the carrier of GX ; :: thesis: verum

( B2 in Fu & B c= B2 & B is a_component ) } as Subset-Family of GX ;

A1: for B being Subset of GX st B in F2 holds

B is a_component

proof

assume A2:
for A being Subset of GX st A in Fu holds
let B be Subset of GX; :: thesis: ( B in F2 implies B is a_component )

assume B in F2 ; :: thesis: B is a_component

then ex A2 being Subset of GX st

( B = A2 & ex B2 being Subset of GX st

( B2 in Fu & A2 c= B2 & A2 is a_component ) ) ;

hence B is a_component ; :: thesis: verum

end;assume B in F2 ; :: thesis: B is a_component

then ex A2 being Subset of GX st

( B = A2 & ex B2 being Subset of GX st

( B2 in Fu & A2 c= B2 & A2 is a_component ) ) ;

hence B is a_component ; :: thesis: verum

A is a_union_of_components of GX ; :: thesis: union Fu is a_union_of_components of GX

A3: union Fu c= union F2

proof

union F2 c= union Fu
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union Fu or x in union F2 )

assume x in union Fu ; :: thesis: x in union F2

then consider X2 being set such that

A4: x in X2 and

A5: X2 in Fu by TARSKI:def 4;

reconsider B3 = X2 as Subset of GX by A5;

B3 is a_union_of_components of GX by A2, A5;

then consider F being Subset-Family of GX such that

A6: for B being Subset of GX st B in F holds

B is a_component and

A7: B3 = union F by Def2;

consider Y2 being set such that

A8: x in Y2 and

A9: Y2 in F by A4, A7, TARSKI:def 4;

reconsider A3 = Y2 as Subset of GX by A9;

( A3 is a_component & Y2 c= B3 ) by A6, A7, A9, ZFMISC_1:74;

then A3 in F2 by A5;

hence x in union F2 by A8, TARSKI:def 4; :: thesis: verum

end;assume x in union Fu ; :: thesis: x in union F2

then consider X2 being set such that

A4: x in X2 and

A5: X2 in Fu by TARSKI:def 4;

reconsider B3 = X2 as Subset of GX by A5;

B3 is a_union_of_components of GX by A2, A5;

then consider F being Subset-Family of GX such that

A6: for B being Subset of GX st B in F holds

B is a_component and

A7: B3 = union F by Def2;

consider Y2 being set such that

A8: x in Y2 and

A9: Y2 in F by A4, A7, TARSKI:def 4;

reconsider A3 = Y2 as Subset of GX by A9;

( A3 is a_component & Y2 c= B3 ) by A6, A7, A9, ZFMISC_1:74;

then A3 in F2 by A5;

hence x in union F2 by A8, TARSKI:def 4; :: thesis: verum

proof

then
union Fu = union F2
by A3;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union F2 or x in union Fu )

assume x in union F2 ; :: thesis: x in union Fu

then consider X being set such that

A10: x in X and

A11: X in F2 by TARSKI:def 4;

ex B being Subset of GX st

( X = B & ex B2 being Subset of GX st

( B2 in Fu & B c= B2 & B is a_component ) ) by A11;

hence x in union Fu by A10, TARSKI:def 4; :: thesis: verum

end;assume x in union F2 ; :: thesis: x in union Fu

then consider X being set such that

A10: x in X and

A11: X in F2 by TARSKI:def 4;

ex B being Subset of GX st

( X = B & ex B2 being Subset of GX st

( B2 in Fu & B c= B2 & B is a_component ) ) by A11;

hence x in union Fu by A10, TARSKI:def 4; :: thesis: verum

hence union Fu is a_union_of_components of GX by A1, Def2; :: thesis: verum