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 )
assume A1: ( p in A & A is connected ) ; :: thesis: A c= Component_of p
consider F being Subset-Family of GX such that
A2: ( ( for B being Subset of GX holds
( B in F iff ( B is connected & p in B ) ) ) & union F = Component_of p ) by CONNSP_1:def 7;
A3: A in F by A1, A2;
A c= union F

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in union F )
thus ( not x in A or x in union F ) by A3, TARSKI:def 4; :: thesis: verum

end;

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