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:90;
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:65;
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:142;
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 13;
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<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;

end;