let G be GraphUnion of G1,G2; :: thesis: ( G is loopfull & G is complete )
for v being Vertex of G ex e being object st e Joins v,v,G by Th31;
hence G is loopfull by GLIB_012:def 1; :: thesis: G is complete

now :: thesis: for v, w being Vertex of G st v <> w holds
v,w are_adjacent

let v, w be Vertex of G; :: thesis: ( v <> w implies v,w are_adjacent )
assume v <> w ; :: thesis: v,w are_adjacent
consider e being object such that
A1: e Joins v,w,G by Th31;
thus v,w are_adjacent by A1, CHORD:def 3; :: thesis: verum

end;

hence G is complete by CHORD:def 6; :: thesis: verum