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