:: deftheorem Def33 defines <= QC_LANG1:def 33 :
for A being QC-alphabet
for s, t being QC-symbol of A holds
( ( s in NAT & t in NAT implies ( s <= t iff ex n, m being Nat st
( n = s & m = t & n <= m ) ) ) & ( not s in NAT & not t in NAT implies ( s <= t iff [s,t] in the Relation of A ) ) & ( ( not s in NAT or not t in NAT ) & ( s in NAT or t in NAT ) implies ( s <= t iff t in NAT ) ) );