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