set D = { a where a is Element of Submodules V : a is LINE of V } ;
consider a1 being LINE of V;
reconsider a2 = a1 as Element of Submodules V by VECTSP_5:def 3;
a2 in { a where a is Element of Submodules V : a is LINE of V } ;
then reconsider D = { a where a is Element of Submodules V : a is LINE of V } as non empty set ;

A1: now

let x be set ; :: thesis: ( x in D implies x is LINE of V )
assume x in D ; :: thesis: x is LINE of V
then consider a being Element of Submodules V such that
A2: ( x = a & a is LINE of V ) ;
thus x is LINE of V by A2; :: thesis: verum

end;

then reconsider D' = D as LINE_DOMAIN of V by Def3;
take D' ; :: thesis: for x being set holds
( x in D' iff x is LINE of V )

now

let x be set ; :: thesis: ( ( x in D' implies x is LINE of V ) & ( x is LINE of V implies x in D' ) )
thus ( x in D' implies x is LINE of V ) by A1; :: thesis: ( x is LINE of V implies x in D' )
thus ( x is LINE of V implies x in D' ) :: thesis: verum

proof

assume A3: x is LINE of V ; :: thesis: x in D'
then reconsider x1 = x as Element of Submodules V by VECTSP_5:def 3;
x1 in D by A3;
hence x in D' ; :: thesis: verum

end;

end;

hence for x being set holds
( x in D' iff x is LINE of V ) ; :: thesis: verum