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 connected holds

A c= Component_of p

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

A c= Component_of p

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

consider F being Subset-Family of GX such that

A1: for B being Subset of GX holds

( B in F iff ( B is connected & p in B ) ) and

A2: union F = Component_of p by CONNSP_1:def 7;

assume ( p in A & A is connected ) ; :: thesis: A c= Component_of p

then A3: A in F by A1;

A c= union F by A3, TARSKI:def 4;

hence A c= Component_of p by A2; :: thesis: verum

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

A c= Component_of p

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

A c= Component_of p

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

consider F being Subset-Family of GX such that

A1: for B being Subset of GX holds

( B in F iff ( B is connected & p in B ) ) and

A2: union F = Component_of p by CONNSP_1:def 7;

assume ( p in A & A is connected ) ; :: thesis: A c= Component_of p

then A3: A in F by A1;

A c= union F by A3, TARSKI:def 4;

hence A c= Component_of p by A2; :: thesis: verum