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

proof

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;

F9 <> {} by A1, Th22;
hence Component_of x c= qComponent_of x by A2, A3, SETFAM_1:5; :: thesis: verum