set e = the Element of M;
take the Element of M ; :: thesis: the Element of M is strict
thus the Element of M is strict by Def2; :: thesis: verum