let X be non empty TopSpace; :: thesis: for X1 being non empty SubSpace of X
for x being Point of X
for x1 being Point of X1 st x = x1 holds
Component_of x1 c= Component_of x
let X1 be non empty SubSpace of X; :: thesis: for x being Point of X
for x1 being Point of X1 st x = x1 holds
Component_of x1 c= Component_of x
let x be Point of X; :: thesis: for x1 being Point of X1 st x = x1 holds
Component_of x1 c= Component_of x
let x1 be Point of X1; :: thesis: ( x = x1 implies Component_of x1 c= Component_of x )
consider F being Subset-Family of X such that
A1: for A being Subset of X holds
( A in F iff ( A is connected & x in A ) ) and
A2: union F = Component_of x by CONNSP_1:def 7;
reconsider Z = Component_of x1 as Subset of X by PRE_TOPC:11;
A3: ( x1 in Z & Z is connected ) by CONNSP_1:23, CONNSP_1:38;
assume x = x1 ; :: thesis: Component_of x1 c= Component_of x
then Z in F by A1, A3;
hence Component_of x1 c= Component_of x by A2, ZFMISC_1:74; :: thesis: verum