theorem :: GRAPH_1:28

for G being Graph
for G1 being strict Graph holds
( G1 in bool G iff G1 c= G ) by Def25;