let C be category; :: thesis: AllCoretr C is non empty subcategory of AllMono C
the carrier of (AllCoretr C) = the carrier of C by Def4;
then A1: the carrier of (AllCoretr C) c= the carrier of (AllMono C) by Def1;
the Arrows of (AllCoretr C) cc= the Arrows of (AllMono C)

proof

thus [: the carrier of (AllCoretr C), the carrier of (AllCoretr C):] c= [: the carrier of (AllMono C), the carrier of (AllMono C):] by A1, ZFMISC_1:96; :: according to ALTCAT_2:def 2 :: thesis: for b₁ being set holds
( not b₁ in [: the carrier of (AllCoretr C), the carrier of (AllCoretr C):] or the Arrows of (AllCoretr C) . b₁ c= the Arrows of (AllMono C) . b₁ )
let i be set ; :: thesis: ( not i in [: the carrier of (AllCoretr C), the carrier of (AllCoretr C):] or the Arrows of (AllCoretr C) . i c= the Arrows of (AllMono C) . i )
assume A2: i in [: the carrier of (AllCoretr C), the carrier of (AllCoretr C):] ; :: thesis: the Arrows of (AllCoretr C) . i c= the Arrows of (AllMono C) . i
then consider o1, o2 being object such that
A3: ( o1 in the carrier of (AllCoretr C) & o2 in the carrier of (AllCoretr C) ) and
A4: i = [o1,o2] by ZFMISC_1:84;
reconsider o1 = o1, o2 = o2 as Object of C by A3, Def4;
let m be object ; :: according to TARSKI:def 3 :: thesis: ( not m in the Arrows of (AllCoretr C) . i or m in the Arrows of (AllMono C) . i )
assume A5: m in the Arrows of (AllCoretr C) . i ; :: thesis: m in the Arrows of (AllMono C) . i
the Arrows of (AllCoretr C) cc= the Arrows of C by Def4;
then the Arrows of (AllCoretr C) . [o1,o2] c= the Arrows of C . (o1,o2) by A2, A4;
then reconsider m1 = m as Morphism of o1,o2 by A4, A5;
m in the Arrows of (AllCoretr C) . (o1,o2) by A4, A5;
then A6: m1 is coretraction by Def4;
A7: m1 in the Arrows of (AllCoretr C) . (o1,o2) by A4, A5;
then A8: <^o1,o2^> <> {} by Def4;
<^o2,o1^> <> {} by A7, Def4;
then m1 is mono by A8, A6, ALTCAT_3:16;
then m in the Arrows of (AllMono C) . (o1,o2) by A8, Def1;
hence m in the Arrows of (AllMono C) . i by A4; :: thesis: verum

end;

then reconsider A = AllCoretr C as non empty with_units SubCatStr of AllMono C by A1, ALTCAT_2:24;

now :: thesis: for o being Object of A
for o1 being Object of (AllMono C) st o = o1 holds
idm o1 in <^o,o^>

let o be Object of A; :: thesis: for o1 being Object of (AllMono C) st o = o1 holds
idm o1 in <^o,o^>
let o1 be Object of (AllMono C); :: thesis: ( o = o1 implies idm o1 in <^o,o^> )
assume A9: o = o1 ; :: thesis: idm o1 in <^o,o^>
reconsider oo = o as Object of C by Def4;
idm o = idm oo by ALTCAT_2:34
.= idm o1 by A9, ALTCAT_2:34 ;
hence idm o1 in <^o,o^> ; :: thesis: verum

end;

hence AllCoretr C is non empty subcategory of AllMono C by ALTCAT_2:def 14; :: thesis: verum