let G be _Graph; :: thesis: ( ex e1, e2, x, y being object st
( e1 DJoins x,y,G & e2 DJoins y,x,G ) implies not VertexDomRel G is asymmetric )
given e1, e2, x, y being object such that A1: ( e1 DJoins x,y,G & e2 DJoins y,x,G ) ; :: thesis: not VertexDomRel G is asymmetric
set R = VertexDomRel G;
ex 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 )

proof

take x ; :: thesis: ex y being object st
( x in field (VertexDomRel G) & y in field (VertexDomRel G) & [x,y] in VertexDomRel G & [y,x] in VertexDomRel G )
take y ; :: thesis: ( x in field (VertexDomRel G) & y in field (VertexDomRel G) & [x,y] in VertexDomRel G & [y,x] in VertexDomRel G )
( [x,y] in VertexDomRel G & [y,x] in VertexDomRel G ) by A1, Th1;
hence ( x in field (VertexDomRel G) & y in field (VertexDomRel G) & [x,y] in VertexDomRel G & [y,x] in VertexDomRel G ) by RELAT_1:15; :: thesis: verum

end;

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