let G be Graph; :: thesis: for G1 being strict Graph holds
( G1 in bool G iff G1 c= G )
let G1 be strict Graph; :: thesis: ( G1 in bool G iff G1 c= G )
thus ( G1 in bool G implies G1 c= G ) :: thesis: ( G1 c= G implies G1 in bool G )

proof

assume A1: G1 in bool G ; :: thesis: G1 c= G
A2: G1 is Subgraph of G by A1, Def25;
thus G1 c= G by A2, Def24; :: thesis: verum

end;

assume A3: G1 c= G ; :: thesis: G1 in bool G
A4: G1 is Subgraph of G by A3, Def24;
thus G1 in bool G by A4, Def25; :: thesis: verum