let X be non empty TopSpace; :: thesis: for x being Point of X holds Component_of x c= qComponent_of x

let x be Point of X; :: thesis: Component_of x c= qComponent_of x

consider F9 being Subset-Family of X such that

A1: for A being Subset of X holds

( A in F9 iff ( A is open & A is closed & x in A ) ) and

A2: qComponent_of x = meet F9 by Def7;

A3: for B1 being set st B1 in F9 holds

Component_of x c= B1

hence Component_of x c= qComponent_of x by A2, A3, SETFAM_1:5; :: thesis: verum

let x be Point of X; :: thesis: Component_of x c= qComponent_of x

consider F9 being Subset-Family of X such that

A1: for A being Subset of X holds

( A in F9 iff ( A is open & A is closed & x in A ) ) and

A2: qComponent_of x = meet F9 by Def7;

A3: for B1 being set st B1 in F9 holds

Component_of x c= B1

proof

F9 <> {}
by A1, Th22;
set S = Component_of x;

let B1 be set ; :: thesis: ( B1 in F9 implies Component_of x c= B1 )

A4: x in Component_of x by CONNSP_1:38;

assume A5: B1 in F9 ; :: thesis: Component_of x c= B1

then reconsider B = B1 as Subset of X ;

A6: x in B by A1, A5;

A7: ( B is open & B is closed ) by A1, A5;

then B ` is closed ;

then Cl (B `) = B ` by PRE_TOPC:22;

then A8: B misses Cl (B `) by XBOOLE_1:79;

A9: ( (Component_of x) /\ B c= B & (Component_of x) /\ (B `) c= B ` ) by XBOOLE_1:17;

Cl B = B by A7, PRE_TOPC:22;

then Cl B misses B ` by XBOOLE_1:79;

then B,B ` are_separated by A8, CONNSP_1:def 1;

then A10: (Component_of x) /\ B,(Component_of x) /\ (B `) are_separated by A9, CONNSP_1:7;

A11: [#] X = B \/ (B `) by PRE_TOPC:2;

Component_of x = (Component_of x) /\ ([#] X) by XBOOLE_1:28

.= ((Component_of x) /\ B) \/ ((Component_of x) /\ (B `)) by A11, XBOOLE_1:23 ;

then ( (Component_of x) /\ B = {} X or (Component_of x) /\ (B `) = {} X ) by A10, CONNSP_1:15;

then Component_of x misses B ` by A6, A4, XBOOLE_0:def 4, XBOOLE_0:def 7;

then Component_of x c= (B `) ` by SUBSET_1:23;

hence Component_of x c= B1 ; :: thesis: verum

end;let B1 be set ; :: thesis: ( B1 in F9 implies Component_of x c= B1 )

A4: x in Component_of x by CONNSP_1:38;

assume A5: B1 in F9 ; :: thesis: Component_of x c= B1

then reconsider B = B1 as Subset of X ;

A6: x in B by A1, A5;

A7: ( B is open & B is closed ) by A1, A5;

then B ` is closed ;

then Cl (B `) = B ` by PRE_TOPC:22;

then A8: B misses Cl (B `) by XBOOLE_1:79;

A9: ( (Component_of x) /\ B c= B & (Component_of x) /\ (B `) c= B ` ) by XBOOLE_1:17;

Cl B = B by A7, PRE_TOPC:22;

then Cl B misses B ` by XBOOLE_1:79;

then B,B ` are_separated by A8, CONNSP_1:def 1;

then A10: (Component_of x) /\ B,(Component_of x) /\ (B `) are_separated by A9, CONNSP_1:7;

A11: [#] X = B \/ (B `) by PRE_TOPC:2;

Component_of x = (Component_of x) /\ ([#] X) by XBOOLE_1:28

.= ((Component_of x) /\ B) \/ ((Component_of x) /\ (B `)) by A11, XBOOLE_1:23 ;

then ( (Component_of x) /\ B = {} X or (Component_of x) /\ (B `) = {} X ) by A10, CONNSP_1:15;

then Component_of x misses B ` by A6, A4, XBOOLE_0:def 4, XBOOLE_0:def 7;

then Component_of x c= (B `) ` by SUBSET_1:23;

hence Component_of x c= B1 ; :: thesis: verum

hence Component_of x c= qComponent_of x by A2, A3, SETFAM_1:5; :: thesis: verum