let V be non empty set ; :: thesis: for a being Object of (Ens V) st {} in V & a is initial holds
a = {}
let a be Object of (Ens V); :: thesis: ( {} in V & a is initial implies a = {} )
assume {} in V ; :: thesis: ( not a is initial or a = {} )
then reconsider B = {} as Element of V ;
set b = @ B;
assume a is initial ; :: thesis: a = {}
then Hom (a,(@ B)) <> {} ;
then Funcs ((@ a),(@ (@ B))) <> {} by Lm6;
hence a = {} ; :: thesis: verum