theorem Th30: :: CALCUL_1:30

for Al being QC-alphabet
for f being FinSequence of CQC-WFF Al holds Ant (f ^ <*(VERUM Al)*>) |= Suc (f ^ <*(VERUM Al)*>)