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

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