let A be empty set ; :: thesis: IdPrefSpace A = PrefSpace A
A1: the carrier of (IdPrefSpace A) = the carrier of (PrefSpace A) by Def5;
A2: the ToleranceRel of (IdPrefSpace A) = id the carrier of (PrefSpace A) by Def5
.= the ToleranceRel of (PrefSpace A) ;
the InternalRel of (IdPrefSpace A) = the InternalRel of (PrefSpace A) by Def5;
hence IdPrefSpace A = PrefSpace A by A1, A2; :: thesis: verum