let R be domRing; :: thesis: for V being strict LeftMod of R
for A, B being Subset of V st Lin A = V & A c= B holds
Lin B = V
let V be strict LeftMod of R; :: 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 Th13;
hence Lin B = V by VECTSP_4:25; :: thesis: verum