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
;
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
;
ex e2, x, y being object st
( e1 DJoins x,y,G & e2 DJoins y,x,G )take
e2
;
ex x, y being object st
( e1 DJoins x,y,G & e2 DJoins y,x,G )take
x
;
ex y being object st
( e1 DJoins x,y,G & e2 DJoins y,x,G )take
y
;
( e1 DJoins x,y,G & e2 DJoins y,x,G )thus
(
e1 DJoins x,
y,
G &
e2 DJoins y,
x,
G )
by A2, A3;
verum end; suppose A4:
e1 DJoins y,
x,
G
;
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
;
ex e2, x, y being object st
( e1 DJoins x,y,G & e2 DJoins y,x,G )take
e2
;
ex x, y being object st
( e1 DJoins x,y,G & e2 DJoins y,x,G )take
y
;
ex y being object st
( e1 DJoins y,y,G & e2 DJoins y,y,G )take
x
;
( e1 DJoins y,x,G & e2 DJoins x,y,G )thus
(
e1 DJoins y,
x,
G &
e2 DJoins x,
y,
G )
by A4, A5;
verum end; end;
end;
hence
not VertexDomRel G is asymmetric
by Th4; verum