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 )
assume A1: ( A is open & A is closed & x in A ) ; :: thesis: ( not A c= qComponent_of x or A = qComponent_of x )
assume A2: A c= qComponent_of x ; :: thesis: A = qComponent_of x
consider F being Subset-Family of X such that
A3: for A being Subset of X holds
( A in F iff ( A is open & A is closed & x in A ) ) and
A4: qComponent_of x = meet F by Def7;
A in F by A1, A3;
then qComponent_of x c= A by A4, SETFAM_1:4;
hence A = qComponent_of x by A2, XBOOLE_0:def 10; :: thesis: verum