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

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