reconsider
m
=
n
as
Element
of
NAT
by
ORDINAL1:def 12
;
let
x
be
Element
of
Rank
n
;
:: thesis:
x
is
finite
per
cases
(
Rank
n
=
{}
or
Rank
n
<>
{}
)
;
suppose
Rank
n
=
{}
;
:: thesis:
x
is
finite
hence
x
is
finite
;
:: thesis:
verum
end;
suppose
A1
:
Rank
n
<>
{}
;
:: thesis:
x
is
finite
A2
:
Rank
m
is
finite
by
CARD_2:67
;
x
c=
Rank
n
by
A1
,
ORDINAL1:def 2
;
hence
x
is
finite
by
A2
;
:: thesis:
verum
end;
end;