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

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