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