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