reconsider H = G2 as SubStr of G1 by Th21;
let G be SubStr of G2; :: thesis: G is SubStr of G1
G is SubStr of H ;
hence G is SubStr of G1 ; :: thesis: verum