let G be _Graph; :: thesis: for v, w being object holds
( [v,w] in VertexAdjSymRel G iff ex e being object st e Joins v,w,G )
let v, w be object ; :: thesis: ( [v,w] in VertexAdjSymRel G iff ex e being object st e Joins v,w,G )

hereby :: thesis: ( ex e being object st e Joins v,w,G implies [v,w] in VertexAdjSymRel G )

assume [v,w] in VertexAdjSymRel G ; :: thesis: ex e being object st e Joins v,w,G

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

suppose [v,w] in VertexDomRel G ; :: thesis: ex e being object st e Joins v,w,G

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

end;

suppose [v,w] in (VertexDomRel G) ~ ; :: thesis: ex e being object st e Joins v,w,G

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

end;

end;

end;

given e being object such that A3: e Joins v,w,G ; :: thesis: [v,w] in VertexAdjSymRel G

per cases ( e DJoins v,w,G or e DJoins w,v,G ) by A3, GLIB_000:16;

suppose e DJoins v,w,G ; :: thesis: [v,w] in VertexAdjSymRel G

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

end;

suppose e DJoins w,v,G ; :: thesis: [v,w] in VertexAdjSymRel G

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

end;

end;