let G be _Graph; :: thesis:
let v, w be object ; :: thesis:

hereby :: thesis:

assume [v,w] in VertexAdjSymRel G ; :: thesis:

per cases in VertexDomRel G or [v,w] in (VertexDomRel G) ~ ) by XBOOLE_0:def 3;

suppose [v,w] in VertexDomRel G ; :: thesis:

then consider e being object such that
A1: e DJoins v,w,G by Th1;
take e = e; :: thesis:
thus e Joins v,w,G by A1, GLIB_000:16; :: thesis:

end;

suppose [v,w] in (VertexDomRel G) ~ ; :: thesis:

then consider e being object such that
A2: e DJoins w,v,G by Th2;
take e = e; :: thesis:
thus e Joins v,w,G by A2, GLIB_000:16; :: thesis:

end;

end;

end;

given e being object such that A3: e Joins v,w,G ; :: thesis:

per cases by A3, GLIB_000:16;

suppose e DJoins v,w,G ; :: thesis:

then [v,w] in VertexDomRel G by Th1;
hence [v,w] in VertexAdjSymRel G by XBOOLE_0:def 3; :: thesis:

end;

suppose e DJoins w,v,G ; :: thesis:

then [v,w] in (VertexDomRel G) ~ by Th2;
hence [v,w] in VertexAdjSymRel G by XBOOLE_0:def 3; :: thesis:

end;

end;