Support p = Support |.p.| by Th3;
hence |.p.| is finite-Support ; :: thesis: verum