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

( A in F iff A is a_component ) ) holds

F is Cover of GX

let F be Subset-Family of GX; :: thesis: ( ( for A being Subset of GX holds

( A in F iff A is a_component ) ) implies F is Cover of GX )

assume A1: for A being Subset of GX holds

( A in F iff A is a_component ) ; :: thesis: F is Cover of GX

hence F is Cover of GX by SETFAM_1:def 11; :: thesis: verum

( A in F iff A is a_component ) ) holds

F is Cover of GX

let F be Subset-Family of GX; :: thesis: ( ( for A being Subset of GX holds

( A in F iff A is a_component ) ) implies F is Cover of GX )

assume A1: for A being Subset of GX holds

( A in F iff A is a_component ) ; :: thesis: F is Cover of GX

now :: thesis: for x being object st x in [#] GX holds

x in union F

then
[#] GX c= union F
by TARSKI:def 3;x in union F

let x be object ; :: thesis: ( x in [#] GX implies x in union F )

assume x in [#] GX ; :: thesis: x in union F

then reconsider y = x as Point of GX ;

Component_of y is a_component by Th40;

then Component_of y in F by A1;

then A2: Component_of y c= union F by ZFMISC_1:74;

y in Component_of y by Th38;

hence x in union F by A2; :: thesis: verum

end;assume x in [#] GX ; :: thesis: x in union F

then reconsider y = x as Point of GX ;

Component_of y is a_component by Th40;

then Component_of y in F by A1;

then A2: Component_of y c= union F by ZFMISC_1:74;

y in Component_of y by Th38;

hence x in union F by A2; :: thesis: verum

hence F is Cover of GX by SETFAM_1:def 11; :: thesis: verum