let C be category; :: thesis: AllRetr C is non empty subcategory of AllEpi C
the carrier of (AllRetr C) = the carrier of C by Def3;
then A1: the carrier of (AllRetr C) c= the carrier of (AllEpi C) by Def2;
AllRetr C is SubCatStr of AllEpi C

proof

the Arrows of (AllRetr C) cc= the Arrows of (AllEpi C)

proof

thus [:the carrier of (AllRetr C),the carrier of (AllRetr C):] c= [:the carrier of (AllEpi C),the carrier of (AllEpi C):] by A1, ZFMISC_1:119; :: according to ALTCAT_2:def 2 :: thesis: for b₁ being set holds
( not b₁ in [:the carrier of (AllRetr C),the carrier of (AllRetr C):] or the Arrows of (AllRetr C) . b₁ c= the Arrows of (AllEpi C) . b₁ )
let i be set ; :: thesis: ( not i in [:the carrier of (AllRetr C),the carrier of (AllRetr C):] or the Arrows of (AllRetr C) . i c= the Arrows of (AllEpi C) . i )
assume A2: i in [:the carrier of (AllRetr C),the carrier of (AllRetr C):] ; :: thesis: the Arrows of (AllRetr C) . i c= the Arrows of (AllEpi C) . i
then consider o1, o2 being set such that
A3: ( o1 in the carrier of (AllRetr C) & o2 in the carrier of (AllRetr C) & i = [o1,o2] ) by ZFMISC_1:103;
reconsider o1 = o1, o2 = o2 as object of C by A3, Def3;
let m be set ; :: according to TARSKI:def 3 :: thesis: ( not m in the Arrows of (AllRetr C) . i or m in the Arrows of (AllEpi C) . i )
assume A4: m in the Arrows of (AllRetr C) . i ; :: thesis: m in the Arrows of (AllEpi C) . i
then A5: m in the Arrows of (AllRetr C) . o1,o2 by A3;
the Arrows of (AllRetr C) cc= the Arrows of C by Def3;
then the Arrows of (AllRetr C) . [o1,o2] c= the Arrows of C . o1,o2 by A2, A3, ALTCAT_2:def 2;
then reconsider m1 = m as Morphism of o1,o2 by A3, A4;
m1 in the Arrows of (AllRetr C) . o1,o2 by A3, A4;
then A6: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) by Def3;
m1 is retraction by A5, Def3;
then m1 is epi by A6, ALTCAT_3:15;
then m in the Arrows of (AllEpi C) . o1,o2 by A6, Def2;
hence m in the Arrows of (AllEpi C) . i by A3; :: thesis: verum

end;

hence AllRetr C is SubCatStr of AllEpi C by A1, ALTCAT_2:25; :: thesis: verum

end;

then reconsider A = AllRetr C as non empty with_units SubCatStr of AllEpi C ;
A is id-inheriting

proof

now

let o be object of A; :: thesis: for o1 being object of (AllEpi C) st o = o1 holds
idm o1 in <^o,o^>
let o1 be object of (AllEpi C); :: thesis: ( o = o1 implies idm o1 in <^o,o^> )
assume A7: o = o1 ; :: thesis: idm o1 in <^o,o^>
reconsider oo = o as object of C by Def3;
idm o = idm oo by ALTCAT_2:35
.= idm o1 by A7, ALTCAT_2:35 ;
hence idm o1 in <^o,o^> ; :: thesis: verum

end;

hence A is id-inheriting by ALTCAT_2:def 14; :: thesis: verum

end;

hence AllRetr C is non empty subcategory of AllEpi C ; :: thesis: verum