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