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 DJoins v,v,G by Th30;
hence G is loopfull by GLIB_012: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 DJoins v,w,G by Th30;
e Joins v,w,G by A1, GLIB_000:16;
hence v,w are_adjacent by CHORD:def 3; :: thesis: verum

end;

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