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

then B1 = B2 by A26, XBOOLE_0:def 10;

hence IT1 = IT2 by A17, A20, A22, A25; :: thesis: verum

( 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

then A26:
B2 c= B1
;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;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

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

x in B2

then
B1 c= B2
;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;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

then B1 = B2 by A26, XBOOLE_0:def 10;

hence IT1 = IT2 by A17, A20, A22, A25; :: thesis: verum