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 F' being Subset-Family of X such that
A1: for A being Subset of X holds
( A in F' iff ( A is open & A is closed & x in A ) ) and
A2: qComponent_of x = meet F' by Def7;
A3: F' <> {} by A1, Th28;
for B1 being set st B1 in F' holds
Component_of x c= B1

proof

let B1 be set ; :: thesis: ( B1 in F' implies Component_of x c= B1 )
assume A4: B1 in F' ; :: thesis: Component_of x c= B1
then reconsider B = B1 as Subset of X ;
A5: ( B is open & B is closed & x in B ) by A1, A4;
set S = Component_of x;
A6: [#] X = B \/ (B ` ) by PRE_TOPC:18;
A7: Component_of x = (Component_of x) /\ ([#] X) by XBOOLE_1:28
.= ((Component_of x) /\ B) \/ ((Component_of x) /\ (B ` )) by A6, XBOOLE_1:23 ;
( Cl B = B & B ` is closed ) by A5, PRE_TOPC:52, TOPS_1:30;
then ( Cl B = B & Cl (B ` ) = B ` ) by PRE_TOPC:52;
then ( Cl B misses B ` & B misses Cl (B ` ) ) by XBOOLE_1:79;
then A8: B,B ` are_separated by CONNSP_1:def 1;
A9: x in Component_of x by CONNSP_1:40;
( (Component_of x) /\ B c= B & (Component_of x) /\ (B ` ) c= B ` ) by XBOOLE_1:17;
then A10: (Component_of x) /\ B,(Component_of x) /\ (B ` ) are_separated by A8, CONNSP_1:8;
Component_of x is connected by CONNSP_1:41;
then ( (Component_of x) /\ B = {} X or (Component_of x) /\ (B ` ) = {} X ) by A7, A10, CONNSP_1:16;
then Component_of x misses B ` by A5, A9, XBOOLE_0:def 4, XBOOLE_0:def 7;
then Component_of x c= (B ` ) ` by SUBSET_1:43;
hence Component_of x c= B1 ; :: thesis: verum

end;

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