:: deftheorem defines < QC_LANG1:def 34 :
for A being QC-alphabet
for s, t being QC-symbol of A holds
( s < t iff ( s <= t & s <> t ) );