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