let A be trivial set ; :: thesis: IdPrefSpace A = PrefSpace A

per cases ( not A is empty or A is empty ) ;

suppose A0: not A is empty ; :: 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) by Lemma1C, A0 ;
the InternalRel of (IdPrefSpace A) = the InternalRel of (PrefSpace A) by Def5;
hence IdPrefSpace A = PrefSpace A by A1, A2, Def5; :: thesis: verum

end;

suppose A is empty ; :: thesis: IdPrefSpace A = PrefSpace A

hence IdPrefSpace A = PrefSpace A by ZZ; :: thesis: verum

end;

end;