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

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