ex e1, e2, x, y being object st
( e1 DJoins x,y,G & e2 DJoins y,x,G )
proof
consider e1, e2, x, y being object such that
A1: ( e1 Joins x,y,G & e2 Joins x,y,G & e1 <> e2 ) by GLIB_000:def 20;
per cases ( e1 DJoins x,y,G or e1 DJoins y,x,G ) by A1, GLIB_000:16;
suppose A2: e1 DJoins x,y,G ; :: thesis: ex e1, e2, x, y being object st
( e1 DJoins x,y,G & e2 DJoins y,x,G )
then not e2 DJoins x,y,G by A1, GLIB_000:def 21;
then A3: e2 DJoins y,x,G by A1, GLIB_000:16;
take e1 ; :: thesis: ex e2, x, y being object st
( e1 DJoins x,y,G & e2 DJoins y,x,G )
take e2 ; :: thesis: ex x, y being object st
( e1 DJoins x,y,G & e2 DJoins y,x,G )
take x ; :: thesis: ex y being object st
( e1 DJoins x,y,G & e2 DJoins y,x,G )
take y ; :: thesis: ( e1 DJoins x,y,G & e2 DJoins y,x,G )
thus ( e1 DJoins x,y,G & e2 DJoins y,x,G ) by A2, A3; :: thesis: verum
end;
suppose A4: e1 DJoins y,x,G ; :: thesis: ex e1, e2, x, y being object st
( e1 DJoins x,y,G & e2 DJoins y,x,G )
then not e2 DJoins y,x,G by A1, GLIB_000:def 21;
then A5: e2 DJoins x,y,G by A1, GLIB_000:16;
take e1 ; :: thesis: ex e2, x, y being object st
( e1 DJoins x,y,G & e2 DJoins y,x,G )
take e2 ; :: thesis: ex x, y being object st
( e1 DJoins x,y,G & e2 DJoins y,x,G )
take y ; :: thesis: ex y being object st
( e1 DJoins y,y,G & e2 DJoins y,y,G )
take x ; :: thesis: ( e1 DJoins y,x,G & e2 DJoins x,y,G )
thus ( e1 DJoins y,x,G & e2 DJoins x,y,G ) by A4, A5; :: thesis: verum
end;
end;
end;
hence not VertexDomRel G is asymmetric by Th4; :: thesis: verum