:: deftheorem Def5 defines PATH SUBSTUT2:def 5 :
for Al being QC-alphabet
for G, H being QC-formula of Al st G is_subformula_of H holds
for b₄ being FinSequence holds
( b₄ is PATH of G,H iff ( 1 <= len b₄ & b₄ . 1 = G & b₄ . (len b₄) = H & ( for k being Nat st 1 <= k & k < len b₄ holds
ex G1, H1 being Element of QC-WFF Al st
( b₄ . k = G1 & b₄ . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) ) );