set A = KurExSet ;
assume {KurExSet ,(KurExSet ` )} meets Kurat14OpPart KurExSet ; :: thesis: contradiction
then consider x being set such that
A1: ( x in {KurExSet ,(KurExSet ` )} & x in Kurat14OpPart KurExSet ) by XBOOLE_0:3;
reconsider x = x as Subset of R^1 by A1;
A2: x is open by A1, TOPS_2:def 1;
( x = KurExSet or x = KurExSet ` ) by A1, TARSKI:def 2;
then x ` = KurExSet by A1, TOPS_2:def 1;
hence contradiction by A2; :: thesis: verum