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