let V be strict RealLinearSpace; :: thesis: for A, B being Subset of V st Lin A = V & A c= B holds

Lin B = V

let A, B be Subset of V; :: thesis: ( Lin A = V & A c= B implies Lin B = V )

assume ( Lin A = V & A c= B ) ; :: thesis: Lin B = V

then V is Subspace of Lin B by Th20;

hence Lin B = V by RLSUB_1:26; :: thesis: verum

Lin B = V

let A, B be Subset of V; :: thesis: ( Lin A = V & A c= B implies Lin B = V )

assume ( Lin A = V & A c= B ) ; :: thesis: Lin B = V

then V is Subspace of Lin B by Th20;

hence Lin B = V by RLSUB_1:26; :: thesis: verum