theorem Th3: :: FINANCE5:10

for k being Real holds
( ].k,+infty.] is Element of Ext_Borel_Sets & [.-infty,k.] is Element of Ext_Borel_Sets )