reconsider P = { A where A is Subset of T : p in Int A } as basis of p by Lm4;
take P ; :: thesis: P is correct
thus P is correct by Lm5; :: thesis: verum