consider p being Element of [:the carrier of M,the carrier of M:];
take p ~ ; :: thesis: ex p being Element of [:the carrier of M,the carrier of M:] st p ~ = p ~
thus ex p being Element of [:the carrier of M,the carrier of M:] st p ~ = p ~ ; :: thesis: verum