consider e being Element of M;
take e ; :: thesis: e is strict
thus e is strict by Def2; :: thesis: verum