let TX be non empty TopSpace; :: thesis: for O being open Subset of TX holds O is open Subset of (Top2NTop TX)
let O be open Subset of TX; :: thesis: O is open Subset of (Top2NTop TX)
O in the topology of TX by PRE_TOPC:def 2;
then O in Family_open_set (Top2NTop TX) by FINTOPO7:def 15;
then O in { OO where OO is open Subset of (Top2NTop TX) : verum } by FINTOPO7:def 11;
then ex OO being open Subset of (Top2NTop TX) st O = OO ;
hence O is open Subset of (Top2NTop TX) ; :: thesis: verum