let GX be non empty TopSpace; :: thesis: for A being Subset of GX
for p being Point of GX st p in A & A is a_union_of_components of GX holds
Component_of p c= A
let A be Subset of GX; :: thesis: for p being Point of GX st p in A & A is a_union_of_components of GX holds
Component_of p c= A
let p be Point of GX; :: thesis: ( p in A & A is a_union_of_components of GX implies Component_of p c= A )
assume A1: ( p in A & A is a_union_of_components of GX ) ; :: thesis: Component_of p c= A
then consider F being Subset-Family of GX such that
A2: ( ( for B being Subset of GX st B in F holds
B is_a_component_of GX ) & A = union F ) by Def2;
consider X being set such that
A3: ( p in X & X in F ) by A1, A2, TARSKI:def 4;
reconsider B2 = X as Subset of GX by A3;
B2 = Component_of p by A2, A3, CONNSP_1:44;
hence Component_of p c= A by A2, A3, ZFMISC_1:92; :: thesis: verum