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