x
in
{
x
}
by
TARSKI:def 1
;
hence
{
[
x
,
x
]
}
is
Relation
of
{
x
}
by
RELSET_1:3
;
:: thesis:
verum