:: deftheorem defines total PREFER_1:def 14 :
for P being PreferenceStr holds
( P is total iff ( the PrefRel of P is transitive & the ToleranceRel of P = id the carrier of P & the InternalRel of P = {} ) );