let K be Ring; :: thesis: for M, N being LeftMod of K st M c= N holds
M c= (Omega). N
let M, N be LeftMod of K; :: thesis: ( M c= N implies M c= (Omega). N )
assume M c= N ; :: thesis: M c= (Omega). N
then A1: M is Subspace of N ;
N is Subspace of (Omega). N by Th4;
then M is Subspace of (Omega). N by A1, VECTSP_4:26;
hence M c= (Omega). N ; :: thesis: verum