let R be Ring; :: thesis: for V being LeftMod of R
for W being strict Subspace of V st W <> (0). V holds
ex v being Vector of V st
( v in W & v <> 0. V )
let V be LeftMod of R; :: thesis: for W being strict Subspace of V st W <> (0). V holds
ex v being Vector of V st
( v in W & v <> 0. V )
let W be strict Subspace of V; :: thesis: ( W <> (0). V implies ex v being Vector of V st
( v in W & v <> 0. V ) )
assume A1: W <> (0). V ; :: thesis: ex v being Vector of V st
( v in W & v <> 0. V )
A2: 0. V in W by VECTSP_4:17;
the carrier of W <> {(0. V)} by A1, VECTSP_4:def 3;
then {(0. V)} c< the carrier of W by A2, ZFMISC_1:31;
then consider v being object such that
A3: v in the carrier of W and
A4: not v in {(0. V)} by XBOOLE_0:6;
reconsider v = v as Vector of V by A3, VECTSP_4:10;
take v ; :: thesis: ( v in W & v <> 0. V )
thus ( v in W & v <> 0. V ) by A3, A4, TARSKI:def 1; :: thesis: verum