let G be _Graph; :: thesis: for E1, E2 being RepEdgeSelection of G holds card E1 = card E2
let E1, E2 be RepEdgeSelection 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 Joins v,w,G iff f . e Joins v,w,G ) by Th85;
thus card E1 = card E2 by A1, WELLORD2:def 4, CARD_1:5; :: thesis: verum