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 Th7;
( dom (GS .set (n1,x)) = (dom GS) \/ {n1} & n1 in {n1} ) by Th7, 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, Th9
.= x by Th8 ; :: thesis: ((GS .set (n1,x)) .set (n2,y)) . n2 = y
thus ((GS .set (n1,x)) .set (n2,y)) . n2 = y by Th8; :: thesis: verum