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