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

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

per cases by A1, TARSKI:def 2, TOPMETR:17;

suppose REAL = KurExSet ; :: thesis:

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

end;

suppose REAL = KurExSet ` ; :: thesis:

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

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: