let NTX be NTopSpace; :: thesis: for A being Subset of NTX st Cl A = A holds
A is closed Subset of NTX
let A be Subset of NTX; :: thesis: ( Cl A = A implies A is closed Subset of NTX )
assume A1: Cl A = A ; :: thesis: A is closed Subset of NTX
reconsider NA = ([#] NTX) \ A as Subset of NTX by XBOOLE_1:36;
A2: Cl A = ([#] NTX) /\ (Cl A) by XBOOLE_1:28
.= ([#] NTX) \ (([#] NTX) \ (Cl A)) by XBOOLE_1:48
.= ([#] NTX) \ (Int NA) by Lm14 ;
Int NA = (Int NA) /\ ([#] NTX) by XBOOLE_1:28
.= NA by A1, A2, XBOOLE_1:48 ;
then A is closed ;
hence A is closed Subset of NTX ; :: thesis: verum