let R be Ring; :: thesis: for V being LeftMod of R
for A, B being Subset of V st Lin A = V & A c= B holds
Lin B = V
let V be 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 that
A1: Lin A = V and
A2: A c= B ; :: thesis: Lin B = V
V is Subspace of Lin B by A1, A2, Th10;
hence Lin B = V by A1, VECTSP_4:25; :: thesis: verum