theorem :: ISOMICHI:26

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