set z = the Element of Q;
take P --> the Element of Q ; :: thesis: P --> the Element of Q is continuous
thus P --> the Element of Q is continuous by Th7; :: thesis: verum