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

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