let R be Relation; :: thesis: card R = card (R ~)
defpred S₁[ object , object ] means for x, y being object st [x,y] = $1 holds
[y,x] = $2;
A1: for x being object st x in R holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in R implies ex y being object st S₁[x,y] )
assume x in R ; :: thesis: ex y being object st S₁[x,y]
then consider y, z being object such that
A2: [y,z] = x by RELAT_1:def 1;
take zy = [z,y]; :: thesis: S₁[x,zy]
let w, t be object ; :: thesis: ( [w,t] = x implies [t,w] = zy )
assume A3: [w,t] = x ; :: thesis: [t,w] = zy
then w = y by A2, XTUPLE_0:1;
hence [t,w] = zy by A3, A2, XTUPLE_0:1; :: thesis: verum

end;

consider h being Function such that
A4: ( dom h = R & ( for x being object st x in R holds
S₁[x,h . x] ) ) from CLASSES1:sch 1(A1);
A5: h is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom h or not x2 in dom h or not h . x1 = h . x2 or x1 = x2 )
assume that
A6: x1 in dom h and
A7: x2 in dom h and
A8: h . x1 = h . x2 ; :: thesis: x1 = x2
consider y2, z2 being object such that
A9: x2 = [y2,z2] by A4, A7, RELAT_1:def 1;
A10: h . x2 = [z2,y2] by A7, A9, A4;
consider y1, z1 being object such that
A11: x1 = [y1,z1] by A6, A4, RELAT_1:def 1;
A12: h . x1 = [z1,y1] by A11, A6, A4;
then z1 = z2 by A10, A8, XTUPLE_0:1;
hence x1 = x2 by A12, A10, A8, XTUPLE_0:1, A11, A9; :: thesis: verum

end;

A13: rng h c= R ~

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng h or y in R ~ )
assume y in rng h ; :: thesis: y in R ~
then consider x being object such that
A14: x in dom h and
A15: h . x = y by FUNCT_1:def 3;
consider t, r being object such that
A16: x = [t,r] by A4, A14, RELAT_1:def 1;
h . x = [r,t] by A14, A16, A4;
hence y in R ~ by A14, A16, A4, RELAT_1:def 7, A15; :: thesis: verum

end;

R ~ c= rng h

proof

let y, z be object ; :: according to RELAT_1:def 3 :: thesis: ( not [y,z] in R ~ or [y,z] in rng h )
assume [y,z] in R ~ ; :: thesis: [y,z] in rng h
then A17: [z,y] in R by RELAT_1:def 7;
then h . [z,y] = [y,z] by A4;
hence [y,z] in rng h by A17, A4, FUNCT_1:def 3; :: thesis: verum

end;

then rng h = R ~ by A13;
hence card R = card (R ~) by A5, WELLORD2:def 4, A4, CARD_1:5; :: thesis: verum