theorem Th17: :: KURATO_1:17

Cl (KurExSet `) = ].-infty,4.] \/ {5} by Th16, BORSUK_5:67;