set P = PrefSpace A;
set a = the Element of A;
the ToleranceRel of (PrefSpace A) = {[ the Element of A, the Element of A]} by ZFMISC_1:132
.= id { the Element of A} by SYSREL:13
.= id the carrier of (PrefSpace A) by ZFMISC_1:132 ;
hence PrefSpace A is total ; :: thesis: verum