:: deftheorem Def35 defines min QC_LANG1:def 35 :
for A being QC-alphabet
for Y being non empty Subset of (QC-symbols A)
for b₃ being QC-symbol of A holds
( b₃ = min Y iff ( b₃ in Y & ( for t being QC-symbol of A st t in Y holds
b₃ <= t ) ) );