let IT1, IT2 be Vertex of G; :: thesis: ( ( dom (L `1) = the_Vertices_of G & IT1 = choose (the_Vertices_of G) & IT2 = choose (the_Vertices_of G) implies IT1 = IT2 ) & ( not dom (L `1) = the_Vertices_of G & ex S being non empty finite Subset of (bool NAT) ex B being non empty finite Subset of (Bags NAT) ex F being Function st
( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & ( for x being finite Subset of NAT st x in S holds
(x,1) -bag in B ) & ( for x being set st x in B holds
ex y being finite Subset of NAT st
( y in S & x = (y,1) -bag ) ) & IT1 = choose (F " {(support (max (B,(InvLexOrder NAT))))}) ) & ex S being non empty finite Subset of (bool NAT) ex B being non empty finite Subset of (Bags NAT) ex F being Function st
( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & ( for x being finite Subset of NAT st x in S holds
(x,1) -bag in B ) & ( for x being set st x in B holds
ex y being finite Subset of NAT st
( y in S & x = (y,1) -bag ) ) & IT2 = choose (F " {(support (max (B,(InvLexOrder NAT))))}) ) implies IT1 = IT2 ) )
set VG = the_Vertices_of G;
set V2G = L `2 ;
set VLG = L `1 ;
thus ( dom (L `1) = the_Vertices_of G & IT1 = choose (the_Vertices_of G) & IT2 = choose (the_Vertices_of G) implies IT1 = IT2 ) ; :: thesis: ( not dom (L `1) = the_Vertices_of G & ex S being non empty finite Subset of (bool NAT) ex B being non empty finite Subset of (Bags NAT) ex F being Function st
( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & ( for x being finite Subset of NAT st x in S holds
(x,1) -bag in B ) & ( for x being set st x in B holds
ex y being finite Subset of NAT st
( y in S & x = (y,1) -bag ) ) & IT1 = choose (F " {(support (max (B,(InvLexOrder NAT))))}) ) & ex S being non empty finite Subset of (bool NAT) ex B being non empty finite Subset of (Bags NAT) ex F being Function st
( S = rng F & F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & ( for x being finite Subset of NAT st x in S holds
(x,1) -bag in B ) & ( for x being set st x in B holds
ex y being finite Subset of NAT st
( y in S & x = (y,1) -bag ) ) & IT2 = choose (F " {(support (max (B,(InvLexOrder NAT))))}) ) implies IT1 = IT2 )
assume dom (L `1) <> the_Vertices_of G ; :: thesis: ( for S being non empty finite Subset of (bool NAT)
for B being non empty finite Subset of (Bags NAT)
for F being Function holds
( not S = rng F or not F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) or ex x being finite Subset of NAT st
( x in S & not (x,1) -bag in B ) or ex x being set st
( x in B & ( for y being finite Subset of NAT holds
( not y in S or not x = (y,1) -bag ) ) ) or not IT1 = choose (F " {(support (max (B,(InvLexOrder NAT))))}) ) or for S being non empty finite Subset of (bool NAT)
for B being non empty finite Subset of (Bags NAT)
for F being Function holds
( not S = rng F or not F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) or ex x being finite Subset of NAT st
( x in S & not (x,1) -bag in B ) or ex x being set st
( x in B & ( for y being finite Subset of NAT holds
( not y in S or not x = (y,1) -bag ) ) ) or not IT2 = choose (F " {(support (max (B,(InvLexOrder NAT))))}) ) or IT1 = IT2 )
assume ex S1 being non empty finite Subset of (bool NAT) ex B1 being non empty finite Subset of (Bags NAT) ex F1 being Function st
( S1 = rng F1 & F1 = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & ( for x being finite Subset of NAT st x in S1 holds
(x,1) -bag in B1 ) & ( for x being set st x in B1 holds
ex y being finite Subset of NAT st
( y in S1 & x = (y,1) -bag ) ) & IT1 = choose (F1 " {(support (max (B1,(InvLexOrder NAT))))}) ) ; :: thesis: ( for S being non empty finite Subset of (bool NAT)
for B being non empty finite Subset of (Bags NAT)
for F being Function holds
( not S = rng F or not F = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) or ex x being finite Subset of NAT st
( x in S & not (x,1) -bag in B ) or ex x being set st
( x in B & ( for y being finite Subset of NAT holds
( not y in S or not x = (y,1) -bag ) ) ) or not IT2 = choose (F " {(support (max (B,(InvLexOrder NAT))))}) ) or IT1 = IT2 )
then consider S1 being non empty finite Subset of (bool NAT), B1 being non empty finite Subset of (Bags NAT), F1 being Function such that
A16: S1 = rng F1 and
A17: F1 = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) and
A18: for x being finite Subset of NAT st x in S1 holds
(x,1) -bag in B1 and
A19: for x being set st x in B1 holds
ex y being finite Subset of NAT st
( y in S1 & x = (y,1) -bag ) and
A20: IT1 = choose (F1 " {(support (max (B1,(InvLexOrder NAT))))}) ;
assume ex S2 being non empty finite Subset of (bool NAT) ex B2 being non empty finite Subset of (Bags NAT) ex F2 being Function st
( S2 = rng F2 & F2 = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) & ( for x being finite Subset of NAT st x in S2 holds
(x,1) -bag in B2 ) & ( for x being set st x in B2 holds
ex y being finite Subset of NAT st
( y in S2 & x = (y,1) -bag ) ) & IT2 = choose (F2 " {(support (max (B2,(InvLexOrder NAT))))}) ) ; :: thesis: IT1 = IT2
then consider S2 being non empty finite Subset of (bool NAT), B2 being non empty finite Subset of (Bags NAT), F2 being Function such that
A21: S2 = rng F2 and
A22: F2 = (L `2) | ((the_Vertices_of G) \ (dom (L `1))) and
A23: for x being finite Subset of NAT st x in S2 holds
(x,1) -bag in B2 and
A24: for x being set st x in B2 holds
ex y being finite Subset of NAT st
( y in S2 & x = (y,1) -bag ) and
A25: IT2 = choose (F2 " {(support (max (B2,(InvLexOrder NAT))))}) ;

now

let x be set ; :: thesis: ( x in B2 implies x in B1 )
assume x in B2 ; :: thesis: x in B1
then ex y being finite Subset of NAT st
( y in S2 & x = (y,1) -bag ) by A24;
hence x in B1 by A16, A17, A18, A21, A22; :: thesis: verum

end;

then A26: B2 c= B1 by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in B1 implies x in B2 )
assume x in B1 ; :: thesis: x in B2
then ex y being finite Subset of NAT st
( y in S1 & x = (y,1) -bag ) by A19;
hence x in B2 by A16, A17, A21, A22, A23; :: thesis: verum

end;

then B1 c= B2 by TARSKI:def 3;
hence IT1 = IT2 by A17, A20, A22, A25, A26, XBOOLE_0:def 10; :: thesis: verum