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

proof

assume A1: G1 c= G2 ; :: thesis: bool G1 c= bool G2
for x being set st x in bool G1 holds
x in bool G2

proof

let x be set ; :: thesis: ( x in bool G1 implies x in bool G2 )
assume x in bool G1 ; :: thesis: x in bool G2
then reconsider G = x as strict Subgraph of G1 by Def25;
G c= G1 by Def24;
then G c= G2 by A1, Th17;
then G is strict Subgraph of G2 by Def24;
hence x in bool G2 by Def25; :: thesis: verum

end;

hence bool G1 c= bool G2 by TARSKI:def 3; :: thesis: verum

end;

assume A7: bool G1 c= bool G2 ; :: thesis: G1 c= G2
G1 in bool G1 by Th31;
then G1 is Subgraph of G2 by A7, Def25;
hence G1 c= G2 by Def24; :: thesis: verum