let X be non empty TopSpace; :: thesis: for x being Point of X holds x in qComponent_of x
let x be Point of X; :: thesis: x in 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 A being set st A in F holds
x in A by A1;
hence x in qComponent_of x by A2, A3, SETFAM_1:def 1; :: thesis: verum