let NTX be NTopSpace; :: thesis: for A being closed Subset of NTX holds A is closed Subset of (NTop2Top NTX)
let A be closed Subset of NTX; :: thesis: A is closed Subset of (NTop2Top NTX)
reconsider T = NTop2Top NTX as TopSpace ;
([#] NTX) \ A is open Subset of NTX by Def9;
then ([#] NTX) \ A is open Subset of (NTop2Top NTX) by Lm9;
then reconsider A9 = ([#] T) \ A as open Subset of T by FINTOPO7:def 16;
( ([#] T) \ A9 = ([#] T) /\ A & A is Subset of T ) by XBOOLE_1:48, FINTOPO7:def 16;
hence A is closed Subset of (NTop2Top NTX) by PRE_TOPC:def 3; :: thesis: verum