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