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;