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 holds
not [y,x] in VertexDomRel G

let x, y be object ; :: thesis: ( x in field (VertexDomRel G) & y in field (VertexDomRel G) & [x,y] in VertexDomRel G implies not [y,x] in VertexDomRel G )
assume ( x in field (VertexDomRel G) & y in field (VertexDomRel G) ) ; :: thesis: ( [x,y] in VertexDomRel G implies not [y,x] in VertexDomRel G )
assume A1: ( [x,y] in VertexDomRel G & [y,x] in VertexDomRel G ) ; :: thesis: contradiction
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;
then x = y by A2, A3, GLIB_000:125;
hence contradiction by A2, GLIB_000:136; :: thesis: verum

end;

hence VertexDomRel G is asymmetric by RELAT_2:def 5, RELAT_2:def 13; :: thesis: verum