let IT1, IT2 be Element of NAT ; :: thesis: ( ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the SEdges of G & v in z ) ) ) & IT1 = card X ) & ex X being finite set st
( ( for z being set holds
( z in X iff ( z in the SEdges of G & v in z ) ) ) & IT2 = card X ) implies IT1 = IT2 )
assume ( ex X1 being finite set st
( ( for z being set holds
( z in X1 iff ( z in the SEdges of G & v in z ) ) ) & IT1 = card X1 ) & ex X2 being finite set st
( ( for z being set holds
( z in X2 iff ( z in the SEdges of G & v in z ) ) ) & IT2 = card X2 ) ) ; :: thesis: IT1 = IT2
then consider X1, X2 being finite set such that
A3: ( ( for z being set holds
( z in X1 iff ( z in the SEdges of G & v in z ) ) ) & IT1 = card X1 & ( for z being set holds
( z in X2 iff ( z in the SEdges of G & v in z ) ) ) & IT2 = card X2 ) ;
A4: X1 c= X2

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in X1 or z in X2 )
assume z in X1 ; :: thesis: z in X2
then ( z in the SEdges of G & v in z ) by A3;
hence z in X2 by A3; :: thesis: verum

end;

X2 c= X1

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in X2 or z in X1 )
assume z in X2 ; :: thesis: z in X1
then ( z in the SEdges of G & v in z ) by A3;
hence z in X1 by A3; :: thesis: verum

end;

hence IT1 = IT2 by A3, A4, XBOOLE_0:def 10; :: thesis: verum