let P be Subset of ; :: 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