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 G1 in bool G ; :: thesis: G1 c= G
then G1 is Subgraph of G by Def25;
hence G1 c= G by Def24; :: thesis: verum

end;

assume G1 c= G ; :: thesis: G1 in bool G
then G1 is Subgraph of G by Def24;
hence G1 in bool G by Def25; :: thesis: verum