let
A
,
C
be
Ordinal
;
:: thesis:
( 1
in
C
&
A
<>
{}
implies 1
in
exp
(
C
,
A
) )
assume
that
A1
: 1
in
C
and
A2
:
A
<>
{}
;
:: thesis:
1
in
exp
(
C
,
A
)
exp
(
C
,
{}
)
=
1
by
ORDINAL2:43
;
hence
1
in
exp
(
C
,
A
)
by
A1
,
A2
,
Th24
,
ORDINAL3:8
;
:: thesis:
verum