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
A2: 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 A3: x in bool G1 ; :: thesis: x in bool G2
reconsider G = x as strict Subgraph of G1 by A3, Def25;
A4: G c= G1 by Def24;
A5: G c= G2 by A1, A4, Th17;
A6: G is strict Subgraph of G2 by A5, Def24;
thus x in bool G2 by A6, Def25; :: thesis: verum

end;

thus bool G1 c= bool G2 by A2, TARSKI:def 3; :: thesis: verum

end;

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