theorem :: YELLOW18:46

for A being category holds A, Concretized A are_isomorphic