let
X
,
A
,
B
be
set
;
:: thesis:
(
A
in
Fin
X
&
B
c=
A
implies
B
in
Fin
X
)
assume
that
A1
:
A
in
Fin
X
and
A2
:
B
c=
A
;
:: thesis:
B
in
Fin
X
A
c=
X
by
A1
,
FINSUB_1:def 5
;
then
B
c=
X
by
A2
;
hence
B
in
Fin
X
by
A1
,
A2
,
FINSUB_1:def 5
;
:: thesis:
verum