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
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in bool G1 or 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 ;
then G c= G2 by A1, Th17;
then G is strict Subgraph of G2 ;
hence x in bool G2 by Def25; :: thesis: verum

end;

assume A2: bool G1 c= bool G2 ; :: thesis: G1 c= G2
G1 in bool G1 by Th29;
then G1 is Subgraph of G2 by A2, Def25;
hence G1 c= G2 ; :: thesis: verum