reconsider R1 = {[a,a],[b,b]}, R2 = {[a,b],[b,a]} as Relation of A ;
take PreferenceStr(# A,({} (A,A)),R1,R2 #) ; :: thesis: ( the carrier of PreferenceStr(# A,({} (A,A)),R1,R2 #) = A & the PrefRel of PreferenceStr(# A,({} (A,A)),R1,R2 #) = {} & the ToleranceRel of PreferenceStr(# A,({} (A,A)),R1,R2 #) = {[a,a],[b,b]} & the InternalRel of PreferenceStr(# A,({} (A,A)),R1,R2 #) = {[a,b],[b,a]} )
thus ( the carrier of PreferenceStr(# A,({} (A,A)),R1,R2 #) = A & the PrefRel of PreferenceStr(# A,({} (A,A)),R1,R2 #) = {} & the ToleranceRel of PreferenceStr(# A,({} (A,A)),R1,R2 #) = {[a,a],[b,b]} & the InternalRel of PreferenceStr(# A,({} (A,A)),R1,R2 #) = {[a,b],[b,a]} ) ; :: thesis: verum