let GS be GraphStruct; :: thesis: for x, y being set
for n1, n2 being Nat st n1 <> n2 holds
( n1 in dom ((GS .set n1,x) .set n2,y) & n2 in dom ((GS .set n1,x) .set n2,y) & ((GS .set n1,x) .set n2,y) . n1 = x & ((GS .set n1,x) .set n2,y) . n2 = y )
let x, y be set ; :: thesis: for n1, n2 being Nat st n1 <> n2 holds
( n1 in dom ((GS .set n1,x) .set n2,y) & n2 in dom ((GS .set n1,x) .set n2,y) & ((GS .set n1,x) .set n2,y) . n1 = x & ((GS .set n1,x) .set n2,y) . n2 = y )
let n1, n2 be Nat; :: thesis: ( n1 <> n2 implies ( n1 in dom ((GS .set n1,x) .set n2,y) & n2 in dom ((GS .set n1,x) .set n2,y) & ((GS .set n1,x) .set n2,y) . n1 = x & ((GS .set n1,x) .set n2,y) . n2 = y ) )
assume A1: n1 <> n2 ; :: thesis: ( n1 in dom ((GS .set n1,x) .set n2,y) & n2 in dom ((GS .set n1,x) .set n2,y) & ((GS .set n1,x) .set n2,y) . n1 = x & ((GS .set n1,x) .set n2,y) . n2 = y )
set G2 = GS .set n1,x;
set G3 = (GS .set n1,x) .set n2,y;
A2: dom ((GS .set n1,x) .set n2,y) = (dom (GS .set n1,x)) \/ {n2} by Th9;
( dom (GS .set n1,x) = (dom GS) \/ {n1} & n1 in {n1} ) by Th9, TARSKI:def 1;
then n1 in dom (GS .set n1,x) by XBOOLE_0:def 3;
hence n1 in dom ((GS .set n1,x) .set n2,y) by A2, XBOOLE_0:def 3; :: thesis: ( n2 in dom ((GS .set n1,x) .set n2,y) & ((GS .set n1,x) .set n2,y) . n1 = x & ((GS .set n1,x) .set n2,y) . n2 = y )
n2 in {n2} by TARSKI:def 1;
hence n2 in dom ((GS .set n1,x) .set n2,y) by A2, XBOOLE_0:def 3; :: thesis: ( ((GS .set n1,x) .set n2,y) . n1 = x & ((GS .set n1,x) .set n2,y) . n2 = y )
thus ((GS .set n1,x) .set n2,y) . n1 = (GS .set n1,x) . n1 by A1, Th12
.= x by Th11 ; :: thesis: ((GS .set n1,x) .set n2,y) . n2 = y
thus ((GS .set n1,x) .set n2,y) . n2 = y by Th11; :: thesis: verum