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 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 GX such that
A3: for B being Subset of GX st B in F holds
B is a_component 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 GX by A6;
B2 = Component_of p by A3, A5, A6, CONNSP_1:41;
hence Component_of p c= A by A4, A6, ZFMISC_1:74; :: thesis: verum