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