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