let K be Ring; :: thesis: for V being LeftMod of K
for W, W1, W2 being Subspace of V holds
( (0). W c= V & (0). V c= W & (0). W1 c= W2 )
let V be LeftMod of K; :: thesis: for W, W1, W2 being Subspace of V holds
( (0). W c= V & (0). V c= W & (0). W1 c= W2 )
let W, W1, W2 be Subspace of V; :: thesis: ( (0). W c= V & (0). V c= W & (0). W1 c= W2 )
(0). W is Subspace of V by VECTSP_4:49;
hence (0). W c= V by Def7; :: thesis: ( (0). V c= W & (0). W1 c= W2 )
(0). V is Subspace of W by VECTSP_4:50;
hence (0). V c= W by Def7; :: thesis: (0). W1 c= W2
(0). W1 is Subspace of W2 by VECTSP_4:51;
hence (0). W1 c= W2 by Def7; :: thesis: verum