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