reconsider G' = G as strict Element of V by Def22;
ID G' is strict Element of Morphs V by Def30;
hence ID G is strict Element of Morphs V ; :: thesis: verum