theorem Th9: :: GOBOARD2:9

for f being FinSequence of (TOP-REAL 2) st f <> {} holds
X_axis f <> {}