let T be TopStruct ; :: thesis: for A being Subset of T
for p being set st p in the carrier of T holds
( p in Cl A iff for C being Subset of T st C is closed & A c= C holds
p in C )
let A be Subset of T; :: thesis: for p being set st p in the carrier of T holds
( p in Cl A iff for C being Subset of T st C is closed & A c= C holds
p in C )
let p be set ; :: thesis: ( p in the carrier of T implies ( p in Cl A iff for C being Subset of T st C is closed & A c= C holds
p in C ) )
assume A1: p in the carrier of T ; :: thesis: ( p in Cl A iff for C being Subset of T st C is closed & A c= C holds
p in C )

A2: now :: thesis: ( ( for C being Subset of T st C is closed & A c= C holds
p in C ) implies p in Cl A )

assume A3: for C being Subset of T st C is closed & A c= C holds
p in C ; :: thesis: p in Cl A
for G being Subset of T st G is open & p in G holds
A meets G

proof

let G be Subset of T; :: thesis: ( G is open & p in G implies A meets G )
assume A4: G is open ; :: thesis: ( not p in G or A meets G )
([#] T) \ (([#] T) \ G) = G by Th3;
then ([#] T) \ G is closed by A4;
then ( A c= G ` implies p in ([#] T) \ G ) by A3;
hence ( not p in G or A meets G ) by SUBSET_1:23, XBOOLE_0:def 5; :: thesis: verum

end;

hence p in Cl A by A1, Def7; :: thesis: verum

end;

now :: thesis: ( p in Cl A implies for C being Subset of T st C is closed & A c= C holds
p in C )

assume A5: p in Cl A ; :: thesis: for C being Subset of T st C is closed & A c= C holds
p in C
let C be Subset of T; :: thesis: ( C is closed & A c= C implies p in C )
assume C is closed ; :: thesis: ( A c= C implies p in C )
then ([#] T) \ C is open ;
then ( p in ([#] T) \ C implies A meets ([#] T) \ C ) by A5, Def7;
then ( not A c= (([#] T) \ C) ` or p in C or not p in [#] T ) by SUBSET_1:23, XBOOLE_0:def 5;
hence ( A c= C implies p in C ) by A1, Th3; :: thesis: verum

end;

hence ( p in Cl A iff for C being Subset of T st C is closed & A c= C holds
p in C ) by A2; :: thesis: verum