set C = RingCat UN;
thus RingCat UN is Category-like by Th21; :: thesis: ( RingCat UN is transitive & RingCat UN is associative & RingCat UN is reflexive )
thus RingCat UN is transitive by Lm9; :: thesis: ( RingCat UN is associative & RingCat UN is reflexive )
thus RingCat UN is associative by Lm10; :: thesis: RingCat UN is reflexive
thus RingCat UN is reflexive :: thesis: verum

proof

let a be Element of (RingCat UN); :: according to CAT_1:def 9 :: thesis: not Hom (a,a) = {}
reconsider G = a as Element of RingObjects UN ;
consider x being set such that
x in UN and
A1: GO x,G by Def16;
set ii = ID G;
consider x1, x2, x3, x4, x5, x6 being set such that
x = [[x1,x2,x3,x4],x5,x6] and
A2: ex H being strict Ring st
( G = H & x1 = the carrier of H & x2 = the addF of H & x3 = comp H & x4 = 0. H & x5 = the multF of H & x6 = 1. H ) by A1;
reconsider G = G as strict Element of RingObjects UN by A2;
reconsider ii = ID G as Morphism of (RingCat UN) ;
reconsider ia = ii as RingMorphismStr ;
A3: dom ii = dom ia by Def19
.= a ;
cod ii = cod ia by Def20
.= a ;
then ii in Hom (a,a) by A3;
hence Hom (a,a) <> {} ; :: thesis: verum

end;