:: deftheorem defines EdgesCount GRAPH_1:def 20 :
for G being finite Graph
for b₂ being Element of NAT holds
( b₂ = EdgesCount G iff ex B being finite set st
( B = the carrier' of G & b₂ = card B ) );