:: deftheorem Def4 defines Impl CALCUL_2:def 4 :
for Al being QC-alphabet
for f being FinSequence of CQC-WFF Al st 1 <= len f holds
for b₃ being Element of CQC-WFF Al holds
( b₃ = Impl f iff ex F being FinSequence of CQC-WFF Al st
( b₃ = F . (len f) & len F = len f & ( F . 1 = Begin f or len f = 0 ) & ( for n being Nat st 1 <= n & n < len f holds
ex p, q being Element of CQC-WFF Al st
( p = f . (n + 1) & q = F . n & F . (n + 1) = p => q ) ) ) );