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 ) ) and
A4: IT1 = card X1 and
A5: for z being set holds
( z in X2 iff ( z in the SEdges of G & v in z ) ) and
A6: IT2 = card X2 ;
A7: X2 c= X1
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in X2 or z in X1 )
reconsider zz = z as set by TARSKI:1;
assume z in X2 ; :: thesis: z in X1
then ( z in the SEdges of G & v in zz ) by A5;
hence z in X1 by A3; :: thesis: verum
end;
X1 c= X2
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in X1 or z in X2 )
reconsider zz = z as set by TARSKI:1;
assume z in X1 ; :: thesis: z in X2
then ( z in the SEdges of G & v in zz ) by A3;
hence z in X2 by A5; :: thesis: verum
end;
hence IT1 = IT2 by A4, A6, A7, XBOOLE_0:def 10; :: thesis: verum