set
a
= the
LINE
of
V
;
set
D
=
{
the
LINE
of
V
}
;
take
{
the
LINE
of
V
}
;
:: thesis:
for
x
being
set
st
x
in
{
the
LINE
of
V
}
holds
x
is
LINE
of
V
thus
for
x
being
set
st
x
in
{
the
LINE
of
V
}
holds
x
is
LINE
of
V
by
TARSKI:def 1
;
:: thesis:
verum