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