theorem Th8: :: PSCOMP_1:8

for T being TopStruct
for f being RealMap of T holds
( f is continuous iff for Y being Subset of REAL st Y is open holds
f " Y is open )