set D = { a where a is Element of Submodules V : a is LINE of V } ;
set a1 = the LINE of V;
reconsider a2 = the LINE of V 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 :: thesis: for x being set st x in D holds
x is LINE of V

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 ex a being Element of Submodules V st
( x = a & a is LINE of V ) ;
hence x is LINE of V ; :: thesis: verum

end;

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

now :: thesis: for x being object holds
( ( x in D9 implies x is LINE of V ) & ( x is LINE of V implies x in D9 ) )

let x be object ; :: thesis: ( ( x in D9 implies x is LINE of V ) & ( x is LINE of V implies x in D9 ) )
thus ( x in D9 implies x is LINE of V ) by A1; :: thesis: ( x is LINE of V implies x in D9 )
thus ( x is LINE of V implies x in D9 ) :: thesis: verum

proof

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

end;

end;

hence for x being object holds
( x in D9 iff x is LINE of V ) ; :: thesis: verum