theorem Th9: :: JGRAPH_2:9

for B being Subset of (TOP-REAL 2) st B = {(0. (TOP-REAL 2))} holds
( B ` <> {} & the carrier of (TOP-REAL 2) \ B <> {} )