let TX be non empty TopSpace; :: thesis: for F being closed Subset of TX holds F is closed Subset of (Top2NTop TX)
let F be closed Subset of TX; :: thesis: F is closed Subset of (Top2NTop TX)
set NTX = Top2NTop TX;
A1: [#] (Top2NTop TX) = [#] TX by FINTOPO7:def 15;
reconsider O = ([#] TX) \ F as open Subset of TX by PRE_TOPC:def 3;
reconsider NO = O as open Subset of (Top2NTop TX) by Lm1;
([#] (Top2NTop TX)) \ NO = ([#] (Top2NTop TX)) /\ F by A1, XBOOLE_1:48
.= F by A1, XBOOLE_1:28 ;
hence F is closed Subset of (Top2NTop TX) by Lm6, FINTOPO7:def 15; :: thesis: verum