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

A1: now :: thesis: for x being set st x in D holds
x is HIPERPLANE of V

let x be set ; :: thesis: ( x in D implies x is HIPERPLANE of V )
assume x in D ; :: thesis: x is HIPERPLANE of V
then ex a being Element of Submodules V st
( x = a & a is HIPERPLANE of V ) ;
hence x is HIPERPLANE of V ; :: thesis: verum

end;

then reconsider D9 = D as HIPERPLANE_DOMAIN of V by Def6;
take D9 ; :: thesis: for x being object holds
( x in D9 iff x is HIPERPLANE of V )

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

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

proof

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

end;

end;

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