set c = the Object of C;
reconsider A = 1Cat ( the Object of C,(id the Object of C)) as Subcategory of C by Th3;
take A ; :: thesis: ( A is strict & A is discrete )
thus ( A is strict & A is discrete ) ; :: thesis: verum