set I = id Q;
id Q in Funcs (Q,Q) by FUNCT_2:126;
then reconsider X = {(id Q)} as Subset of (Funcs (Q,Q)) by SUBSET_1:33;
take X ; :: thesis: ( X is composition-closed & X is inverse-closed & not X is empty )
thus ( X is composition-closed & X is inverse-closed & not X is empty ) ; :: thesis: verum