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

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