consider I being object such that
A1: ( I in dom the Sorts of A & a in the Sorts of A . I ) by CARD_5:2;
reconsider I = I as SortSymbol of S by A1;
take I ; :: thesis: a in the Sorts of A . I
thus a in the Sorts of A . I by A1; :: thesis: verum