let X be non empty set ; :: thesis:
let G be SimpleGraph of X; :: thesis:
let v be set ; :: thesis:
set ww = { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) } ;
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 ) ) and
A2: degree (G,v) = card Y by Def11;
A3: 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 ) )

let z be set ; :: thesis:

hereby :: thesis:

assume z in { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) } ; :: thesis:
then ex w being Element of X st
( z = w & w in the carrier of G & {v,w} in the SEdges of G ) ;
hence ( z in the carrier of G & {v,z} in the SEdges of G ) ; :: thesis:

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:

proof

assume A4: ( z in the carrier of G & {v,z} in the SEdges of G ) ; :: thesis:
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:

end;

A5: { 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:
assume z in { w where w is Element of X : ( w in the carrier of G & {v,w} in the SEdges of G ) } ; :: thesis:
hence z in the carrier of G by A3; :: thesis:

end;

the carrier of G is finite by Th27;
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,Y are_equipotent

proof

set wwY = { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } ;
take { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } ; :: according to TARSKI:def 6 :: thesis:
A6: 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:
assume that
A7: [x,y] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } and
A8: [z,u] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } ; :: thesis:
consider w1 being Element of X such that
A9: [x,y] = [w1,{v,w1}] and
w1 in ww and
A10: {v,w1} in Y by A7;
consider w2 being Element of X such that
A11: [z,u] = [w2,{v,w2}] and
w2 in ww and
{v,w2} in Y by A8;

hereby :: thesis:

assume A12: x = z ; :: thesis:
w1 = [x,y] `1 by A9, MCART_1:7
.= z by A12, MCART_1:7
.= [w2,{v,w2}] `1 by A11, MCART_1:7
.= w2 by MCART_1:7 ;
hence y = [w2,{v,w2}] `2 by A9, MCART_1:7
.= u by A11, MCART_1:7 ;
:: thesis:

end;

hereby :: thesis:

{v,w1} in the SEdges of G by A1, A10;
then A13: v <> w1 by Th12;
assume A14: y = u ; :: thesis:
{v,w1} = [x,y] `2 by A9, MCART_1:7
.= u by A14, MCART_1:7
.= [w2,{v,w2}] `2 by A11, MCART_1:7
.= {v,w2} by MCART_1:7 ;
then w1 = w2 by A13, ZFMISC_1:6;
hence x = [z,u] `1 by A9, A11, MCART_1:7
.= z by MCART_1:7 ;
:: thesis:

end;

A15: 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:

hereby :: thesis:

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

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:

proof

assume that
A18: w in ww and
A19: {v,w} in Y ; :: thesis:
A20: w in the carrier of G by A5, A18;
the carrier of G is finite Subset of X by Th27;
then reconsider w = w as Element of X by A20;
ex z being Element of X st
( [w,{v,w}] = [z,{v,z}] & z in ww & {v,z} in Y ) by A18, A19;
hence [w,{v,w}] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } ; :: thesis:

end;

A21: 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:
assume A22: y in Y ; :: thesis:
then A23: y in the SEdges of G by A1;
A24: v in y by A1, A22;
ex w being set st
( w in the carrier of G & y = {v,w} )

proof

consider v1, v2 being set such that
A25: v1 in the carrier of G and
A26: v2 in the carrier of G and
v1 <> v2 and
A27: y = {v1,v2} by A23, Th10;

per cases by A24, A27, TARSKI:def 2;

suppose A28: v = v1 ; :: thesis:

take v2 ; :: thesis:
thus ( v2 in the carrier of G & y = {v,v2} ) by A26, A27, A28; :: thesis:

end;

suppose A29: v = v2 ; :: thesis:

take v1 ; :: thesis:
thus v1 in the carrier of G by A25; :: thesis:
thus y = {v,v1} by A27, A29; :: thesis:

end;

then consider w being set such that
A30: w in the carrier of G and
A31: y = {v,w} ;
take w ; :: thesis:
thus w in ww by A3, A23, A30, A31; :: thesis:
hence [w,y] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } by A15, A22, A31; :: thesis:

end;

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:
assume A32: x in ww ; :: thesis:
take {v,x} ; :: thesis:
A33: v in {v,x} by TARSKI:def 2;
{v,x} in the SEdges of G by A3, A32;
hence {v,x} in Y by A1, A33; :: thesis:
hence [x,{v,x}] in { [w,{v,w}] where w is Element of X : ( w in ww & {v,w} in Y ) } by A15, A32; :: thesis:

end;

hence ( ( 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 A21, A6; :: thesis:

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 A2, CARD_1:5; :: thesis: