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

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