let G be Graph; :: thesis: for v1, v2 being Vertex of G holds
( the carrier' of G in the carrier' of (AddNewEdge (v1,v2)) & the carrier' of G = the carrier' of (AddNewEdge (v1,v2)) \ { the carrier' of G} & the Source of (AddNewEdge (v1,v2)) . the carrier' of G = v1 & the Target of (AddNewEdge (v1,v2)) . the carrier' of G = v2 )
let v1, v2 be Vertex of G; :: thesis: ( the carrier' of G in the carrier' of (AddNewEdge (v1,v2)) & the carrier' of G = the carrier' of (AddNewEdge (v1,v2)) \ { the carrier' of G} & the Source of (AddNewEdge (v1,v2)) . the carrier' of G = v1 & the Target of (AddNewEdge (v1,v2)) . the carrier' of G = v2 )
set G9 = AddNewEdge (v1,v2);
set E = the carrier' of G;
set S = the Source of G;
set T = the Target of G;
set E9 = the carrier' of (AddNewEdge (v1,v2));
A1: the carrier' of (AddNewEdge (v1,v2)) = the carrier' of G \/ { the carrier' of G} by Def7;
the carrier' of G in { the carrier' of G} by TARSKI:def 1;
hence the carrier' of G in the carrier' of (AddNewEdge (v1,v2)) by A1, XBOOLE_0:def 3; :: thesis: ( the carrier' of G = the carrier' of (AddNewEdge (v1,v2)) \ { the carrier' of G} & the Source of (AddNewEdge (v1,v2)) . the carrier' of G = v1 & the Target of (AddNewEdge (v1,v2)) . the carrier' of G = v2 )

now :: thesis: for x being object holds
( ( x in the carrier' of G implies x in the carrier' of (AddNewEdge (v1,v2)) \ { the carrier' of G} ) & ( x in the carrier' of (AddNewEdge (v1,v2)) \ { the carrier' of G} implies x in the carrier' of G ) )

let x be object ; :: thesis: ( ( x in the carrier' of G implies x in the carrier' of (AddNewEdge (v1,v2)) \ { the carrier' of G} ) & ( x in the carrier' of (AddNewEdge (v1,v2)) \ { the carrier' of G} implies x in the carrier' of G ) )

hereby :: thesis: ( x in the carrier' of (AddNewEdge (v1,v2)) \ { the carrier' of G} implies x in the carrier' of G )

assume A2: x in the carrier' of G ; :: thesis: x in the carrier' of (AddNewEdge (v1,v2)) \ { the carrier' of G}
then reconsider x1 = x as set ;
not x1 in x1 ;
then x <> the carrier' of G by A2;
then A3: not x in { the carrier' of G} by TARSKI:def 1;
x in the carrier' of (AddNewEdge (v1,v2)) by A1, A2, XBOOLE_0:def 3;
hence x in the carrier' of (AddNewEdge (v1,v2)) \ { the carrier' of G} by A3, XBOOLE_0:def 5; :: thesis: verum

end;

assume A4: x in the carrier' of (AddNewEdge (v1,v2)) \ { the carrier' of G} ; :: thesis: x in the carrier' of G
then not x in { the carrier' of G} by XBOOLE_0:def 5;
hence x in the carrier' of G by A1, A4, XBOOLE_0:def 3; :: thesis: verum

end;

hence the carrier' of G = the carrier' of (AddNewEdge (v1,v2)) \ { the carrier' of G} by TARSKI:2; :: thesis: ( the Source of (AddNewEdge (v1,v2)) . the carrier' of G = v1 & the Target of (AddNewEdge (v1,v2)) . the carrier' of G = v2 )
A5: the carrier' of G in dom ( the carrier' of G .--> v1) by TARSKI:def 1;
the Source of (AddNewEdge (v1,v2)) = the Source of G +* ( the carrier' of G .--> v1) by Def7;
hence the Source of (AddNewEdge (v1,v2)) . the carrier' of G = ( the carrier' of G .--> v1) . the carrier' of G by A5, FUNCT_4:13
.= v1 by FUNCOP_1:72 ;
:: thesis: the Target of (AddNewEdge (v1,v2)) . the carrier' of G = v2
A6: the carrier' of G in dom ( the carrier' of G .--> v2) by TARSKI:def 1;
the Target of (AddNewEdge (v1,v2)) = the Target of G +* ( the carrier' of G .--> v2) by Def7;
hence the Target of (AddNewEdge (v1,v2)) . the carrier' of G = ( the carrier' of G .--> v2) . the carrier' of G by A6, FUNCT_4:13
.= v2 by FUNCOP_1:72 ;
:: thesis: verum