set A = the non empty trivial set ;
reconsider P = PrefSpace the non empty trivial set as non empty PreferenceSpace ;
take P ; :: thesis: P is total
thus P is total ; :: thesis: verum