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 )
A1: (0). W is Subspace of V by VECTSP_4:49;
A2: (0). V is Subspace of W by VECTSP_4:50;
A3: (0). W1 is Subspace of W2 by VECTSP_4:51;
thus (0). W c= V by A1, Def7; :: thesis: ( (0). V c= W & (0). W1 c= W2 )
thus (0). V c= W by A2, Def7; :: thesis: (0). W1 c= W2
thus (0). W1 c= W2 by A3, Def7; :: thesis: verum