Consolidate use of Ishikawa's result for countably metacompact

[prabau]

Consolidate use of Ishikawa's result for countably metacompact (plus some streamlining).

Also, simplify the description of S61 (pointed irrational extension of the reals), similar to S60.

[yhx-12243]

Maybe we can do the same things for P32 (Countably paracompact).

[prabau]

Maybe we can do the same things for P32 (Countably paracompact).

There are in fact many other equivalent characterizations for both countably paracompact and countably metacompact.
I think it would be more useful to add it if we get an opportunity to make use of it in the proof of some theorem or some trait.
So I would say it can wait if it is not needed at the moment.

[yhx-12243]

No other problems, okay for now.