let G1, G2 be _Graph; :: thesis: ( G1 == G2 & G1 is complete implies G2 is complete )
assume A1: G1 == G2 ; :: thesis: ( not G1 is complete or G2 is complete )
assume A2: G1 is complete ; :: thesis: G2 is complete

now

let u, v be Vertex of G2; :: thesis: ( u <> v implies u,v are_adjacent )
assume A3: u <> v ; :: thesis: u,v are_adjacent
reconsider v2 = v as Vertex of G1 by A1, GLIB_000:def 34;
reconsider u2 = u as Vertex of G1 by A1, GLIB_000:def 34;
u2,v2 are_adjacent by A2, A3, Def6;
hence u,v are_adjacent by A1, Th44; :: thesis: verum

end;

hence G2 is complete by Def6; :: thesis: verum