let X be non empty TopSpace; :: thesis: for x being Point of X
for A being Subset of X st A is open & A is closed & x in A & A c= qComponent_of x holds
A = qComponent_of x
let x be Point of X; :: thesis: for A being Subset of X st A is open & A is closed & x in A & A c= qComponent_of x holds
A = qComponent_of x
let A be Subset of X; :: thesis: ( A is open & A is closed & x in A & A c= qComponent_of x implies A = 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;
assume ( A is open & A is closed & x in A ) ; :: thesis: ( not A c= qComponent_of x or A = qComponent_of x )
then A in F by A1;
then A3: qComponent_of x c= A by A2, SETFAM_1:3;
assume A c= qComponent_of x ; :: thesis: A = qComponent_of x
hence A = qComponent_of x by A3, XBOOLE_0:def 10; :: thesis: verum