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, Th56, XBOOLE_1:1; :: thesis: verum