let y, x be set ; :: thesis: for a, b being Object of (1Cat x,y) holds Hom a,b = {y}
let a, b be Object of (1Cat x,y); :: thesis: Hom a,b = {y}
thus
Hom a,b c= {y}
; :: according to XBOOLE_0:def 10 :: thesis: {y} c= Hom a,b
y is Morphism of (1Cat x,y)
by TARSKI:def 1;
then
y in Hom a,b
by CAT_1:36;
hence
{y} c= Hom a,b
by ZFMISC_1:37; :: thesis: verum