:: deftheorem defines a_proof CALCUL_1:def 8 :
for Al being QC-alphabet
for PR being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] holds
( PR is a_proof iff ( PR <> {} & ( for n being Nat st 1 <= n & n <= len PR holds
PR,n is_a_correct_step ) ) );