let NTX be NTopSpace; :: thesis: for F being closed Subset of NTX holds F is closed Subset of (NTop2Top NTX)
let F be closed Subset of NTX; :: thesis: F is closed Subset of (NTop2Top NTX)
reconsider TX = NTop2Top NTX as non empty TopSpace ;
A1: [#] NTX = [#] TX by FINTOPO7:def 16;
reconsider O = ([#] NTX) \ F as Subset of NTX by XBOOLE_1:36;
reconsider O = O as open Subset of NTX by Lm8;
reconsider NO = O as open Subset of TX by Lm9;
reconsider NF = ([#] TX) \ NO as Subset of TX by XBOOLE_1:36;
A2: ([#] TX) \ NF = ([#] TX) /\ NO by XBOOLE_1:48
.= NO by XBOOLE_1:28 ;
([#] TX) \ NO = ([#] TX) /\ F by A1, XBOOLE_1:48
.= F by A1, XBOOLE_1:28 ;
hence F is closed Subset of (NTop2Top NTX) by A2, PRE_TOPC:def 3; :: thesis: verum