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

proof

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;

then reconsider F2 = { B where B is Subset of GX : ex B2 being Subset of GX st
( 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

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 A2: for A being Subset of GX st A in Fu holds
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

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;

union F2 c= union Fu

proof

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;

then union Fu = union F2 by A3;
hence union Fu is a_union_of_components of GX by A1, Def2; :: thesis: verum