deffunc
H
_{1}
(
set
)
->
Element
of
X
= the
Element
of
X
;
defpred
S
_{1}
[
set
]
means
X
in
X
\
{
{}
}
;
{
[
x
,
H
_{1}
(
x
)
]
where
x
is
Element
of
X
\
{
{}
}
:
S
_{1}
[
x
] } is
Function
from
FOMODEL0:sch 3
();
hence
(
ChoiceOn
X
is
Relation-like
&
ChoiceOn
X
is
Function-like
) ;
:: thesis:
verum