let G be _Graph; for E1, E2 being RepDEdgeSelection of G holds card E1 = card E2
let E1, E2 be RepDEdgeSelection of G; card E1 = card E2
consider f being one-to-one Function such that
A1:
( dom f = E1 & rng f = E2 )
and
for e, v, w being object st e in E1 holds
( e DJoins v,w,G iff f . e DJoins v,w,G )
by Th87;
thus
card E1 = card E2
by A1, WELLORD2:def 4, CARD_1:5; verum