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