reconsider B = {1}, C = ((RAT 2,4) \/ ].4,5.[) \/ ].5,+infty .[ as Subset of R^1 by TOPMETR:24;
set A = KurExSet ;
A1:
KurExSet = {1} \/ (((RAT 2,4) \/ ].4,5.[) \/ ].5,+infty .[)
by XBOOLE_1:113;
A2:
B ` = ].-infty ,1.[ \/ ].1,+infty .[
by BORSUK_5:90;
C ` = ((].-infty ,2.] \/ (IRRAT 2,4)) \/ {4}) \/ {5}
by BORSUK_5:89;
hence
KurExSet ` = (((].-infty ,1.[ \/ ].1,2.]) \/ (IRRAT 2,4)) \/ {4}) \/ {5}
by A1, A2, BORSUK_5:92, XBOOLE_1:53; :: thesis: verum