set VG = the_Vertices_of G;
set V2G = L `2 ;
set VLG = L `1 ;
set F = (L `2) | ((the_Vertices_of G) \ (dom (L `1)));
set S = rng ((L `2) | ((the_Vertices_of G) \ (dom (L `1))));

per cases ( dom (L `1) = the_Vertices_of G or dom (L `1) <> the_Vertices_of G ) ;

suppose dom (L `1) = the_Vertices_of G ; :: thesis: ( ( dom (L `1) = the_Vertices_of G implies ex b₁ being Vertex of G st b₁ = choose (the_Vertices_of G) ) & ( not dom (L `1) = the_Vertices_of G implies ex b<sub>1</sub> being Vertex of G ex S being non empty natural-membered finite set ex F being Function st
( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & b₁ = choose (F " {(max S)}) ) ) )

hence ( ( dom (L `1) = the_Vertices_of G implies ex b<sub>1</sub> being Vertex of G st b<sub>1</sub> = choose (the_Vertices_of G) ) & ( not dom (L `1) = the_Vertices_of G implies ex b₁ being Vertex of G ex S being non empty natural-membered finite set ex F being Function st
( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & b₁ = choose (F " {(max S)}) ) ) ) ; :: thesis: verum

end;

suppose A1: dom (L `1) <> the_Vertices_of G ; :: thesis: ( ( dom (L `1) = the_Vertices_of G implies ex b₁ being Vertex of G st b₁ = choose (the_Vertices_of G) ) & ( not dom (L `1) = the_Vertices_of G implies ex b<sub>1</sub> being Vertex of G ex S being non empty natural-membered finite set ex F being Function st
( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & b₁ = choose (F " {(max S)}) ) ) )

A2: dom ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) = (dom (L `2)) /\ ((the_Vertices_of G) \ (dom (L `1))) by RELAT_1:61;
dom (L `2) = the_Vertices_of G by FUNCT_2:def 1;
then A3: dom ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) = ((the_Vertices_of G) /\ (the_Vertices_of G)) \ (dom (L `1)) by A2, XBOOLE_1:49;

now

assume dom ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) = {} ; :: thesis: contradiction
then the_Vertices_of G c= dom (L `1) by A3, XBOOLE_1:37;
hence contradiction by A1, XBOOLE_0:def 10; :: thesis: verum

end;

then reconsider S = rng ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) as non empty natural-membered finite set by RELAT_1:42;
set y = max S;
set IT = choose (((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) " {(max S)});
max S in S by XXREAL_2:def 8;
then not ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) " {(max S)} is empty by FUNCT_1:72;
then choose (((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) " {(max S)}) in dom ((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) by FUNCT_1:def 7;
then choose (((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) " {(max S)}) in dom (L `2) by RELAT_1:57;
then reconsider IT = choose (((L `2) | ((the_Vertices_of G) \ (dom (L `1)))) " {(max S)}) as Vertex of G ;
ex S being non empty natural-membered finite set ex F being Function st
( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & IT = choose (F " {(max S)}) & IT is Vertex of G ) ;
hence ( ( dom (L `1) = the_Vertices_of G implies ex b₁ being Vertex of G st b₁ = choose (the_Vertices_of G) ) & ( not dom (L `1) = the_Vertices_of G implies ex b<sub>1</sub> being Vertex of G ex S being non empty natural-membered finite set ex F being Function st
( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & b₁ = choose (F " {(max S)}) ) ) ) ; :: thesis: verum

end;

end;