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_009:6;
hence contradiction by A2, GLIB_009:17; :: thesis: verum