theorem :: PREFER_1:55

for P being non empty PreferenceSpace holds
( P is total iff CharRel P is connected Order of the carrier of P )