set cNB = choose (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) . (choose (AP:NextBestEdges VL)) in dom VL implies VL +* (((the_Source_of G) . (choose (AP:NextBestEdges VL))) .--> (choose (AP:NextBestEdges VL))) is AP:VLabeling of EL ) & ( not AP:NextBestEdges VL = {} & ( not AP:NextBestEdges VL <> {} or (the_Source_of G) . (choose (AP:NextBestEdges VL)) in dom VL ) implies VL +* (((the_Target_of G) . (choose (AP:NextBestEdges VL))) .--> (choose (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) . (choose (AP:NextBestEdges VL)) in dom VL implies VL +* (((the_Source_of G) . (choose (AP:NextBestEdges VL))) .--> (choose (AP:NextBestEdges VL))) is AP:VLabeling of EL ) & ( not AP:NextBestEdges VL = {} & ( not AP:NextBestEdges VL <> {} or (the_Source_of G) . (choose (AP:NextBestEdges VL)) in dom VL ) implies VL +* (((the_Target_of G) . (choose (AP:NextBestEdges VL))) .--> (choose (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) . (choose (AP:NextBestEdges VL)) in dom VL implies VL +* (((the_Source_of G) . (choose (AP:NextBestEdges VL))) .--> (choose (AP:NextBestEdges VL))) is AP:VLabeling of EL ) & ( not AP:NextBestEdges VL = {} & ( not AP:NextBestEdges VL <> {} or (the_Source_of G) . (choose (AP:NextBestEdges VL)) in dom VL ) implies VL +* (((the_Target_of G) . (choose (AP:NextBestEdges VL))) .--> (choose (AP:NextBestEdges VL))) is AP:VLabeling of EL ) )

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

proof

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

end;

{(choose (AP:NextBestEdges VL))} c= the_Edges_of G

proof

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

end;

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

proof

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

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {((the_Target_of G) . (choose (AP:NextBestEdges VL)))} or x in the_Vertices_of G )
assume x in {((the_Target_of G) . (choose (AP:NextBestEdges VL)))} ; :: thesis: x in the_Vertices_of G
then x = (the_Target_of G) . (choose (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) . (choose (AP:NextBestEdges VL))) .--> (choose (AP:NextBestEdges VL)))) = (dom VL) \/ (dom (((the_Target_of G) . (choose (AP:NextBestEdges VL))) .--> (choose (AP:NextBestEdges VL)))) by FUNCT_4:def 1
.= (dom VL) \/ {((the_Target_of G) . (choose (AP:NextBestEdges VL)))} by FUNCOP_1:13 ;
then A10: VL +* (((the_Target_of G) . (choose (AP:NextBestEdges VL))) .--> (choose (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) . (choose (AP:NextBestEdges VL))) .--> (choose (AP:NextBestEdges VL)))) = (dom VL) \/ (dom (((the_Source_of G) . (choose (AP:NextBestEdges VL))) .--> (choose (AP:NextBestEdges VL)))) by FUNCT_4:def 1
.= (dom VL) \/ {((the_Source_of G) . (choose (AP:NextBestEdges VL)))} by FUNCOP_1:13 ;
then VL +* (((the_Source_of G) . (choose (AP:NextBestEdges VL))) .--> (choose (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) . (choose (AP:NextBestEdges VL)) in dom VL implies VL +* (((the_Source_of G) . (choose (AP:NextBestEdges VL))) .--> (choose (AP:NextBestEdges VL))) is AP:VLabeling of EL ) & ( not AP:NextBestEdges VL = {} & ( not AP:NextBestEdges VL <> {} or (the_Source_of G) . (choose (AP:NextBestEdges VL)) in dom VL ) implies VL +* (((the_Target_of G) . (choose (AP:NextBestEdges VL))) .--> (choose (AP:NextBestEdges VL))) is AP:VLabeling of EL ) ) by A10, Def5; :: thesis: verum

end;

end;