let NTX be NTopSpace; :: thesis: for O being open Subset of NTX holds O is open Subset of (NTop2Top NTX)
let O be open Subset of NTX; :: thesis: O is open Subset of (NTop2Top NTX)
O in { OO where OO is open Subset of NTX : verum } ;
then O in Family_open_set NTX by FINTOPO7:def 11;
then O in the topology of (NTop2Top NTX) by FINTOPO7:def 16;
hence O is open Subset of (NTop2Top NTX) by PRE_TOPC:def 2; :: thesis: verum