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