let A be non empty trivial set ; :: thesis: the ToleranceRel of (PrefSpace A) = id the carrier of (PrefSpace A)
set a = the Element of A;
set X = PrefSpace A;
reconsider C = { the Element of A} as Subset of A ;
the ToleranceRel of (PrefSpace A) = {[ the Element of A, the Element of A]} by ZFMISC_1:132;
then the ToleranceRel of (PrefSpace A) = id { the Element of A} by SYSREL:13;
hence the ToleranceRel of (PrefSpace A) = id the carrier of (PrefSpace A) by ZFMISC_1:132; :: thesis: verum