for Z being open Subset of REAL
for A being non empty closed_interval Subset of REAL st not 0 in Z & A c= Z holds
((id Z) ^) | A is continuous