let C be Category; for O being non empty Subset of the carrier of C holds union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } is non empty Subset of the carrier' of C
let O be non empty Subset of the carrier of C; union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } is non empty Subset of the carrier' of C
set H = { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ;
set M = union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } ;
A1:
union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } c= the carrier' of C
hence
union { (Hom (a,b)) where a, b is Object of C : ( a in O & b in O ) } is non empty Subset of the carrier' of C
by A1; verum