let NTX be NTopSpace; :: thesis: for A being closed Subset of NTX holds Cl A = A
let A be closed Subset of NTX; :: thesis: Cl A = A
reconsider NA = ([#] NTX) \ A as open Subset of NTX by Def9;
Cl A = ([#] NTX) /\ (Cl A) by XBOOLE_1:28
.= ([#] NTX) \ (([#] NTX) \ (Cl A)) by XBOOLE_1:48
.= ([#] NTX) \ (Int NA) by Lm14
.= ([#] NTX) \ NA by Lm19
.= ([#] NTX) /\ A by XBOOLE_1:48
.= A by XBOOLE_1:28 ;
hence Cl A = A ; :: thesis: verum