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
A17: S1 = rng F1 and
A18: F1 = (L `2 ) | ((the_Vertices_of G) \ (dom (L `1 ))) and
A19: for x being finite Subset of NAT st x in S1 holds
x,1 -bag in B1 and
A20: 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
A21: 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
A22: S2 = rng F2 and
A23: F2 = (L `2 ) | ((the_Vertices_of G) \ (dom (L `1 ))) and
A24: for x being finite Subset of NAT st x in S2 holds
x,1 -bag in B2 and
A25: 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
A26: 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 A25;
hence x in B1 by A17, A18, A19, A22, A23; :: thesis: verum

end;

then A27: 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 A20;
hence x in B2 by A17, A18, A22, A23, A24; :: thesis: verum

end;

then B1 c= B2 by TARSKI:def 3;
hence IT1 = IT2 by A18, A21, A23, A26, A27, XBOOLE_0:def 10; :: thesis: verum