theorem Th21: :: RFUNCT_4:21

for x0 being Real
for f being PartFunc of REAL,REAL st x0 in dom f holds
( ( f is_upper_semicontinuous_in x0 & f is_lower_semicontinuous_in x0 ) iff f is_continuous_in x0 )