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 )
assume A1: x = x1 ; :: thesis: Component_of x1 c= Component_of x
consider F being Subset-Family of X such that
A2: for A being Subset of X holds
( A in F iff ( A is connected & x in A ) ) and
A3: union F = Component_of x by CONNSP_1:def 7;
reconsider Z = Component_of x1 as Subset of X by PRE_TOPC:39;
A4: Component_of x1 is connected by CONNSP_1:41;
A5: x1 in Z by CONNSP_1:40;
Z is connected by A4, CONNSP_1:24;
then Z in F by A1, A2, A5;
hence Component_of x1 c= Component_of x by A3, ZFMISC_1:92; :: thesis: verum