let
A
be
set
;
:: thesis:
for
x
being
object
holds
(
A
-->
x
)
"
{
x
}
=
A
let
x
be
object
;
:: thesis:
(
A
-->
x
)
"
{
x
}
=
A
x
in
{
x
}
by
TARSKI:def 1
;
hence
(
A
-->
x
)
"
{
x
}
=
A
by
Th14
;
:: thesis:
verum