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

now :: thesis: for x being object st x in [#] GX holds
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;

then [#] GX c= union F by TARSKI:def 3;
hence F is Cover of GX by SETFAM_1:def 11; :: thesis: verum