:: deftheorem Def17 defines QC-Sub-WFF SUBSTUT1:def 17 :
for A being QC-alphabet
for b₂ being non empty set holds
( b₂ = QC-Sub-WFF A iff ( b₂ is A -Sub-closed & ( for D being non empty set st D is A -Sub-closed holds
b₂ c= D ) ) );