let G be _Graph; ( 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 )
; 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 )
hence
not VertexDomRel G is asymmetric
by RELAT_2:def 5, RELAT_2:def 13; verum