let IT1, IT2 be Vertex of G; ( ( dom (L `1) = the_Vertices_of G & IT1 = the Element of the_Vertices_of G & IT2 = the Element of 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 = the Element of 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 = the Element of 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 = the Element of the_Vertices_of G & IT2 = the Element of 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 = the Element of 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 = the Element of F " {(support (max (B,(InvLexOrder NAT))))} ) implies IT1 = IT2 )
assume
dom (L `1) <> the_Vertices_of G
; ( 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 = the Element of 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 = the Element of F " {(support (max (B,(InvLexOrder NAT))))} ) or IT1 = IT2 )
given 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 = the Element of F1 " {(support (max (B1,(InvLexOrder NAT))))}
; ( 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 = the Element of F " {(support (max (B,(InvLexOrder NAT))))} ) or IT1 = IT2 )
given 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 = the Element of F2 " {(support (max (B2,(InvLexOrder NAT))))}
; IT1 = IT2
then A26:
B2 c= B1
;
then
B1 c= B2
;
then
B1 = B2
by A26, XBOOLE_0:def 10;
hence
IT1 = IT2
by A17, A20, A22, A25; verum