reconsider R1 = P /\ ((P ~) `), R2 = P /\ (P ~), R3 = Aux P as Relation of X ;
take PreferenceStr(# X,R1,R2,R3 #) ; :: thesis: ( the carrier of PreferenceStr(# X,R1,R2,R3 #) = X & the PrefRel of PreferenceStr(# X,R1,R2,R3 #) = P /\ ((P ~) `) & the ToleranceRel of PreferenceStr(# X,R1,R2,R3 #) = P /\ (P ~) & the InternalRel of PreferenceStr(# X,R1,R2,R3 #) = Aux P )
thus ( the carrier of PreferenceStr(# X,R1,R2,R3 #) = X & the PrefRel of PreferenceStr(# X,R1,R2,R3 #) = P /\ ((P ~) `) & the ToleranceRel of PreferenceStr(# X,R1,R2,R3 #) = P /\ (P ~) & the InternalRel of PreferenceStr(# X,R1,R2,R3 #) = Aux P ) ; :: thesis: verum