let F be Field; :: thesis: for x being object
for VS being strict VectSp of F
for S being Subset of VS st not S is empty & S is linearly-closed & x in Lin S holds
x in S
let x be object ; :: thesis: for VS being strict VectSp of F
for S being Subset of VS st not S is empty & S is linearly-closed & x in Lin S holds
x in S
let VS be strict VectSp of F; :: thesis: for S being Subset of VS st not S is empty & S is linearly-closed & x in Lin S holds
x in S
let S be Subset of VS; :: thesis: ( not S is empty & S is linearly-closed & x in Lin S implies x in S )
assume ( not S is empty & S is linearly-closed ) ; :: thesis: ( not x in Lin S or x in S )
then consider W being strict Subspace of VS such that
A1: S = the carrier of W by VECTSP_4:34;
assume A2: x in Lin S ; :: thesis: x in S
Lin S = W by A1, VECTSP_7:11;
hence x in S by A2, A1, STRUCT_0:def 5; :: thesis: verum