:: deftheorem defines |- CALCUL_1:def 9 :
for Al being QC-alphabet
for f being FinSequence of CQC-WFF Al holds
( |- f iff ex PR being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] st
( PR is a_proof & f = (PR . (len PR)) `1 ) );