assume KurExSet = KurExSet ` ; :: thesis: contradiction
then KurExSet meets KurExSet ` by XBOOLE_1:66;
hence contradiction by XBOOLE_1:79; :: thesis: verum