let y, x be set ; for a, b being Object of (1Cat x,y) holds Hom a,b = {y}
let a, b be Object of (1Cat x,y); Hom a,b = {y}
thus
Hom a,b c= {y}
; XBOOLE_0:def 10 {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; verum