let n be Nat; :: thesis: for f being FinSequence of (TOP-REAL n) st len f >= 2 holds
L~ f <> {}
let f be FinSequence of (TOP-REAL n); :: thesis: ( len f >= 2 implies L~ f <> {} )
assume A1: len f >= 2 ; :: thesis: L~ f <> {}
then not len f = 1 ;
hence L~ f <> {} by A1, Th22; :: thesis: verum