reconsider AA = {KurExSet,(KurExSet `)} as Subset-Family of R^1 by MEASURE1:2;
AA is with_proper_subsets

proof

assume A1: the carrier of R^1 in AA ; :: according to SETFAM_1:def 12 :: thesis: contradiction

per cases ( REAL = KurExSet or REAL = KurExSet ` ) by A1, TARSKI:def 2, TOPMETR:17;

suppose REAL = KurExSet ; :: thesis: contradiction

then [#] R^1 = KurExSet by TOPMETR:17;
hence contradiction ; :: thesis: verum

end;

suppose REAL = KurExSet ` ; :: thesis: contradiction

then [#] R^1 = KurExSet ` by TOPMETR:17;
hence contradiction by TOPS_1:3; :: thesis: verum

end;

end;

end;

then A2: AA \/ (Kurat14ClPart KurExSet) is with_proper_subsets by SETFAM_1:48;
Kurat14Set KurExSet = (AA \/ (Kurat14ClPart KurExSet)) \/ (Kurat14OpPart KurExSet) by Lm2;
hence Kurat14Set KurExSet is with_proper_subsets by A2, SETFAM_1:48; :: thesis: verum