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 ;

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

( x in D9 iff x is HIPERPLANE of V )

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

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

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

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

hence
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

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

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