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