let G1 be reverseEdgeDirections of G,E; :: thesis: G1 is complete
for v1, v2 being Vertex of G1 st v1 <> v2 holds
v1,v2 are_adjacent

proof

let v1, v2 be Vertex of G1; :: thesis: ( v1 <> v2 implies v1,v2 are_adjacent )
assume A1: v1 <> v2 ; :: thesis: v1,v2 are_adjacent
reconsider u1 = v1, u2 = v2 as Vertex of G by Th10;
consider e being object such that
A2: e Joins u1,u2,G by A1, CHORD:def 6, CHORD:def 3;
thus v1,v2 are_adjacent by CHORD:def 3, A2, Th9; :: thesis: verum

end;

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