let V be RealLinearSpace; :: thesis: for V1 being Subspace of V
for W1 being Subspace of V1
for v being VECTOR of V st v in W1 holds
v is VECTOR of V1
let V1 be Subspace of V; :: thesis: for W1 being Subspace of V1
for v being VECTOR of V st v in W1 holds
v is VECTOR of V1
let W1 be Subspace of V1; :: thesis: for v being VECTOR of V st v in W1 holds
v is VECTOR of V1
let v be VECTOR of V; :: thesis: ( v in W1 implies v is VECTOR of V1 )
assume v in W1 ; :: thesis: v is VECTOR of V1
then ( the carrier of W1 c= the carrier of V1 & v in the carrier of W1 ) by RLSUB_1:def 2;
hence v is VECTOR of V1 ; :: thesis: verum