theorem :: RFUNCT_4:22

for X being set
for f being PartFunc of REAL,REAL st X c= dom f holds
( ( f is_upper_semicontinuous_on X & f is_lower_semicontinuous_on X ) iff f | X is continuous )