let Al be QC-alphabet ; :: thesis: for f being FinSequence of CQC-WFF Al st len f > 1 holds
len (Ant f) > 0
let f be FinSequence of CQC-WFF Al; :: 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