set cNB = the Element of AP:NextBestEdges VL;
set SG = the_Source_of G;
set TG = the_Target_of G;
set VG = the_Vertices_of G;
set EG = the_Edges_of G;
set NB = AP:NextBestEdges VL;

per cases ( AP:NextBestEdges VL = {} or AP:NextBestEdges VL <> {} ) ;

suppose AP:NextBestEdges VL = {} ; :: thesis: ( ( AP:NextBestEdges VL = {} implies VL is AP:VLabeling of EL ) & ( AP:NextBestEdges VL <> {} & not (the_Source_of G) . the Element of AP:NextBestEdges VL in dom VL implies VL +* (((the_Source_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL) is AP:VLabeling of EL ) & ( not AP:NextBestEdges VL = {} & ( not AP:NextBestEdges VL <> {} or (the_Source_of G) . the Element of AP:NextBestEdges VL in dom VL ) implies VL +* (((the_Target_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL) is AP:VLabeling of EL ) )

hence ( ( AP:NextBestEdges VL = {} implies VL is AP:VLabeling of EL ) & ( AP:NextBestEdges VL <> {} & not (the_Source_of G) . the Element of AP:NextBestEdges VL in dom VL implies VL +* (((the_Source_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL) is AP:VLabeling of EL ) & ( not AP:NextBestEdges VL = {} & ( not AP:NextBestEdges VL <> {} or (the_Source_of G) . the Element of AP:NextBestEdges VL in dom VL ) implies VL +* (((the_Target_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL) is AP:VLabeling of EL ) ) ; :: thesis: verum

end;

suppose AP:NextBestEdges VL <> {} ; :: thesis: ( ( AP:NextBestEdges VL = {} implies VL is AP:VLabeling of EL ) & ( AP:NextBestEdges VL <> {} & not (the_Source_of G) . the Element of AP:NextBestEdges VL in dom VL implies VL +* (((the_Source_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL) is AP:VLabeling of EL ) & ( not AP:NextBestEdges VL = {} & ( not AP:NextBestEdges VL <> {} or (the_Source_of G) . the Element of AP:NextBestEdges VL in dom VL ) implies VL +* (((the_Target_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL) is AP:VLabeling of EL ) )

then A1: the Element of AP:NextBestEdges VL in AP:NextBestEdges VL ;
A2: {((the_Source_of G) . the Element of AP:NextBestEdges VL)} c= the_Vertices_of G

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {((the_Source_of G) . the Element of AP:NextBestEdges VL)} or x in the_Vertices_of G )
assume x in {((the_Source_of G) . the Element of AP:NextBestEdges VL)} ; :: thesis: x in the_Vertices_of G
then x = (the_Source_of G) . the Element of AP:NextBestEdges VL by TARSKI:def 1;
hence x in the_Vertices_of G by A1, FUNCT_2:5; :: thesis: verum

end;

{ the Element of AP:NextBestEdges VL} c= the_Edges_of G

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { the Element of AP:NextBestEdges VL} or x in the_Edges_of G )
assume x in { the Element of AP:NextBestEdges VL} ; :: thesis: x in the_Edges_of G
then x = the Element of AP:NextBestEdges VL by TARSKI:def 1;
hence x in the_Edges_of G by A1; :: thesis: verum

end;

then A3: { the Element of AP:NextBestEdges VL} c= {1} \/ (the_Edges_of G) by XBOOLE_1:10;
rng (((the_Target_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL) c= { the Element of AP:NextBestEdges VL} by FUNCOP_1:13;
then rng (((the_Target_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL) c= {1} \/ (the_Edges_of G) by A3;
then A4: (rng VL) \/ (rng (((the_Target_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL)) c= {1} \/ (the_Edges_of G) by XBOOLE_1:8;
rng (VL +* (((the_Target_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL)) c= (rng VL) \/ (rng (((the_Target_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL)) by FUNCT_4:17;
then A5: rng (VL +* (((the_Target_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL)) c= {1} \/ (the_Edges_of G) by A4;
{ the Element of AP:NextBestEdges VL} c= the_Edges_of G

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { the Element of AP:NextBestEdges VL} or x in the_Edges_of G )
assume x in { the Element of AP:NextBestEdges VL} ; :: thesis: x in the_Edges_of G
then x = the Element of AP:NextBestEdges VL by TARSKI:def 1;
hence x in the_Edges_of G by A1; :: thesis: verum

end;

then A6: { the Element of AP:NextBestEdges VL} c= {1} \/ (the_Edges_of G) by XBOOLE_1:10;
rng (((the_Source_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL) c= { the Element of AP:NextBestEdges VL} by FUNCOP_1:13;
then rng (((the_Source_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL) c= {1} \/ (the_Edges_of G) by A6;
then A7: (rng VL) \/ (rng (((the_Source_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL)) c= {1} \/ (the_Edges_of G) by XBOOLE_1:8;
rng (VL +* (((the_Source_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL)) c= (rng VL) \/ (rng (((the_Source_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL)) by FUNCT_4:17;
then A8: rng (VL +* (((the_Source_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL)) c= {1} \/ (the_Edges_of G) by A7;
A9: {((the_Target_of G) . the Element of AP:NextBestEdges VL)} c= the_Vertices_of G

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {((the_Target_of G) . the Element of AP:NextBestEdges VL)} or x in the_Vertices_of G )
assume x in {((the_Target_of G) . the Element of AP:NextBestEdges VL)} ; :: thesis: x in the_Vertices_of G
then x = (the_Target_of G) . the Element of AP:NextBestEdges VL by TARSKI:def 1;
hence x in the_Vertices_of G by A1, FUNCT_2:5; :: thesis: verum

end;

dom (VL +* (((the_Target_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL)) = (dom VL) \/ (dom (((the_Target_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL)) by FUNCT_4:def 1
.= (dom VL) \/ {((the_Target_of G) . the Element of AP:NextBestEdges VL)} ;
then A10: VL +* (((the_Target_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL) is Relation of (the_Vertices_of G),({1} \/ (the_Edges_of G)) by A9, A5, RELSET_1:4, XBOOLE_1:8;
dom (VL +* (((the_Source_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL)) = (dom VL) \/ (dom (((the_Source_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL)) by FUNCT_4:def 1
.= (dom VL) \/ {((the_Source_of G) . the Element of AP:NextBestEdges VL)} ;
then VL +* (((the_Source_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL) is Relation of (the_Vertices_of G),({1} \/ (the_Edges_of G)) by A2, A8, RELSET_1:4, XBOOLE_1:8;
hence ( ( AP:NextBestEdges VL = {} implies VL is AP:VLabeling of EL ) & ( AP:NextBestEdges VL <> {} & not (the_Source_of G) . the Element of AP:NextBestEdges VL in dom VL implies VL +* (((the_Source_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL) is AP:VLabeling of EL ) & ( not AP:NextBestEdges VL = {} & ( not AP:NextBestEdges VL <> {} or (the_Source_of G) . the Element of AP:NextBestEdges VL in dom VL ) implies VL +* (((the_Target_of G) . the Element of AP:NextBestEdges VL) .--> the Element of AP:NextBestEdges VL) is AP:VLabeling of EL ) ) by A10, Def5; :: thesis: verum

end;

end;