reconsider K = { A where A is Subset of T : p in Int A } as correct basis of p by Lm4, Lm5;
take K ; :: thesis: ( not K is empty & K is correct )
thus ( not K is empty & K is correct ) ; :: thesis: verum