let P be Subset of R^1; :: according to TOPS_2:def 1 :: thesis: ( not P in Kurat14OpPart KurExSet or P is open )
assume P in Kurat14OpPart KurExSet ; :: thesis: P is open
hence P is open by ENUMSET1:def 4; :: thesis: verum