set C = the empty CategoryStr opp ;
for f being morphism of ( the empty CategoryStr opp) holds f is identity

proof

let f be morphism of ( the empty CategoryStr opp); :: thesis: f is identity
for f1 being morphism of ( the empty CategoryStr opp) st f |> f1 holds
f (*) f1 = f1 ;
then A1: f is left_identity ;
for f1 being morphism of ( the empty CategoryStr opp) st f1 |> f holds
f1 (*) f = f1 ;
hence f is identity by A1, Def5; :: thesis: verum

end;

hence the empty CategoryStr opp is discrete ; :: thesis: verum