set F = field (VertexDomRel G);
now 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 Glet x,
y be
object ;
( 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) )
;
( [x,y] in VertexDomRel G implies not [y,x] in VertexDomRel G )assume A1:
(
[x,y] in VertexDomRel G &
[y,x] in VertexDomRel G )
;
contradictionthen 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;
verum end;
hence
VertexDomRel G is asymmetric
by RELAT_2:def 5, RELAT_2:def 13; verum