let X be non empty TopSpace; :: thesis: for x being Point of X holds qComponent_of x is closed

let x be Point of X; :: thesis: qComponent_of x is closed

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;

for A being Subset of X st A in F holds

A is closed by A1;

hence qComponent_of x is closed by A2, PRE_TOPC:14; :: thesis: verum

let x be Point of X; :: thesis: qComponent_of x is closed

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;

for A being Subset of X st A in F holds

A is closed by A1;

hence qComponent_of x is closed by A2, PRE_TOPC:14; :: thesis: verum