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