set p = the Element of T;
take T | the Element of T ; :: thesis: ex p being Element of T st T | the Element of T = T | p
take the Element of T ; :: thesis: T | the Element of T = T | the Element of T
thus T | the Element of T = T | the Element of T ; :: thesis: verum