:: deftheorem defines -one_in QC_LANG1:def 41 :
for A being QC-alphabet
for Y being set holds
( ( Y is non empty Subset of (QC-symbols A) implies A -one_in Y = the Element of Y ) & ( Y is not non empty Subset of (QC-symbols A) implies A -one_in Y = 0 A ) );