let IT1, IT2 be Vertex of G; :: thesis: ( ( 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 ) ; :: 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 = 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 ; :: 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 = 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))))} ; :: 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 = 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))))} ; :: thesis: IT1 = IT2

now :: thesis: for x being object st x in B2 holds
x in B1

let x be object ; :: 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 ;

now :: thesis: for x being object st x in B1 holds
x in B2

let x be object ; :: 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 ;
then B1 = B2 by A26, XBOOLE_0:def 10;
hence IT1 = IT2 by A17, A20, A22, A25; :: thesis: verum