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

assume A1: G1 == G2 ; :: thesis: ( not G1 is complete or G2 is complete )

assume A2: G1 is complete ; :: thesis: G2 is complete

now :: thesis: for u, v being Vertex of G2 st u <> v holds

u,v are_adjacent

hence
G2 is complete
; :: thesis: verumu,v are_adjacent

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;

reconsider u2 = u as Vertex of G1 by A1;

u2,v2 are_adjacent by A2, A3;

hence u,v are_adjacent by A1, Th43; :: thesis: verum

end;assume A3: u <> v ; :: thesis: u,v are_adjacent

reconsider v2 = v as Vertex of G1 by A1;

reconsider u2 = u as Vertex of G1 by A1;

u2,v2 are_adjacent by A2, A3;

hence u,v are_adjacent by A1, Th43; :: thesis: verum