let f be non trivial FinSequence; :: thesis: 1 < len f
1 + 1 <= len f by NAT_D:60;
hence 1 < len f by NAT_1:13; :: thesis: verum