let F be Field; :: thesis: for VS being strict VectSp of F

for H being non empty Subset of (Subspaces VS) holds not (carr VS) .: H is empty

let VS be strict VectSp of F; :: thesis: for H being non empty Subset of (Subspaces VS) holds not (carr VS) .: H is empty

let H be non empty Subset of (Subspaces VS); :: thesis: not (carr VS) .: H is empty

consider x being Element of Subspaces VS such that

A1: x in H by SUBSET_1:4;

(carr VS) . x in (carr VS) .: H by A1, FUNCT_2:35;

hence not (carr VS) .: H is empty ; :: thesis: verum

for H being non empty Subset of (Subspaces VS) holds not (carr VS) .: H is empty

let VS be strict VectSp of F; :: thesis: for H being non empty Subset of (Subspaces VS) holds not (carr VS) .: H is empty

let H be non empty Subset of (Subspaces VS); :: thesis: not (carr VS) .: H is empty

consider x being Element of Subspaces VS such that

A1: x in H by SUBSET_1:4;

(carr VS) . x in (carr VS) .: H by A1, FUNCT_2:35;

hence not (carr VS) .: H is empty ; :: thesis: verum