let G be strict Graph; :: thesis: G in bool G
G is Subgraph of G by Def23;
hence G in bool G by Def24; :: thesis: verum