theorem :: ISOMICHI:25

for A being Subset of R^1
for a being Real st A = ].-infty,a.] holds
Int A = ].-infty,a.[