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:
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:
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 & () /\ (B `) c= B ` ) by XBOOLE_1:17;
Cl B = B by ;
then Cl B misses B ` by XBOOLE_1:79;
then B,B ` are_separated by ;
then A10: (Component_of x) /\ B,() /\ (B `) are_separated by ;
A11: [#] X = B \/ (B `) by PRE_TOPC:2;
Component_of x = () /\ ([#] X) by XBOOLE_1:28
.= (() /\ B) \/ (() /\ (B `)) by ;
then ( (Component_of x) /\ B = {} X or () /\ (B `) = {} X ) by ;
then Component_of x misses B ` by ;
then Component_of x c= (B `) ` by SUBSET_1:23;
hence Component_of x c= B1 ; :: thesis: verum
end;
F9 <> {} by ;
hence Component_of x c= qComponent_of x by ; :: thesis: verum