let n be Nat; :: thesis: for f being FinSequence of (TOP-REAL n) st L~ f <> {} holds
2 <= len f
let f be FinSequence of (TOP-REAL n); :: thesis: ( L~ f <> {} implies 2 <= len f )
assume L~ f <> {} ; :: thesis: 2 <= len f
then ( len f <> 0 & len f <> 1 ) by TOPREAL1:22;
then len f > 1 by NAT_1:25;
then len f >= 1 + 1 by NAT_1:13;
hence 2 <= len f ; :: thesis: verum