let
a
,
b
,
c
be
object
;
:: thesis:
(
(
a
,
b
)
.-->
c
)
.
(
a
,
b
)
=
c
[
a
,
b
]
in
{
[
a
,
b
]
}
by
TARSKI:def 1
;
hence
(
(
a
,
b
)
.-->
c
)
.
(
a
,
b
)
=
c
by
Th7
;
:: thesis:
verum