let NTX be NTopSpace; :: thesis: ( [#] NTX is open & {} NTX is open )
reconsider X = NTop2Top NTX as non empty TopSpace ;
now :: thesis: ( [#] NTX = the carrier of (NTop2Top NTX) & {} NTX = {} (NTop2Top NTX) & the carrier of (NTop2Top NTX) is open Subset of (NTop2Top NTX) )
thus [#] NTX = the carrier of (NTop2Top NTX) by FINTOPO7:def 16; :: thesis: ( {} NTX = {} (NTop2Top NTX) & the carrier of (NTop2Top NTX) is open Subset of (NTop2Top NTX) )
thus {} NTX = {} (NTop2Top NTX) ; :: thesis: the carrier of (NTop2Top NTX) is open Subset of (NTop2Top NTX)
the carrier of (NTop2Top NTX) in the topology of (NTop2Top NTX) by PRE_TOPC:def 1;
hence the carrier of (NTop2Top NTX) is open Subset of (NTop2Top NTX) by PRE_TOPC:def 2; :: thesis: verum
end;
then reconsider S1 = [#] NTX, S2 = {} NTX as open Subset of X ;
Top2NTop X = NTX by FINTOPO7:25;
then ( S1 is open Subset of NTX & S2 is open Subset of NTX ) by Lm1;
hence ( [#] NTX is open & {} NTX is open ) ; :: thesis: verum