let f be FinSequence of CQC-WFF ; :: thesis: ( len f > 1 implies len (Ant f) > 0 )
assume len f > 1 ; :: thesis: len (Ant f) > 0
then (len (Ant f)) + 1 > 1 by Th2;
hence len (Ant f) > 0 by NAT_1:13; :: thesis: verum