let G be _Graph; :: thesis: for E1, E2 being RepDEdgeSelection of G holds card E1 = card E2
let E1, E2 be RepDEdgeSelection of G; :: thesis: 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; :: thesis: verum