Kurat14Set KurExSet = ({KurExSet ,(KurExSet ` )} \/ (Kurat14ClPart KurExSet )) \/ (Kurat14OpPart KurExSet ) by Lm2;
then A1: {KurExSet ,(KurExSet ` )} \/ (Kurat14ClPart KurExSet ) c= Kurat14Set KurExSet by XBOOLE_1:7;
Kurat14ClPart KurExSet c= {KurExSet ,(KurExSet ` )} \/ (Kurat14ClPart KurExSet ) by XBOOLE_1:7;
hence Kurat14ClPart KurExSet is with_non-empty_elements by A1, Th59, XBOOLE_1:1; :: thesis: verum