let G be GraphUnion of G1,G2; :: 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
then consider e being object such that
A1: e Joins v,w,G by Th33;
thus v,w are_adjacent by A1, CHORD:def 3; :: thesis: verum

end;

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