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