let K be Ring; :: thesis:
let M1, N, M2 be LeftMod of K; :: thesis:
assume A1: ( M1 c= N & M2 c= N ) ; :: thesis:
thus 0. M1 = 0. M2 :: thesis:

proof

reconsider M1' = M1, M2' = M2 as Subspace of N by A1, Def7;
0. M1' = 0. M2' by VECTSP_4:20;
hence 0. M1 = 0. M2 ; :: thesis:

end;

thus 0. M1 in M2 :: thesis:

proof

reconsider M1' = M1, M2' = M2 as Subspace of N by A1, Def7;
0. M1' in M2' by VECTSP_4:26;
hence 0. M1 in M2 ; :: thesis:

end;

thus ( the carrier of M1 c= the carrier of M2 implies M1 c= M2 ) :: thesis:

proof

assume A2: the carrier of M1 c= the carrier of M2 ; :: thesis:
reconsider M1' = M1, M2' = M2 as Subspace of N by A1, Def7;
M1' is Subspace of M2' by A2, VECTSP_4:35;
hence M1 c= M2 by Def7; :: thesis:

end;

thus ( ( for n being Vector of N st n in M1 holds
n in M2 ) implies M1 c= M2 ) :: thesis:

proof

assume A3: for n being Vector of N st n in M1 holds
n in M2 ; :: thesis:
reconsider M1' = M1, M2' = M2 as Subspace of N by A1, Def7;
M1' is Subspace of M2' by A3, VECTSP_4:36;
hence M1 c= M2 by Def7; :: thesis:

end;

thus ( the carrier of M1 = the carrier of M2 & M1 is strict & M2 is strict implies M1 = M2 ) :: thesis:

proof

assume that
A4: the carrier of M1 = the carrier of M2 and
A5: ( M1 is strict & M2 is strict ) ; :: thesis:
reconsider M1' = M1 as strict Subspace of N by A1, A5, Def7;
reconsider M2' = M2 as strict Subspace of N by A1, A5, Def7;
M1' = M2' by A4, VECTSP_4:37;
hence M1 = M2 ; :: thesis:

end;

thus (0). M1 c= M2 :: thesis:

proof

reconsider M1' = M1, M2' = M2 as Subspace of N by A1, Def7;
(0). M1' is Subspace of M2' by VECTSP_4:51;
hence (0). M1 c= M2 by Def7; :: thesis:

end;