set F = field (VertexDomRel G);

now :: thesis: for x, y being object st x in field (VertexDomRel G) & y in field (VertexDomRel G) & [x,y] in VertexDomRel G & [y,x] in VertexDomRel G holds
x = y

let x, y be object ; :: thesis: ( x in field (VertexDomRel G) & y in field (VertexDomRel G) & [x,y] in VertexDomRel G & [y,x] in VertexDomRel G implies x = y )
assume ( x in field (VertexDomRel G) & y in field (VertexDomRel G) ) ; :: thesis: ( [x,y] in VertexDomRel G & [y,x] in VertexDomRel G implies x = y )
assume A1: ( [x,y] in VertexDomRel G & [y,x] in VertexDomRel G ) ; :: thesis: x = y
then consider e1 being object such that
A2: e1 DJoins x,y,G by Th1;
consider e2 being object such that
A3: e2 DJoins y,x,G by A1, Th1;
( e1 Joins x,y,G & e2 Joins x,y,G ) by A2, A3, GLIB_000:16;
then e1 = e2 by GLIB_000:def 20;
hence x = y by A2, A3, GLIB_000:125; :: thesis: verum

end;

hence VertexDomRel G is antisymmetric by RELAT_2:def 4, RELAT_2:def 12; :: thesis: verum