let GX be non empty TopSpace; :: thesis: for A being Subset of GX

for p being Point of GX st A is connected & p in A holds

Component_of p = Component_of A

let A be Subset of GX; :: thesis: for p being Point of GX st A is connected & p in A holds

Component_of p = Component_of A

let p be Point of GX; :: thesis: ( A is connected & p in A implies Component_of p = Component_of A )

assume that

A1: A is connected and

A2: p in A ; :: thesis: Component_of p = Component_of A

( A c= Component_of A & Component_of A is a_component ) by A1, A2, Th1, Th8;

hence Component_of p = Component_of A by A2, CONNSP_1:41; :: thesis: verum

for p being Point of GX st A is connected & p in A holds

Component_of p = Component_of A

let A be Subset of GX; :: thesis: for p being Point of GX st A is connected & p in A holds

Component_of p = Component_of A

let p be Point of GX; :: thesis: ( A is connected & p in A implies Component_of p = Component_of A )

assume that

A1: A is connected and

A2: p in A ; :: thesis: Component_of p = Component_of A

( A c= Component_of A & Component_of A is a_component ) by A1, A2, Th1, Th8;

hence Component_of p = Component_of A by A2, CONNSP_1:41; :: thesis: verum