theorem Th22: :: TOPREAL1:22

for n being Nat
for f being FinSequence of (TOP-REAL n) holds
( ( len f = 0 or len f = 1 ) iff L~ f = {} )