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