:: deftheorem defines is_formal_provable_from CALCUL_1:def 10 :
for Al being QC-alphabet
for p being Element of CQC-WFF Al
for X being Subset of (CQC-WFF Al) holds
( p is_formal_provable_from X iff ex f being FinSequence of CQC-WFF Al st
( rng (Ant f) c= X & Suc f = p & |- f ) );