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 ;

take D9 ; :: thesis: for x being object holds

( x in D9 iff x is LINE of V )

( x in D9 iff x is LINE of V ) ; :: thesis: verum

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

then reconsider D9 = D as LINE_DOMAIN of V by Def3;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;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

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 ) )

hence
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

end;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;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

( x in D9 iff x is LINE of V ) ; :: thesis: verum