let X be non empty TopSpace; :: thesis: for x being Point of holds qComponent_of x is closed
let x be Point of ; :: thesis: qComponent_of x is closed
consider F being Subset-Family of such that
A1: for A being Subset of holds
( A in F iff ( A is open & A is closed & x in A ) ) and
A2: qComponent_of x = meet F by Def7;
for A being Subset of st A in F holds
A is closed by A1;
hence qComponent_of x is closed by A2, PRE_TOPC:44; :: thesis: verum