let G be SubStr of G2; :: thesis: G is SubStr of G1
( H2(G) c= H2(G2) & H2(G2) c= H2(G1) ) by Def23;
hence H2(G) c= H2(G1) ; :: according to MONOID_0:def 23 :: thesis: verum