let X be non empty set ; :: thesis: for G being SimpleGraph of X
for v being set ex ww being finite set st
( ww = { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) } & degree G,v = card ww )
let G be SimpleGraph of X; :: thesis: for v being set ex ww being finite set st
( ww = { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) } & degree G,v = card ww )
let v be set ; :: thesis: ex ww being finite set st
( ww = { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) } & degree G,v = card ww )
consider Y being finite set such that
A1: ( ( for z being set holds
( z in Y iff ( z in the SEdges of G & v in z ) ) ) & degree G,v = card Y ) by Def11;
set ww = { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) } ;
A2: for z being set holds
( z in { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) } iff ( z in the carrier of G & {v,z} in the SEdges of G ) )

proof

let z be set ; :: thesis: ( z in { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) } iff ( z in the carrier of G & {v,z} in the SEdges of G ) )

hereby :: thesis: ( z in the carrier of G & {v,z} in the SEdges of G implies z in { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) } )

assume z in { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) } ; :: thesis: ( z in the carrier of G & {v,z} in the SEdges of G )
then consider w being Element of X such that
A3: ( z = w & w in the carrier of G & {v,w} in the SEdges of G ) ;
thus ( z in the carrier of G & {v,z} in the SEdges of G ) by A3; :: thesis: verum

end;

thus ( z in the carrier of G & {v,z} in the SEdges of G implies z in { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) } ) :: thesis: verum

proof

assume A4: ( z in the carrier of G & {v,z} in the SEdges of G ) ; :: thesis: z in { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) }
the carrier of G is finite Subset of X by Th27;
hence z in { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) } by A4; :: thesis: verum

end;

end;

A5: the carrier of G is finite by Th27;
A6: { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) } c= the carrier of G

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) } or z in the carrier of G )
assume z in { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) } ; :: thesis: z in the carrier of G
hence z in the carrier of G by A2; :: thesis: verum

end;

then reconsider ww = { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) } as finite set by A5;
take ww ; :: thesis: ( ww = { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) } & degree G,v = card ww )
ww,Y are_equipotent

proof

set wwY = { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } ;
A7: for w being set holds
( [w,{v,w}] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } iff ( w in ww & {v,w} in Y ) )

proof

let w be set ; :: thesis: ( [w,{v,w}] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } iff ( w in ww & {v,w} in Y ) )

hereby :: thesis: ( w in ww & {v,w} in Y implies [w,{v,w}] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } )

assume [w,{v,w}] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } ; :: thesis: ( w in ww & {v,w} in Y )
then consider w' being Element of X such that
A8: ( [w,{v,w}] = [w',{v,w'}] & w' in ww & {v,w'} in Y ) ;
w = [w',{v,w'}] `1 by A8, MCART_1:7
.= w' by MCART_1:7 ;
hence ( w in ww & {v,w} in Y ) by A8; :: thesis: verum

end;

thus ( w in ww & {v,w} in Y implies [w,{v,w}] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } ) :: thesis: verum

proof

assume A9: ( w in ww & {v,w} in Y ) ; :: thesis: [w,{v,w}] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) }
the carrier of G is finite Subset of X by Th27;
then ( w in the carrier of G & the carrier of G c= X ) by A6, A9;
then reconsider w = w as Element of X ;
ex z being Element of X st
( [w,{v,w}] = [z,{v,z}] & z in ww & {v,z} in Y ) by A9;
hence [w,{v,w}] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } ; :: thesis: verum

end;

end;

A10: for x being set st x in ww holds
ex y being set st
( y in Y & [x,y] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } )

proof

let x be set ; :: thesis: ( x in ww implies ex y being set st
( y in Y & [x,y] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } ) )
assume A11: x in ww ; :: thesis: ex y being set st
( y in Y & [x,y] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } )
then A12: ( x in the carrier of G & {v,x} in the SEdges of G ) by A2;
A13: v in {v,x} by TARSKI:def 2;
take {v,x} ; :: thesis: ( {v,x} in Y & [x,{v,x}] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } )
thus {v,x} in Y by A1, A12, A13; :: thesis: [x,{v,x}] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) }
hence [x,{v,x}] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } by A7, A11; :: thesis: verum

end;

A14: for y being set st y in Y holds
ex x being set st
( x in ww & [x,y] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } )

proof

let y be set ; :: thesis: ( y in Y implies ex x being set st
( x in ww & [x,y] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } ) )
assume A15: y in Y ; :: thesis: ex x being set st
( x in ww & [x,y] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } )
then A16: ( y in the SEdges of G & v in y ) by A1;
ex w being set st
( w in the carrier of G & y = {v,w} )

proof

consider v1, v2 being set such that
A17: ( v1 in the carrier of G & v2 in the carrier of G & v1 <> v2 & y = {v1,v2} ) by A16, Th10;

per cases ( v = v1 or v = v2 ) by A16, A17, TARSKI:def 2;

suppose A18: v = v1 ; :: thesis: ex w being set st
( w in the carrier of G & y = {v,w} )

take v2 ; :: thesis: ( v2 in the carrier of G & y = {v,v2} )
thus ( v2 in the carrier of G & y = {v,v2} ) by A17, A18; :: thesis: verum

end;

suppose A19: v = v2 ; :: thesis: ex w being set st
( w in the carrier of G & y = {v,w} )

take v1 ; :: thesis: ( v1 in the carrier of G & y = {v,v1} )
thus v1 in the carrier of G by A17; :: thesis: y = {v,v1}
thus y = {v,v1} by A17, A19; :: thesis: verum

end;

end;

end;

then consider w being set such that
A20: ( w in the carrier of G & y = {v,w} ) ;
take w ; :: thesis: ( w in ww & [w,y] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } )
thus w in ww by A2, A16, A20; :: thesis: [w,y] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) }
hence [w,y] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } by A7, A15, A20; :: thesis: verum

end;

A21: for x, y, z, u being set st [x,y] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } & [z,u] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } holds
( x = z iff y = u )

proof

let x, y, z, u be set ; :: thesis: ( [x,y] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } & [z,u] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } implies ( x = z iff y = u ) )
assume A22: ( [x,y] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } & [z,u] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } ) ; :: thesis: ( x = z iff y = u )
then consider w1 being Element of X such that
A23: ( [x,y] = [w1,{v,w1}] & w1 in ww & {v,w1} in Y ) ;
consider w2 being Element of X such that
A24: ( [z,u] = [w2,{v,w2}] & w2 in ww & {v,w2} in Y ) by A22;

hereby :: thesis: ( y = u implies x = z )

assume A25: x = z ; :: thesis: y = u
w1 = [x,y] `1 by A23, MCART_1:7
.= z by A25, MCART_1:7
.= [w2,{v,w2}] `1 by A24, MCART_1:7
.= w2 by MCART_1:7 ;
hence y = [w2,{v,w2}] `2 by A23, MCART_1:7
.= u by A24, MCART_1:7 ;
:: thesis: verum

end;

hereby :: thesis: verum

assume A26: y = u ; :: thesis: x = z
A27: {v,w1} = [x,y] `2 by A23, MCART_1:7
.= u by A26, MCART_1:7
.= [w2,{v,w2}] `2 by A24, MCART_1:7
.= {v,w2} by MCART_1:7 ;
{v,w1} in the SEdges of G by A1, A23;
then v <> w1 by Th12;
then w1 = w2 by A27, ZFMISC_1:10;
hence x = [z,u] `1 by A23, A24, MCART_1:7
.= z by MCART_1:7 ;
:: thesis: verum

end;

end;

take { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } ; :: according to TARSKI:def 6 :: thesis: ( ( for b₁ being set holds
( not b₁ in ww or ex b₂ being set st
( b₂ in Y & [b₁,b₂] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } ) ) ) & ( for b₁ being set holds
( not b₁ in Y or ex b₂ being set st
( b₂ in ww & [b₂,b₁] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } ) ) ) & ( for b₁, b₂, b₃, b₄ being set holds
( not [b₁,b₂] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } or not [b₃,b₄] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } or ( ( not b₁ = b₃ or b₂ = b₄ ) & ( not b₂ = b₄ or b₁ = b₃ ) ) ) ) )
thus ( ( for b₁ being set holds
( not b₁ in ww or ex b₂ being set st
( b₂ in Y & [b₁,b₂] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } ) ) ) & ( for b₁ being set holds
( not b₁ in Y or ex b₂ being set st
( b₂ in ww & [b₂,b₁] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } ) ) ) & ( for b₁, b₂, b₃, b₄ being set holds
( not [b₁,b₂] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } or not [b₃,b₄] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } or ( ( not b₁ = b₃ or b₂ = b₄ ) & ( not b₂ = b₄ or b₁ = b₃ ) ) ) ) ) by A10, A14, A21; :: thesis: verum

end;

hence ( ww = { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) } & degree G,v = card ww ) by A1, CARD_1:21; :: thesis: verum