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;
set cNB = choose (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 A02: choose (AP:NextBestEdges VL) in AP:NextBestEdges VL ;
A0: 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:19 ;
A1: {((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 A02, FUNCT_2:7; :: thesis: verum

end;

Aa0: 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:18;
Aa02: rng (((the_Source_of G) . (choose (AP:NextBestEdges VL))) .--> (choose (AP:NextBestEdges VL))) c= {(choose (AP:NextBestEdges VL))} by FUNCOP_1:19;
{(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 A02; :: thesis: verum

end;

then {(choose (AP:NextBestEdges VL))} c= {1} \/ (the_Edges_of G) by XBOOLE_1:10;
then rng (((the_Source_of G) . (choose (AP:NextBestEdges VL))) .--> (choose (AP:NextBestEdges VL))) c= {1} \/ (the_Edges_of G) by Aa02, XBOOLE_1:1;
then (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;
then rng (VL +* (((the_Source_of G) . (choose (AP:NextBestEdges VL))) .--> (choose (AP:NextBestEdges VL)))) c= {1} \/ (the_Edges_of G) by Aa0, XBOOLE_1:1;
then A: 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 A1, A0, RELSET_1:11, XBOOLE_1:8;
A0: 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:19 ;
A1: {((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 A02, FUNCT_2:7; :: thesis: verum

end;

Aa0: 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:18;
Aa02: rng (((the_Target_of G) . (choose (AP:NextBestEdges VL))) .--> (choose (AP:NextBestEdges VL))) c= {(choose (AP:NextBestEdges VL))} by FUNCOP_1:19;
{(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 A02; :: thesis: verum

end;

then {(choose (AP:NextBestEdges VL))} c= {1} \/ (the_Edges_of G) by XBOOLE_1:10;
then rng (((the_Target_of G) . (choose (AP:NextBestEdges VL))) .--> (choose (AP:NextBestEdges VL))) c= {1} \/ (the_Edges_of G) by Aa02, XBOOLE_1:1;
then (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;
then rng (VL +* (((the_Target_of G) . (choose (AP:NextBestEdges VL))) .--> (choose (AP:NextBestEdges VL)))) c= {1} \/ (the_Edges_of G) by Aa0, XBOOLE_1:1;
then 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 A1, A0, RELSET_1:11, 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 A, HeHe; :: thesis: verum

end;

end;