:: deftheorem Def3 defines Begin CALCUL_2:def 3 :
for Al being QC-alphabet
for f being FinSequence of CQC-WFF Al
for b₃ being Element of CQC-WFF Al holds
( ( 1 <= len f implies ( b₃ = Begin f iff b₃ = f . 1 ) ) & ( not 1 <= len f implies ( b₃ = Begin f iff b₃ = VERUM Al ) ) );