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