chose better names for ax1, ax2, ax3 (topology mixin)

[affeldt-aist]

analysis/theories/topology.v

Lines 1616 to 1619 in 0e392b5

	ax1 : forall p : T, ProperFilter (nbhs p) ;
	ax2 : forall p : T, nbhs p =
	[set A : set T | exists B : set T, [/\ open B, B p & B `<=` A] ] ;
	ax3 : open = [set A : set T | A `<=` nbhs^~ A ]

[affeldt-aist]

ax1 -> nbhs_pfilter
ax3 -> openE
ax2 -> nbhsE