reconsider G = G as strict Element of V by Def1;
ID G is strict Element of Morphs V by Def7;
hence ID G is strict Element of Morphs V ; :: thesis: verum