theorem Th23: :: TOPREAL1:23

for n being Nat
for f being FinSequence of (TOP-REAL n) st len f >= 2 holds
L~ f <> {}