consider c being Object of C;
reconsider A = 1Cat c,(id c) as Subcategory of C by Th7;
take A ; :: thesis: ( A is strict & A is discrete )
thus ( A is strict & A is discrete ) by Th46; :: thesis: verum