let C be Category; :: thesis: for a, b being Element of C st Hom (a,b) <> {} holds
ex m being Morphism of a,b st m in Hom (a,b)
let a, b be Element of C; :: thesis: ( Hom (a,b) <> {} implies ex m being Morphism of a,b st m in Hom (a,b) )
assume Hom (a,b) <> {} ; :: thesis: ex m being Morphism of a,b st m in Hom (a,b)
then consider m being object such that
A1: m in Hom (a,b) by XBOOLE_0:def 1;
reconsider m = m as Morphism of a,b by A1, Def3;
take m ; :: thesis: m in Hom (a,b)
thus m in Hom (a,b) by A1; :: thesis: verum